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?