Hindley–Milner type system

A Hindley–Milner (HM) type system is a classical type system for the lambda calculus with parametric polymorphism. It is also known as Damas–Milner or Damas–Hindley–Milner. It was first described by J. Roger Hindley and later rediscovered by Robin Milner. Luis Damas contributed a close formal analysis and proof of the method in his PhD thesis. A Hindley–Milner (HM) type system is a classical type system for the lambda calculus with parametric polymorphism. It is also known as Damas–Milner or Damas–Hindley–Milner. It was first described by J. Roger Hindley and later rediscovered by Robin Milner. Luis Damas contributed a close formal analysis and proof of the method in his PhD thesis. Among HM's 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. Algorithm W is an efficient type inference method that performs in almost linear time with respect to the size of the source, making it practically useful to type large programs. HM is preferably used for functional languages. It was first implemented as part of the type system of the programming language ML. Since then, HM has been extended in various ways, most notably with type class constraints like those in Haskell. One and the same thing can be used for many purposes. A chair might be used to support a sitting person but also as a ladder to stand on while changing a light bulb or as a clothes valet. Beside having particular material qualities, which make a chair usable as such, it also has the particular designation for its use. When no chair is at hand, other things might be used as a seat, and so the designation of a thing can be changed as fast as one can turn an empty bottle crate upside down to change its purpose from a container to that of a support. Different uses of physically near-identical things are usually accompanied by giving those things different names to emphasize the intended purpose. Depending on the use, seamen have a dozen or more words for a rope though it might materially be the same thing. The same in everyday language, where a leash indicates a use different to a line. In computer science, this practice of naming things by its intended use is put to an extreme called typing and the names or expressions called types: