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

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

View edit of May 26, 2010 or FindPage with title or text search