[Haskell-cafe] forall & ST monad
g9ks157k at acme.softbase.org
Mon Feb 16 13:22:04 EST 2009
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.
However, if we talk about existential types in Haskell, we usually mean these
special algebraic data types whose declarations have a forall part before a
data constructor. So it’s better to talk about rank-2 (or rank-n)
polymorphism when talking about runST.
More information about the Haskell-Cafe