[Haskell-cafe] forall & ST monad

[Kim-Ee Yeoh]

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.