# What is the difference between System F and Hindley-Milner type system?

Hindley-Milner type system is some restriction of System F, which allows type inference.

But from simple descriptions I cannot see, what is the difference between them?

• This question is more suitable for cs.stackexchange.com. If you want to understand the relationship between F and HM, I suggest to pay close attention to where $\forall$ quantifiers can occur in types. Commented Dec 20, 2017 at 20:59
• @MartinBerger As far as I understand, HM system allows only rank-1 polymorphism. Is it the only restriction? Commented Dec 20, 2017 at 22:53

Yes, In Hindley-Milner universal quantifiers are allowed only at the outside of a type (and therefore omitted). For example, in HM you can have the type $\forall \alpha.(\alpha\to\alpha) \to (\alpha\to\alpha)$ usually abbreviated as $(\alpha\to\alpha)\to(\alpha\to\alpha)$, but you cannot have $(\forall \alpha.\alpha\to\alpha) \to (\forall \alpha.\alpha\to\alpha)$.

A special feature of HM (that does not make sense for system F) is the distinction between let-bindings and beta reducts. In a let-binding the type of the bound variable may be polymorphic in the sense that its free type variables are quantified separately. For example,

let f = λ x . x in λ x . f f x


can be typed in HM and in system F (by giving f the polymorphic type $\forall \alpha.\alpha\rightarrow\alpha$), but

(λ f . λ x. f f x) (λ x . x)


cannot be typed in HM, only in Sytem F.

The advantage of these restrictions is that type inference for HM is decidable and rather efficiently so whereas it is undecidable for F.

• Welcome Martin! You can use LaTeX as usual in your answers. Commented Dec 22, 2017 at 10:54