RankN types
From HaskellWiki
(Encoding of existentials in terms of higher rank types) 
Benmachine (Talk  contribs) 

Line 4:  Line 4:  
Normal Haskell '98 types are considered Rank1 types. A Haskell '98 type signature such as 
Normal Haskell '98 types are considered Rank1 types. A Haskell '98 type signature such as 

−  +  <haskell>a > b > a</haskell> 

−  <hask>a > b > a</hask> 

−  
implies that the type variables are universally quantified like so: 
implies that the type variables are universally quantified like so: 

−  +  <haskell>forall a b. a > b > a</haskell> 

−  <hask>forall a b. a > b > a</hask> 
+  <hask>forall</hask> can be floated out of the righthand side of <hask>></hask> if it appears there, so: 
−  +  <haskell>forall a. a > (forall b. b > a)</haskell> 

−  <hask>forall</hask> can be floated out of the righthand side of <hask>(>)</hask> if it appears there, so: 

−  
−  <hask>forall a. a > (forall b. b > a)</hask> 

−  
is also a Rank1 type because it is equivalent to the previous signature. 
is also a Rank1 type because it is equivalent to the previous signature. 

Line 27:  Line 27:  
In general, you can replace 
In general, you can replace 

+  <haskell>data T a1 .. ai = forall t1 .. tj. constraints => Constructor e1 .. ek</haskell> 

+  (where <hask>e1..ek</hask> are types in terms of <hask>a1..ai</hask> and <hask>t1..tj</hask>) 

−  <hask>data T a1 .. ai = forall t1 .. tj. constraints => Constructor e1 .. ek</hask> (where <hask>e1..ek</hask> are types in terms of <hask>a1..ai</hask> and <hask>t1..tj</hask>) 
+  <haskell>Constructor exp1 .. expk  application of the constructor</haskell> 
−  
−  <hask>Constructor exp1 .. expk  application of the constructor</hask> 

−  <hask>case e of (Constructor pat1 .. patk) > res</hask> 
+  <haskell>case e of (Constructor pat1 .. patk) > res</haskell> 
with 
with 

−  <hask>data T' a1 .. ai = Constructor' (forall b. (forall t1..tj. constraints => e1 > e2 > ... > ek > b) > b)</hask> 
+  <haskell>data T' a1 .. ai = Constructor' (forall b. (forall t1..tj. constraints => e1 > e2 > ... > ek > b) > b)</haskell> 
−  <hask>Constructor' (\f > f exp1 .. expk)</hask> 
+  <haskell>Constructor' (\f > f exp1 .. expk)</haskell> 
−  <hask>case e of (Constructor' f) > let k pat1 .. patk = res in f k</hask> 
+  <haskell>case e of (Constructor' f) > let k pat1 .. patk = res in f k</haskell> 
−  == Also see == 
+  == See also == 
−  [http://hackage.haskell.org/trac/haskellprime/wiki/RankNTypes RankN types] on the Haskell' website. 
+  * [http://hackage.haskell.org/trac/haskellprime/wiki/RankNTypes RankN types] on the Haskell' website. 
+  * [http://www.haskell.org/ghc/docs/latest/html/users_guide/othertypeextensions.html#universalquantification The GHC User's Guide on higherranked polymorphism.] 
Revision as of 01:03, 6 September 2012
1 About
Normal Haskell '98 types are considered Rank1 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 Rank1 type because it is equivalent to the previous signature.
However, aRankN type reconstruction is undecidable in general, and some explicit type annotations are required in their presence.
Rank2 or RankN 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 higherrank types and existentials; and an encoding of existentials in terms of higher rank types in continuationpassing 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
with
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
* RankN types on the Haskell' website. * The GHC User's Guide on higherranked polymorphism.