2009/2/15 Brandon S. Allbery KF8NH <span dir="ltr"><<a href="mailto:allbery@ece.cmu.edu">allbery@ece.cmu.edu</a>></span><br><div class="gmail_quote"><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
<div style=""><div><div class="Ih2E3d"><div>On 2009 Feb 15, at 11:50, Peter Verswyvelen wrote:</div><blockquote type="cite"><div><div><div><div>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? </div>
</div></div></div></blockquote><div><br></div></div><div>You could think about it as playing a dirty trick on the typechecker. </div></div></div></blockquote><div><br>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 :-)<br>
<br>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:<br>
<br>runST :: (forall s. ST s a) -> a<br><br>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.<br>
<br>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.<br><br>Luke<br></div></div>