<p>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)$. </p>

<p>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, </p>

<pre><code>let f = λ x . x in λ x . f f x
</code></pre>

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

<pre><code>(λ f . λ x. f f x) (λ x . x)
</code></pre>

<p>cannot be typed in HM, only in Sytem F.</p>

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

CC BY-SA 3.0
2017-12-22T10:54:46.480Z
Welcome Martin! You can use LaTeX as usual in your answers.
Andrej Bauer
CC BY-SA 3.0
2017-12-22T09:09:58.100Z
2017-12-22T11:08:12.053Z
2017-12-22T11:08:12.053Z
Martin Hofmann
<p>Hindley-Milner type system is some restriction of System F, which allows type inference.</p>

<p>But from simple descriptions I cannot see, what is the difference between them?</p>

CC BY-SA 3.0
2017-12-20T20:59:35.843Z
This question is more suitable for [cs.stackexchange.com](https://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.
Martin Berger
CC BY-SA 3.0
2017-12-20T22:53:11.637Z
@MartinBerger As far as I understand, HM system allows only rank-1 polymorphism. Is it the only restriction?
uhbif19
<type-theory><type-inference>
What is the difference between System F and Hindley-Milner type system?
uhbif19
# What is the difference between System F and Hindley-Milner type system?

(Asked by: username_0 on 2017-12-20)

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?

**Tags:** type-theory, type-inference

> **Comments:**
> **username_1**: This question is more suitable for [cs.stackexchange.com](https://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.  
> **username_0**: @MartinBerger As far as I understand, HM system allows only rank-1 polymorphism. Is it the only restriction?  

---

## 1 answers

### Answer by username_2 on 2017-12-22. Score: 16 | Accepted answer

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.

> **Comments:**
> **username_3**: Welcome Martin! You can use LaTeX as usual in your answers.  

---

