Example of type in System F that is not available in Hindley Milner type inference

Question

Under 'What is Hindley Milner' it states:

Hindley-Milner is a restriction of System F, which allows more types but which requires annotations by the programmer.

My question is, What is an example of a type available in System F, that is not available in Hindley Milner (type inference)?

(The assumption being that the inference of System F types has been proven undecideable)

Answer 1

Hindley/Milner does not support higher-rank polymorphic types, i.e., types where the universal quantifier is nested into some larger type (i.e., any notion of first-class polymorphism).

One of the simplest example would be e.g.:

f : (∀α. α → α) → int × string
f id = (id 4, id "boo")

Inferring higher-rank polymorphism is known to be undecidable in general. Similar limitations apply to recursion: a recursive definition cannot have polymorphic recursive uses. For a contrived example:

g : ∀α. int × α → int
g (n,x) = if n = 0 then 0 else if odd n then g (n-1, 3) else g (n-1, "boo")

This is kind of unsurprising given the above, and the fact that a recursive definition like the above is just a shorthand for applying the higher-order Y combinator at a polymorphic type, which would again require (impredicative) first-class polymorphism.

Answer 2

Yes, System F type inference has been proven undecidable by J. B. Wells in Typability and type checking in System F are equivalent and undecidable.

H-M type system allows type quantifiers only on the top level of type expressions. More precisely, H-M distinguishes types, which can't contain quantifiers, and type schemas:

type := type variable | type → type

type schema := type | ∀α . type schema

And polymorphic expressions are typed using type schemata.

So any type that has type quantifiers inside a type expression (in particular inside the left part of →) can't be expressed in the HM type system.

One example could be typing of Church numerals. Their type in System F is ∀α.(α→α)→(α→α), and while this alone can be expressed in HM, we can't express types where a Church numeral is used as an argument. For example if define exponentiation on Church numerals

(λmn.nm) : (∀α.(α→α)→(α→α)) → (∀α.(α→α)→(α→α)) → (∀α.(α→α)→(α→α))

this type can't be expressed in the HM type system, because of the type quantifiers in the arguments.