Programming Languages: Concepts and Implementation

7.13 Notes and Further Reading

The classical type inference algorithm with parametric polymorphism for the λ-calculus used in ML and Haskell is informally referred to as the Hindley–Milner type inference algorithm (HM). This algorithm is based on a type inference algorithm, developed by Haskell Curry and Robert Feys in 1958, for the simply typed λ-calculus. The simply typed λ-calculus (λ^→), introduced by Alonzo Church in 1940, is a typed interpretation of the λ-calculus with only one type constructor (i.e., →) that builds function types. The simply typed λ-calculus is the simplest (and canonical) example of a typed λ-calculus. (The λ-calculus introduced in Chapter 5 is the untyped λ-calculus.) Systems with polymorphic types, including ML and ...