# What is “Hindley-Milner (i.e., uniﬁcation-based) polymorphism”?

In Types and Programming Languages by Pierce, Ch11 Simple Extensions extends the typed lambda calculus.

Section 11.5 Let Bindings says:

In Chapter 22 we will see another reason not to treat let as a derived form: in languages with Hindley-Milner (i.e., uniﬁcation-based) polymorphism, the let construct is treated specially by the typechecker, which uses it for generalizing polymorphic deﬁnitions to obtain typings that cannot be emulated using ordinary λ-abstraction and application.

What is "Hindley-Milner (i.e., uniﬁcation-based) polymorphism"?

• Is "Hindley-Milner (i.e., uniﬁcation-based) polymorphism" the same thing as let polymorphism?

In Ch22, I searched for "polymorphism", but only find one form of polymorphism: Section 22.7 Let Polymorphism.

• Does "Hindley-Milner (i.e., uniﬁcation-based) polymorphism" mean polytype in the Hndley-Milner type system?

Does Ch22 define or study the Hindley-Milner type system? I can't find it. In particular, does it have the polytype and monotype concepts in the Hindley-Milner type system?

Yes, in that context Hindley-Milner polymorphism is let-polymorphism, since such language uses $$\sf let$$ to introduce polymorphic functions.

In the untyped lambda calculus, we can consider a (non recursive) $${\sf let}\ x = e \ {\sf in}\ t$$ to be syntactic sugar for $$(\lambda x.t)e$$.

In System F, where polymorphism is introduced by explicit $$\Lambda \alpha$$ abstractions, we can similarly regard $$\sf let$$ as syntactic sugar.

By contrast, H-M based languages do not use $$\Lambda \alpha$$ in terms. Roughly, these languages achieve polymorphism by making $$\sf let$$ perform the wanted type generalization, as if $$\sf let$$ implicitly added the $$\Lambda \alpha$$ binders we would explicitly write in System F. This is done during type inference. For instance the H-M term

$$\begin{array}{l} {\sf let}\ f = \lambda x.\ x \\ {\sf in}\ (f\ 3, f\ {\sf true}) \end{array}$$

works similarly to the System F (-like) term

$$\begin{array}{l} {\sf let}\ f = \Lambda \alpha.\ \lambda x:\alpha.\ x \\ {\sf in}\ (f\ [{\sf int}]\ 3, f\ [{\sf bool}]\ {\sf true}) \end{array}$$

where the type of $$f$$ is $$\forall \alpha.\ \alpha$$, as wanted.