RankN types
From HaskellWiki
m (not a stub) 
(→About: add new subsection on Churchencoded Lists, link/attribute to SO answer by sacundim) 

(4 intermediate revisions by 2 users not shown)  
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 22:  Line 22:  
<hask>{# LANGUAGE Rank2Types #}</hask> or <hask>{# LANGUAGE RankNTypes #}</hask>. 
<hask>{# LANGUAGE Rank2Types #}</hask> or <hask>{# LANGUAGE RankNTypes #}</hask>. 

+  == Churchencoded Lists == 

+  Churchencoded lists use RankNTypes too, as seen in [http://stackoverflow.com/a/15593349/849891 a StackOverflow answer by sacundim]: 

+  <haskell> 

+    Laws: 

+   

+   > runList xs cons nil == xs 

+   > runList (fromList xs) f z == foldr f z xs 

+   > foldr f z (toList xs) == runList xs f z 

+  newtype ChurchList a = 

+  ChurchList { runList :: forall r. (a > r > r) > r > r } 

+  
+    Make a 'ChurchList' out of a regular list. 

+  fromList :: [a] > ChurchList a 

+  fromList xs = ChurchList $ \k z > foldr k z xs 

+  
+    Turn a 'ChurchList' into a regular list. 

+  toList :: ChurchList a > [a] 

+  toList xs = runList xs (:) [] 

+  
+    The 'ChurchList' counterpart to '(:)'. Unlike 'DList', whose 

+   implementation uses the regular list type, 'ChurchList' abstracts 

+   over it as well. 

+  cons :: a > ChurchList a > ChurchList a 

+  cons x xs = ChurchList $ \k z > k x (runList xs k z) 

+  
+    Append two 'ChurchList's. This runs in O(1) time. Note that 

+   there is no need to materialize the lists as @[a]@. 

+  append :: ChurchList a > ChurchList a > ChurchList a 

+  append xs ys = ChurchList $ \k z > runList xs k (runList ys k z) 

+  
+   i.e., 

+  
+  nil = { fromList [] = ChurchList $ \k z > foldr k z [] 

+  = } ChurchList $ \k z > z 

+  
+  singleton x = { cons x nil = ChurchList $ \k z > k x (runList nil k z) 

+  = } ChurchList $ \k z > k x z 

+  
+  snoc xs x = { append xs $ singleton x 

+  = ChurchList $ \k z > runList xs k (runList (singleton x) k z) 

+  = } ChurchList $ \k z > runList xs k (k x z) 

+  </haskell> 

+  
+  == 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 

+  <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>) 

+  
+  <haskell>Constructor exp1 .. expk  application of the constructor</haskell> 

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

+  
+  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> 

−  == 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]. 
Latest revision as of 10:46, 29 March 2013
Contents 
[edit] 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
[edit] 2 Churchencoded Lists
Churchencoded lists use RankNTypes too, as seen in a StackOverflow answer by sacundim:
  Laws:   > runList xs cons nil == xs  > runList (fromList xs) f z == foldr f z xs  > foldr f z (toList xs) == runList xs f z newtype ChurchList a = ChurchList { runList :: forall r. (a > r > r) > r > r }   Make a 'ChurchList' out of a regular list. fromList :: [a] > ChurchList a fromList xs = ChurchList $ \k z > foldr k z xs   Turn a 'ChurchList' into a regular list. toList :: ChurchList a > [a] toList xs = runList xs (:) []   The 'ChurchList' counterpart to '(:)'. Unlike 'DList', whose  implementation uses the regular list type, 'ChurchList' abstracts  over it as well. cons :: a > ChurchList a > ChurchList a cons x xs = ChurchList $ \k z > k x (runList xs k z)   Append two 'ChurchList's. This runs in O(1) time. Note that  there is no need to materialize the lists as @[a]@. append :: ChurchList a > ChurchList a > ChurchList a append xs ys = ChurchList $ \k z > runList xs k (runList ys k z)  i.e., nil = { fromList [] = ChurchList $ \k z > foldr k z [] = } ChurchList $ \k z > z singleton x = { cons x nil = ChurchList $ \k z > k x (runList nil k z) = } ChurchList $ \k z > k x z snoc xs x = { append xs $ singleton x = ChurchList $ \k z > runList xs k (runList (singleton x) k z) = } ChurchList $ \k z > runList xs k (k x z)
[edit] 3 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
[edit] 4 See also
 RankN types on the Haskell' website.
 The GHC User's Guide on higherranked polymorphism.