What is “Hindley-Milner (i.e., unification-based) polymorphism”?

Question

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., unification-based) polymorphism, the let construct is treated specially by the typechecker, which uses it for generalizing polymorphic definitions to obtain typings that cannot be emulated using ordinary λ-abstraction and application.

What is "Hindley-Milner (i.e., unification-based) polymorphism"?

• Is "Hindley-Milner (i.e., unification-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., unification-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?

Answer 1

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.