-1
$\begingroup$

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?

$\endgroup$
2
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.