Math 2.0

Computer science Type theory Concept

Hindley–Milner type system

Builds on Simply typed lambda calculusType inference

Summary

The Hindley–Milner type system is a typed lambda calculus with a restricted form of polymorphism. In it, a name bound by 𝗅𝖾𝗍\mathsf{let} can be used at several types. It was found by J. Roger Hindley for combinatory logic and independently by Robin Milner for the language ML. Luis Damas proved the completeness of its inference algorithm. Its key property is that type inference is decidable and every typable term has a principal type, so programs need no type annotations. It is the core of the type systems of ML, OCaml and Haskell.

Reading path

To understand this page from the ground up, read these 26 pages in order. The foundations come first.

Show the path as a graph
Element, definition, no evidence levelElementdefinitionIntuitionistic logic, concept, no evidence levelIntuitionistic logicconceptLambda calculus, concept, no evidence levelLambda calculusconceptProposition, concept, no evidence levelPropositionconceptSet, concept, no evidence levelSetconceptType system, concept, no evidence levelType systemconceptSet, definition, no evidence levelSetdefinitionConjunction, definition, no evidence levelConjunctiondefinitionDisjunction, definition, no evidence levelDisjunctiondefinitionImplication, definition, no evidence levelImplicationdefinitionNegation, definition, no evidence levelNegationdefinitionType inference, concept, no evidence levelType inferenceconceptBiconditional, definition, no evidence levelBiconditionaldefinitionTruth table, concept, no evidence levelTruth tableconceptModus ponens, concept, no evidence levelModus ponensconceptMathematical proof, concept, no evidence levelMathematical proofconceptPropositional logic, concept, no evidence levelPropositional logicconceptTautology, definition, no evidence levelTautologydefinitionLogical equivalence, definition, no evidence levelLogical equivalencedefinitionDouble negation law, statement, no evidence levelDouble negation lawstatementProof by contradiction, concept, no evidence levelProof by contradictionconceptRussell's paradox, statement, no evidence levelRussell's paradoxstatementType theory, concept, no evidence levelType theoryconceptCurry–Howard correspondence, concept, no evidence levelCurry–Howard correspo…conceptSimply typed lambda calculus, concept, no evidence levelSimply typed lambda c…conceptHindley–Milner type system, concept, no evidence levelHindley–Milner type s…concept
Each page uses the pages above it. The colour of the bar on a box shows how strong the evidence is, and the box also gives it as text. The list has the same pages.
  • no evidence level
  1. Element definition
  2. Intuitionistic logic concept
  3. Lambda calculus concept
  4. Proposition concept
  5. Set concept
  6. Type system concept
  7. Set definition
  8. Conjunction definition
  9. Disjunction definition
  10. Implication definition
  11. Negation definition
  12. Type inference concept
  13. Biconditional definition
  14. Truth table concept
  15. Modus ponens concept
  16. Mathematical proof concept
  17. Propositional logic concept
  18. Tautology definition
  19. Logical equivalence definition
  20. Double negation law statement
  21. Proof by contradiction concept
  22. Russell's paradox statement
  23. Type theory concept
  24. Curry–Howard correspondence concept
  25. Simply typed lambda calculus concept
  26. Hindley–Milner type system concept

Further reading

  1. Web https://en.wikipedia.org/wiki/Hindley–Milner_type_system
About this page
Tag703R12KENG
URIm2://703R12KENG
Kindconcept
WritingW0 stub
MSC68N18, 68N15, 03B40
UsesSimply typed lambda calculus, Type inference
Same as
Changed3 November 2026

Markdown · JSON · Edit on GitHub

What this page needs for W1

  • an inventory row: the row of the inventory that the node accounts for (0 of 1)
  • a source with a locator (0 of 1)

The writing levels say how complete the text of a page is. They do not measure its truth.

What links here

Definitions