# Difference between revisions of "Rank-N types"

m (→See also: Update link) |
(fix link to ghc user guide) |
||

(5 intermediate revisions by 3 users not shown) | |||

Line 1: | Line 1: | ||

[[Category:Language extensions]] |
[[Category:Language extensions]] |
||

+ | |||

+ | {{GHCUsersGuide|exts/rank_polymorphism||an Arbitrary Rank Polymorphism section}} |
||

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

Line 87: | Line 89: | ||

== See also == |
== See also == |
||

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

* [https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#arbitrary-rank-polymorphism The GHC User's Guide on higher-ranked polymorphism]. |
* [https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#arbitrary-rank-polymorphism The GHC User's Guide on higher-ranked polymorphism]. |

## Latest revision as of 22:52, 12 June 2021

**The GHC Users Guide has an Arbitrary Rank Polymorphism section.**

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

can be floated out of the right-hand side of `->`

if it appears there, so:

```
forall a. a -> (forall b. b -> a)
```

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

However, a `forall`

appearing within the left-hand side of `(->)`

cannot be moved up, and therefore forms another level or rank. The type is labeled "Rank-N" 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 Rank-2 type because the latter `forall`

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
`{-# LANGUAGE Rank2Types #-}`

or `{-# LANGUAGE RankNTypes #-}`

.

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

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

(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

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