Hindley-Milner type system

The Hindley-Milner type system, also known as Damas-Milner or Damas-Hindley-Milner, is a classical type system for the lambda calculus with parametric polymorphism. Its more notable properties are its completeness and its ability to infer the most general type of a given program without programmer-supplied type annotations or other hints, which makes it core to the type systems of many functional programming languages. The origin of the method is the type inference algorithm for the simply typed lambda calculus devised by Haskell Curry and Robert Feys in 1958. In 1969 J. Roger Hindley extended that work and proved that the algorithm always inferred the most general type. In 1978 Robin Milner, independently of Hindley, provided an equivalent algorithm, Algorithm W, and in 1982 Luis Damas proved Milner's algorithm complete and extended it to support systems with polymorphic references. HM was first implemented as part of the type system of the ML programming language and has since been extended in various ways, most notably with type class constraints like those in Haskell.