Hindley Milner Type Inference

TypeInference using the classical HindleyMilner algorithm or an extension thereof. Commonly used by StaticallyTyped FunctionalProgrammingLanguages like Haskell [HaskellLanguage] or ML [MlLanguage]. Languages with a Hindley-Milner type system have the important property that one can assign to every expression a unique "most general" type, the PrincipalType?.

It is frustratingly easy to extend a given type system in a way that makes type inference undecidable or ambiguous; HindleyMilnerTypeInference, by contrast, is provably decideable. It is guaranteed to complete its type inference proof in finite (and pragmatically fast) time, making it suitable for use in a practical language interpreter/compiler.

This algorithm is also known as the DamasMilner? algorithm. (LuisDamas? proved the completeness of the algorithm and the fact that the algorithm does in fact compute PrincipalType?s. He was RobinMilner's PhD student.) RogerHindley? himself attributes the algorithm to HaskellCurry (see http://www.cis.upenn.edu/~bcpierce/types/archives/1988/msg00042.html).

Description of algorithm http://www.ii.uib.no/~bezem/I121/week17.pdf (This link is broken, is there another? AnswerMe http://web.archive.org/web/20050327171418/http://www.ii.uib.no/~bezem/I121/week17.pdf works)

Behavior on programs with type errors can be unpredicatable, and often announcing type errors only toward end of program unifying substitutions can find type errors earlier: http://www.lfcs.inf.ed.ac.uk/reports/98/ECS-LFCS-98-384/

A paper on improving type error reporting http://www3.oup.co.uk/computer_journal/hdb/Volume_45/Issue_04/450436.sgm.abs.html

Locating the Source of Type Errors http://www.cs.kent.ac.uk/people/staff/oc/Talks/kent2003.pdf

On relaxing type constraints from equations X = Y to inclusions X Y http://citeseer.ist.psu.edu/aiken93type.html

Constrained type inference is strictly more general than Hindley Milner type inferenc. "Subtyping Constrained Types" http://citeseer.ist.psu.edu/trifonov96subtyping.html

2003 Interview with Robin Milner http://nick.dcs.qmul.ac.uk/~martinb/interviews/milner/

archive.org mirrors of interview http://web.archive.org/web/20031203011108/http://nick.dcs.qmul.ac.uk/~martinb/interviews/milner/

http://web.archive.org/web/20040203154611/http://nick.dcs.qmul.ac.uk/~martinb/interviews/milner/

discussion of interview on Lambda the Ultimate http://lambda-the-ultimate.org/classic/message10126.html

short blog discussion thereof http://www.kimbly.com/blog/000283.html

slashdot article/discussion on interview; links to e.g. Coq, ProofCarryingCode... http://science.slashdot.org/article.pl?sid=03/11/26/186240

In the category of seriously geeky entertainment, there's now an amusing T-Shirt: http://www.cafeshops.com/skicalc

"What part of [the HM type inferencing algorithm] don't you understand?"

Is there any reason why the Hindley-Milner type system is only used in functional languages? Can it not be applied to languages without ReferentialTransparency?

MuAnswer, the Hindley-Milner type system is not at all only used in functional languages.

Can you give examples of imperative languages that use H-M type inference? What about languages with runtime polymorphism?

ObjectiveCaml has both.

CategoryLanguageTyping CategoryLanguageFeature