# Rank-N types

### From HaskellWiki

m (+category) |
(→About: add new subsection on Church-encoded Lists, link/attribute to SO answer by sacundim) |
||

(7 intermediate revisions by 4 users not shown) | |||

Line 3: | Line 3: | ||

== About == | == About == | ||

− | + | Normal Haskell '98 types are considered Rank-1 types. A Haskell '98 type signature such as | |

+ | <haskell>a -> b -> a</haskell> | ||

+ | implies that the type variables are universally quantified like so: | ||

+ | <haskell>forall a b. a -> b -> a</haskell> | ||

+ | <hask>forall</hask> can be floated out of the right-hand side of <hask>-></hask> if it appears there, so: | ||

+ | <haskell>forall a. a -> (forall b. b -> a)</haskell> | ||

+ | is also a Rank-1 type because it is equivalent to the previous signature. | ||

− | + | However, a <hask>forall</hask> appearing within the left-hand side of <hask>(->)</hask> cannot be moved up, and therefore forms another level or rank. The type is labeled "Rank-N" where N is the number of <hask>forall</hask>s which are nested and cannot be merged with a previous one. For example: | |

− | + | <hask>(forall a. a -> a) -> (forall b. b -> b)</hask> | |

− | [http://hackage.haskell.org/trac/haskell-prime/wiki/RankNTypes Rank-N types] on the Haskell' website. | + | is a Rank-2 type because the latter <hask>forall</hask> can be moved to the start but the former one cannot. Therefore, there are two levels of universal quantification. |

+ | |||

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

+ | <hask>{-# LANGUAGE Rank2Types #-}</hask> or <hask>{-# LANGUAGE RankNTypes #-}</hask>. | ||

+ | |||

+ | == Church-encoded Lists == | ||

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

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

+ | |||

+ | == See also == | ||

+ | |||

+ | * [http://hackage.haskell.org/trac/haskell-prime/wiki/RankNTypes Rank-N types] on the Haskell' website. | ||

+ | * [http://www.haskell.org/ghc/docs/latest/html/users_guide/other-type-extensions.html#universal-quantification The GHC User's Guide on higher-ranked polymorphism]. |

## Revision as of 10:46, 29 March 2013

## Contents |

## 1 About

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, aRank-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 Church-encoded Lists

Church-encoded 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)

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

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

## 4 See also

- Rank-N types on the Haskell' website.
- The GHC User's Guide on higher-ranked polymorphism.