[Haskell-cafe] forall & ST monad
g9ks157k at acme.softbase.org
Mon Feb 16 13:36:29 EST 2009
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).
More information about the Haskell-Cafe