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?
Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It only takes a minute to sign up.
Sign up to join this communityHindley-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?
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.