ML-style polymorphic type systems have all quantifiers at the start of the type. For example, when in Haskell we write
map :: (a -> b) -> [a] -> [b]
then this type is understood to be forall a. forall b. (a -> b) -> [a] -> [b]
. As a result, the type variables a
and b
must be instantiated exactly once in the body of the function.
This becomes a problem if we want to, say, use a higher-order argument twice in a function body, instantiated at different types. For example, suppose we define
g :: a -> Integer
g x = 1
This function completely ignores its argument, and returns the integer 1
. Thus, we expect to be able to write a function
f :: (a -> Integer) -> Integer
f h = h 0 + h "lol"
Moreover, we expect that f g
would output 2
.
Unfortunately, the restriction to rank-1 functions means that the type we gave above to f
expands to
f :: forall a. (a -> Integer) -> Integer
Thus, as soon as h
is bound for the first time, its type is determined: it can either be Integer
, or it can be String
- but not both. As a result, the body of f
does not type check.
What we really would like is that the type of f
be
f :: (forall a. a -> Integer) -> Integer
If the scope of forall
was in fact this higher-order argument, we would be able to instantiate it twice: once with Integer
, and once with String
.
This type for f
, in which the forall
quantifier does not occur at the very start of the type, is a rank-2 polymorphic function. The deeper the occurrences of forall
are nested, the higher the rank of the polymorphism.
Haskell allows the above definition of f
with the Rank2Types
or the RankNTypes
extensions.
Such functions are allowed by System F, but not by polymorphism of the ML variety. The price to pay is that type inference is no longer decidable.
The motivating example comes from a StackOverflow question.
There is a Haskell wiki page on Rank-N types.
There is also a Haskell' wiki page.