[Haskell-cafe] forall & ST monad

[Luke Palmer]

2009/2/15 Brandon S. Allbery KF8NH <allbery at 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090215/1dcfd0a5/attachment.htm