2009/2/15 Brandon S. Allbery KF8NH <allbery@ece.cmu.edu>
On 2009 Feb 15, at 11:50, Peter Verswyvelen wrote:
I could try to read the article a couple of times again, but are there any other good readings about these existentially quantified types and how the ST monad works? 

You could think about it as playing a dirty trick on the typechecker.

But if you don't want to, there's another way to think about it.  I'm still working on this interpretation, so be gentle :-)

Think of the s in ST s a not as a type, but as itself a "state"; eg. a map from keys to values and a free list of fresh keys.  This is the initial state of the computation, which ST transforms.  Then runST says:

runST :: (forall s. ST s a) -> a

If a computation works on every initial state, we can extract the value.   Since it works for every initial state, it must not depend on it, and thus the computation's value is well-defined.

Something like that.  I think using existential types as regions is more essential than a "dirty trick", and I advocate trying to interpret it in a semantically well-defined way.

Luke