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?
$\begingroup$
$\endgroup$
-
6$\begingroup$ 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. $\endgroup$ – Martin Berger Dec 20 '17 at 20:59
-
1$\begingroup$ @MartinBerger As far as I understand, HM system allows only rank-1 polymorphism. Is it the only restriction? $\endgroup$ – uhbif19 Dec 20 '17 at 22:53
$\begingroup$
$\endgroup$
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.
-
1$\begingroup$ Welcome Martin! You can use LaTeX as usual in your answers. $\endgroup$ – Andrej Bauer Dec 22 '17 at 10:54
