(Encoding of existentials in terms of higher rank types)
Revision as of 01:03, 6 September 2012
Normal Haskell '98 types are considered Rank-1 types. A Haskell '98 type signature such as
a -> b -> a
implies that the type variables are universally quantified like so:
forall a b. a -> b -> a
forall a. a -> (forall b. b -> a)
is also a Rank-1 type because it is equivalent to the previous signature.However, a
Rank-N type reconstruction is undecidable in general, and some explicit type annotations are required in their presence.
Rank-2 or Rank-N types may be specifically enabled by the language extensions
2 Relation to Existentials
In order to unpack an existential type, you need a polymorphic function that works on any type that could be stored in the existential. This leads to a natural relation between higher-rank types and existentials; and an encoding of existentials in terms of higher rank types in continuation-passing style.
In general, you can replace
data T a1 .. ai = forall t1 .. tj. constraints => Constructor e1 .. ek
Constructor exp1 .. expk -- application of the constructor
case e of (Constructor pat1 .. patk) -> res
data T' a1 .. ai = Constructor' (forall b. (forall t1..tj. constraints => e1 -> e2 -> ... -> ek -> b) -> b)
Constructor' (\f -> f exp1 .. expk)
case e of (Constructor' f) -> let k pat1 .. patk = res in f k
3 See also
* Rank-N types on the Haskell' website. * The GHC User's Guide on higher-ranked polymorphism.