Difference between revisions of "RankN types"
(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 

−  
⚫  
⚫  
−  
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 
+  <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 29:  Line 27:  
In general, you can replace 
In general, you can replace 

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

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

−  < 
+  <haskell>data T' a1 .. ai = Constructor' (forall b. (forall t1..tj. constraints => e1 > e2 > ... > ek > b) > b)</haskell> 
−  < 
+  <haskell>Constructor' (\f > f exp1 .. expk)</haskell> 
−  < 
+  <haskell>case e of (Constructor' f) > let k pat1 .. patk = res in f k</haskell> 
−  == 
+  == 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
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
can be floated out of the righthand side of >
if it appears there, so:
forall a. a > (forall b. b > a)
is also a Rank1 type because it is equivalent to the previous signature.
However, a forall
appearing within the lefthand side of (>)
cannot be moved up, and therefore forms another level or rank. The type is labeled "RankN" where N is the number of forall
s which are nested and cannot be merged with a previous one. For example:
(forall a. a > a) > (forall b. b > b)
is a Rank2 type because the latter forall
can be moved to the start but the former one cannot. Therefore, there are two levels of universal quantification.
RankN 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
{# LANGUAGE Rank2Types #}
or {# LANGUAGE RankNTypes #}
.
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
(where e1..ek
are types in terms of a1..ai
and t1..tj
)
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
See also
* RankN types on the Haskell' website. * The GHC User's Guide on higherranked polymorphism.