# Rank-N types

### From HaskellWiki

(Difference between revisions)

m (+category) |
(a real description of rank n types) |
||

Line 4: | Line 4: | ||

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

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

+ | |||

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

+ | |||

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

+ | |||

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

+ | |||

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

+ | |||

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

+ | |||

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

+ | |||

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

− | |||

== Also see == | == Also see == | ||

[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. |

## Revision as of 12:48, 26 August 2007

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

(->)

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

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

However, aforall

(->)

forall

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

forall

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

{-# LANGUAGE RankNTypes #-}

## 2 Also see

Rank-N types on the Haskell' website.