Difference between revisions of "Rank-N types"
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 |
||
| − | As best as I can tell, rank-N types are exactly like [[existential type]]s - except that they're completely different. |
||
| + | |||
| + | <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>. |
||
| − | Rank-2 types are a special case of rank-N types, and normal Haskell 98 types are all rank-1 types. |
||
== Also see == |
== Also see == |
||
Revision as of 12:48, 26 August 2007
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 foralls 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 #-}.
Also see
Rank-N types on the Haskell' website.