Correct. And under the hood, GHC does implement runST in its existential dual form using a hidden State# type. I wonder however, if we're wandering too far away from the OP's query about grokking runST and "how the ST monad works." I'd imagine that means he'd like to see how rank-2 polymorphism keeps different threads separated, something which doesn't require existentials, much less the perforce crippled (because constructivist) duality between the two flavors of quantification. Wolfgang Jeltsch-2 wrote:
Am Montag, 16. Februar 2009 19:22 schrieb Wolfgang Jeltsch:
Am Montag, 16. Februar 2009 19:04 schrieb Kim-Ee Yeoh:
Despite its rank-2 type, runST really doesn't have anything to do with existential quantification.
First, I thought so too but I changed my mind. To my knowledge a type (forall a. T[a]) -> T' is equivalent to the type exists a. (T[a] -> T'). It’s the same as in predicate logic – Curry-Howard in action.
Oops, this is probably not true. The statement holds for classical predicate logic with only non-empty domains. But in constructivist logic only the first of the above statements follows from the second, not the other way round. So arguing with the Curry-Howard isomorphism fails and indeed, the two types are not equivalent. There is just a function from the second to the first (it’s the function application function ($) actually).
-- View this message in context: http://www.nabble.com/forall---ST-monad-tp22024677p22044960.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.