Rank-N types
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 #-}
.
Also see
Rank-N types on the Haskell' website.