Difference between revisions of "RankN types"
Benmachine (talk  contribs) 
(fix another ghc users guide link) 

(10 intermediate revisions by 6 users not shown)  
Line 1:  Line 1:  
[[Category:Language extensions]] 
[[Category:Language extensions]] 

+  
+  {{GHCUsersGuideexts/rank_polymorphisman Arbitrary Rank Polymorphism section}} 

== About == 
== About == 

Line 21:  Line 23:  
Rank2 or RankN types may be specifically enabled by the language extensions 
Rank2 or RankN types may be specifically enabled by the language extensions 

<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 == 
== Relation to Existentials == 

Line 44:  Line 89:  
== See also == 
== See also == 

−  +  * [https://gitlab.haskell.org/haskell/prime//wikis/RankNTypes RankN types] on the [[Haskell']] website. 

−  +  * {{GHCUsersGuideexts/rank_polymorphisma section on Arbitrary Rank Polymorphism}} 
Latest revision as of 23:27, 24 July 2021
The GHC Users Guide has an Arbitrary Rank Polymorphism section.
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 #}
.
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)
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 Users Guide has a section on Arbitrary Rank Polymorphism.