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

References