Difference between revisions of "Rank-N types"
(Encoding of existentials in terms of higher rank types) |
Benmachine (talk | contribs) m (→See also) |
||
| (2 intermediate revisions by the same user not shown) | |||
| 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 |
||
| ⚫ | |||
| − | |||
| ⚫ | |||
| − | |||
implies that the type variables are universally quantified like so: |
implies that the type variables are universally quantified like so: |
||
| ⚫ | |||
| − | |||
| − | <hask>forall |
+ | <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>(->)</hask> if it appears there, so: |
||
| − | |||
| ⚫ | |||
| − | |||
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 |
||
| ⚫ | |||
| + | (where <hask>e1..ek</hask> are types in terms of <hask>a1..ai</hask> and <hask>t1..tj</hask>) |
||
| ⚫ | |||
| ⚫ | |||
| − | |||
| ⚫ | |||
| − | < |
+ | <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:04, 6 September 2012
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 #-}.
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.