# Higher-Rank Polymorphism

• Polymorphic type systems in functional programming languages have quantifiers in type signatures at the start of the type
• In the example:
map :: (a -> b) -> [a] -> [b]

the type signature is understood as: forall a. forall b. (a -> b) -> [a] -> [b]

• Therefor, the type variables a and b must be instantiated exactly once in the body of the function
• If we consider the following function:
g :: a -> Int
g x = 1
• g ignores its argument and always returns 1
• If now imagine to write
f :: (a -> Int) -> Int
f h = h 0 + h "hello world"

one would think f g would result in 2

• BUT, since polymorphism is restricted to rank-1 the type signature of f actually expands to forall a. (a -> Int) -> Int
• Hence, as soon as h is bound for the first time, its type is either Int OR String but never both
• So f does not type check
• So the type signature of f would need to be (forall a. a -> Int) -> Int to make this work
• For this, the scope of forall would need to be of higher-order to be able to instantiate it twice
• This type for f, where the quantifier does not occur at the very beginning of its type, is what we call a rank-2 polymorphic function
• Ranks increase the more nested the quantifiers are
• Such functions are allowed in System F but not in Haskell or ML