# Rank-N types

### From HaskellWiki

(Encoding of existentials in terms of higher rank types) |
Benmachine (Talk | contribs) |
||

Line 4: | Line 4: | ||

Normal Haskell '98 types are considered Rank-1 types. A Haskell '98 type signature such as | 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: | 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> | |

− | <hask>forall</hask> can be floated out of the right-hand side of <hask> | + | |

− | + | ||

− | < | + | |

− | + | ||

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

Line 33: | Line 27: | ||

In general, you can replace | 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 | 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://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 01:03, 6 September 2012

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

## 3 See also

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