What does Hindely-Milner refer to?

  1. In Types and Programming Languages by Pierce, I only find that Section 22.4 Unification mentions "Hindley" and "Milner", when introducing the unification algorithm.

    Does Hindley-Milner refer to the unification algorithm for type reconstruction/inference?

  2. https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system refers to Hindley-Milner as a type system.

    Where does Types and Programming Languages by Pierce define Hindley-Milner as a typing system?

    Is a Hindley-Milner type system the same one which I heard:

    Hindley-Milner is a special and restricted form of parametric polymorphism, in that it only allows to appear at the beginning of a type. That is, you cannot have types like ∀α.(∀β.β→β)→α.


  3. What is the relation between Hindley-Milner as a type reconstruction/inference algorithm and as a type system?

    Does the unification algorithm by Hindley and Milner apply only to the Hindley-Milner type system?

    Does type reconstruction/inference (what I saw in Ch22 Type Reconstruction in Pierce's book) only apply to polymorphic systems, not to monomorphic systems?

    Section 22.2 defines type reconstruction/inference as:

    "Is some substitution instance of t well typed?” That is, can we find a type substitition σ such that σΓ |- σt : T for some T?

    Looking for valid instantiations of type variables leads to the idea of type reconstruction (sometimes called type inference),

    The footnote of Ch22 on p317 says

    The system studied in this chapter is the simply typed lambda-calculus (Figure 9-1) with booleans (8-1), numbers (8-2), and an infinite collection of base types (11-1). The corresponding OCaml implementations are recon and fullrecon.

    Does that imply that type reconstruction/inference only apply to polymorphic systems or also to monomorphic systems?


Also appreciate if you could consider What is "Hindley-Milner (i.e., unification-based) polymorphism"?