Principal type-schemes for functional programs

✨ Summary

The paper establishes that, for the purely applicative part of ML modeled by its skeletal language, type assignment is decidable and every typable expression has a principal type-scheme: any other derivable type-scheme is a generic instance of the principal one. It formalizes polymorphic type schemes, instantiation and generalization, gives inference rules for variables, abstraction, application, and let, and presents Algorithm W. Algorithm W combines fresh type variables with Robinson’s unification algorithm to compute a most-general substitution and type. The paper proves both soundness—that inferred types are derivable—and completeness—that every derivable typing is an instance of the computed result.

The result became a foundation for Hindley–Milner-style type inference. The Haskell 2010 Report preserves the principal-type and generalization ideas in an extended Hindley–Milner system, while official OCaml documentation identifies its type inference as based on the Hindley–Milner algorithm and describes principal types as the most general inferred types. (haskell.org) Later research explicitly treats Algorithm W and Damas–Milner inference as the baseline for extensions involving overloading, subtyping, higher-rank polymorphism, and first-class polymorphism. (sciencedirect.com) The paper’s bibliographic record identifies it as a POPL ’82 conference contribution by Damas and Milner, published on January 25, 1982. (doi.org)