TypeInference using the classical HindleyMilner algorithm or an extension thereof. Commonly used by StaticallyTyped FunctionalProgrammingLanguage''''''s 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