Skip to content

References — Chapter 7 · Type Inference

Every source this chapter cites, grouped by kind. Lessons cite entries inline as [KEY]; each entry says why and when to read it. Core reading marks the entries the chapter assumes you will open.

Foundational and research papers

  • [DK13] Jana Dunfield and Neelakantan R. Krishnaswami. Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism. ICFP 2013, Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming, 429–442, 2013. doi:10.1145/2500365.2500582
    Why and when: The shortest complete algorithm for predicative higher-rank types (Theorem 7.8.5), with an ordered context of existential variables. Read §3–5 after Lesson 7.8.
    Cited in: 08-higher-rank-and-impredicativity

  • [DM82] Luis Damas and Robin Milner. Principal Type-Schemes for Functional Programs. POPL 1982, 9th ACM Symposium on Principles of Programming Languages, 207–212, 1982. doi:10.1145/582153.582176
    Why and when: Core reading. The declarative HM rules (Definition 7.2.4) and the statements of soundness and completeness of W (Theorem 7.2.11). Six pages; read all of it after Lesson 7.2 §4.
    Cited in: overview, 02-hindley-milner

  • [Gar04] Jacques Garrigue. Relaxing the Value Restriction. FLOPS 2004, Functional and Logic Programming, LNCS 2998, 196–213, 2004.
    Why and when: OCaml's relaxed value restriction (generalize covariant variables of expansive expressions). Read after Lesson 7.3 §6 to understand OCaml's '_weak variables.
    Note: Springer LNCS 2998; the author's copy is on his Nagoya University home page.
    Cited in: overview, 03-generalization-and-complexity

  • [HHPW96] Cordelia V. Hall, Kevin Hammond, Simon L. Peyton Jones, and Philip L. Wadler. Type Classes in Haskell. ACM Transactions on Programming Languages and Systems 18(2), 109–138, 1996. doi:10.1145/227699.227700
    Why and when: The complete static semantics of Haskell's classes and their dictionary translation, the reference for Theorem 7.7.9. Read §3–5 after Lesson 7.7 §2.
    Cited in: 07-type-classes-and-traits

  • [Hin69] J. Roger Hindley. The Principal Type-Scheme of an Object in Combinatory Logic. Transactions of the American Mathematical Society 146, 29–60, 1969.
    Why and when: The first principal-type theorem, for combinatory logic, which Milner's work rediscovered for ML. Historical background for Lesson 7.2 §1; skim the introduction.
    Note: Available through JSTOR and the AMS journal archive.
    Cited in: 01-unification, 02-hindley-milner

  • [HW04] Christian Haack and J. B. Wells. Type Error Slicing in Implicitly Typed Higher-Order Languages. Science of Computer Programming 50(1–3), 189–224, 2004.
    Why and when: Error slices as minimal unsatisfiable constraint sets (Definition 7.9.2). Read §1–4 after Lesson 7.9 §2.
    Note: Science of Computer Programming (Elsevier), volume 50; an ESOP 2003 version exists.
    Cited in: 09-error-localization

  • [KTU90] A. J. Kfoury, J. Tiuryn, and P. Urzyczyn. ML Typability is DEXPTIME-Complete. CAAP '90, 15th Colloquium on Trees in Algebra and Programming, LNCS 431, 206–220, 1990.
    Why and when: The independent proof of the same bound as [Mai90], by a different encoding. Consult it if Mairson's construction is hard to follow.
    Note: Springer LNCS 431.
    Cited in: 02-hindley-milner, 03-generalization-and-complexity

  • [LY98] Oukseh Lee and Kwangkeun Yi. Proofs about a Folklore Let-Polymorphic Type Inference Algorithm. ACM Transactions on Programming Languages and Systems 20(4), 707–723, 1998. doi:10.1145/291891.291892
    Why and when: Algorithm M (Algorithm 7.2.9): top-down inference, proved sound and complete, and shown to fail earlier than W. Read §2–4 after Lesson 7.2 §3; the lab's L3 is this algorithm.
    Cited in: 02-hindley-milner, 09-error-localization

  • [Mai90] Harry G. Mairson. Deciding ML Typability is Complete for Deterministic Exponential Time. POPL 1990, 17th ACM Symposium on Principles of Programming Languages, 382–401, 1990. doi:10.1145/96709.96748
    Why and when: The DEXPTIME lower bound of Theorem 7.3.11 by simulating Turing machines with nested lets. Read §1–2 for the type-doubling construction; the full encoding is optional.
    Cited in: 02-hindley-milner, 03-generalization-and-complexity

  • [McA03] David McAllester. A Logical Algorithm for ML Type Inference. RTA 2003, Rewriting Techniques and Applications, LNCS 2706, 436–451, 2003.
    Why and when: Why ML inference is fast in practice: nearly linear time when let-depth and type size are bounded (Lesson 7.3 §5). Read the introduction and the main theorem.
    Note: Springer LNCS 2706.
    Cited in: overview, 03-generalization-and-complexity

  • [McA98] Bruce J. McAdam. On the Unification of Substitutions in Type Inference. IFL '98, Implementation of Functional Languages, LNCS 1595, 137–152, 1998.
    Why and when: The left-to-right bias of W's error reports and a symmetric alternative (Lesson 7.9). Read §1–3.
    Note: Springer LNCS 1595; also an Edinburgh technical report.
    Cited in: 09-error-localization

  • [Mil78] Robin Milner. A Theory of Type Polymorphism in Programming. Journal of Computer and System Sciences 17(3), 348–375, 1978. doi:10.1016/0022-0000(78)90014-4
    Why and when: Core reading. The origin of let-polymorphism, Algorithm W and Algorithm J (§4). Read §3–4 after Lesson 7.2 §2; the J presentation is what every production ML checker descends from.
    Cited in: overview, 01-unification, 02-hindley-milner, 04-constraint-based-inference

  • [MM82] Alberto Martelli and Ugo Montanari. An Efficient Unification Algorithm. ACM Transactions on Programming Languages and Systems 4(2), 258–282, 1982. doi:10.1145/357162.357169
    Why and when: Core reading. Unification as rewriting a set of equations to solved form (Algorithm 7.1.8) and the termination measure of Theorem 7.1.15. Read §2 after Lesson 7.1 §4; §3–5 develop the efficient multi-equation algorithm mentioned in §6.
    Cited in: overview, 01-unification

  • [OL96] Martin Odersky and Konstantin Läufer. Putting Type Annotations to Work. POPL 1996, 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 54–67, 1996. doi:10.1145/237721.237729
    Why and when: Rank-N polymorphism with annotations on top of HM (Lesson 7.8 §1). Read §1–3.
    Cited in: 08-higher-rank-and-impredicativity

  • [OSW99] Martin Odersky, Martin Sulzmann, and Martin Wehr. Type Inference with Constrained Types. Theory and Practice of Object Systems 5(1), 35–55, 1999.
    Why and when: Core reading. HM(X): Hindley–Milner parameterized by a constraint system, with soundness for every X and principal types when X has principal solutions (Theorems 7.4.7, 7.4.9). Read §2–5 after Lesson 7.4 §2.
    Note: Wiley journal TAPOS 5(1); preprints circulate from the authors' pages.
    Cited in: 04-constraint-based-inference

  • [PJVWS07] Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark Shields. Practical Type Inference for Arbitrary-Rank Types. Journal of Functional Programming 17(1), 1–82, 2007. doi:10.1017/S0956796806006034
    Why and when: GHC's RankNTypes: bidirectional checking, subsumption and skolemization, with a complete implementation in the appendix (Lesson 7.8). Read §1–6.
    Cited in: 08-higher-rank-and-impredicativity

  • [PKW14] Zvonimir Pavlinovic, Tim King, and Thomas Wies. Finding Minimum Type Error Sources. OOPSLA 2014, ACM International Conference on Object-Oriented Programming, Systems, Languages & Applications, 525–542, 2014. doi:10.1145/2660193.2660230
    Why and when: Minimum error sources computed with a MaxSMT solver, with timings on OCaml programs (Lesson 7.9 §5). Read §1–4.
    Cited in: overview, 09-error-localization

  • [PW78] Michael S. Paterson and Mark N. Wegman. Linear Unification. Journal of Computer and System Sciences 16(2), 158–167, 1978.
    Why and when: The strictly linear-time unification algorithm of Lesson 7.1 §6. Read it after the union-find algorithm to see what the last \(\alpha(n)\) factor costs to remove.
    Note: Journal of Computer and System Sciences (Elsevier), volume 16, issue 2.
    Cited in: 01-unification

  • [Rob65] J. A. Robinson. A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM 12(1), 23–41, 1965. doi:10.1145/321250.321253
    Why and when: Core reading. The origin of unification and of the most general unifier. Read §5 (the unification algorithm and its theorem) after Lesson 7.1 §2; the resolution part is optional for this chapter.
    Cited in: 01-unification

  • [SHPJV20] Alejandro Serrano, Jurriaan Hage, Simon Peyton Jones, and Dimitrios Vytiniotis. A Quick Look at Impredicativity. Proceedings of the ACM on Programming Languages 4 (ICFP 2020), Article 89, 2020. doi:10.1145/3408971
    Why and when: Quick Look (Algorithm 7.8.4), GHC's impredicative instantiation since 9.2, with the soundness and conservativity results of Theorem 7.8.7a. Read §1–4.
    Cited in: 04-constraint-based-inference, 08-higher-rank-and-impredicativity

  • [Tar75] Robert Endre Tarjan. Efficiency of a Good But Not Linear Set Union Algorithm. Journal of the ACM 22(2), 215–225, 1975. doi:10.1145/321879.321884
    Why and when: The inverse-Ackermann bound for union by rank with path compression that Lesson 7.1 §5 uses for union-find unification. Read the statement of the main theorem; the proof is optional.
    Cited in: 01-unification

  • [Tof90] Mads Tofte. Type Inference for Polymorphic References. Information and Computation 89(1), 1–34, 1990.
    Why and when: Imperative type variables, the SML '90 solution that the value restriction replaced (Lesson 7.3 §6). Read §1–2 for the counterexample of Proposition 7.3.9.
    Note: Information and Computation (Elsevier), volume 89, issue 1.
    Cited in: 03-generalization-and-complexity

  • [VPJS10] Dimitrios Vytiniotis, Simon Peyton Jones, and Tom Schrijvers. Let Should Not Be Generalised. TLDI 2010, 5th ACM Workshop on Types in Language Design and Implementation, 39–50, 2010.
    Why and when: The argument for MonoLocalBinds (Lesson 7.2 §6, Lesson 7.4 §6), with measurements of how rarely Haskell code needs generalized local lets. Short; read after Lesson 7.4.
    Note: ACM TLDI 2010 proceedings; also on the Microsoft Research site.
    Cited in: 02-hindley-milner, 04-constraint-based-inference

  • [VPJSS11] Dimitrios Vytiniotis, Simon Peyton Jones, Tom Schrijvers, and Martin Sulzmann. OutsideIn(X): Modular Type Inference with Local Assumptions. Journal of Functional Programming 21(4–5), 333–412, 2011. doi:10.1017/S0956796811000098
    Why and when: Core reading. GHC's inference algorithm: implication constraints, touchable variables, and why guessing is forbidden (Lesson 7.4). Read §1–5; §7 is the concrete solver.
    Cited in: overview, 03-generalization-and-complexity, 04-constraint-based-inference

  • [WB89] Philip Wadler and Stephen Blott. How to Make Ad-hoc Polymorphism Less Ad Hoc. POPL 1989, 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 60–76, 1989. doi:10.1145/75277.75283
    Why and when: Core reading. The origin of type classes and of their translation to dictionary passing (Lesson 7.7). Read all of it; the translation examples are the ★ lab's L5.
    Cited in: overview, 07-type-classes-and-traits

  • [Wel99] J. B. Wells. Typability and Type Checking in System F Are Equivalent and Undecidable. Annals of Pure and Applied Logic 98(1–3), 111–156, 1999.
    Why and when: The undecidability of System F inference (Theorem 7.8.7b) by reduction from semi-unification. Read the introduction for the statement and its history.
    Note: Annals of Pure and Applied Logic (Elsevier), volume 98.
    Cited in: 08-higher-rank-and-impredicativity

  • [Wri95] Andrew K. Wright. Simple Imperative Polymorphism. Lisp and Symbolic Computation 8(4), 343–355, 1995.
    Why and when: Core reading. The value restriction (Definition 7.3.3) and its soundness argument, with the observation that it rejects few real programs. Short; read it after Lesson 7.3 §4.
    Note: Lisp and Symbolic Computation (Kluwer), volume 8, issue 4.
    Cited in: overview, 02-hindley-milner, 03-generalization-and-complexity

  • [ZM14] Danfeng Zhang and Andrew C. Myers. Toward General Diagnosis of Static Errors. POPL 2014, 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 569–581, 2014. doi:10.1145/2535838.2535870
    Why and when: SHErrLoc: likelihood-ranked error locations over a general constraint language (Lesson 7.9 §6). Read §1–3 and the evaluation.
    Cited in: 09-error-localization

Textbooks and monographs

  • [BS01] Franz Baader and Wayne Snyder. Unification Theory (chapter 8 of the Handbook of Automated Reasoning). Elsevier and MIT Press, 2001. Read: §2 (syntactic unification: substitutions, MGUs), §3 (algorithms: Robinson, Martelli–Montanari rules, the union-find algorithm and its complexity), §4–5 (E-unification).
    Why and when: The best single survey of unification: the three algorithms of Lesson 7.1 with proofs, the exponential example of §5 and the extensions of §6. Read §2–3 alongside Lesson 7.1.
    Cited in: 01-unification

  • [Jon94] Mark P. Jones. Qualified Types: Theory and Practice. Cambridge University Press, 1994. Read: Ch. 2 (predicates and entailment), Ch. 3 (type inference with qualified types), Ch. 5 (evidence and the translation to dictionaries).
    Why and when: The theory of type classes as HM with predicates, including coherence of the evidence translation. Read Ch. 3 and 5 after Lesson 7.7 §4.
    Cited in: 04-constraint-based-inference, 07-type-classes-and-traits

  • [PR05] François Pottier and Didier Rémy. The Essence of ML Type Inference (chapter 10 of Advanced Topics in Types and Programming Languages, B. C. Pierce, ed.). MIT Press, 2005. Read: §10.1 (let-polymorphism, let-expansion), §10.2–10.4 (constraints and constraint generation), §10.5–10.6 (constraint solving by rewriting, with let-constraints).
    Why and when: Core reading. The generate-then-solve presentation of HM(X) that Lesson 7.4's Algorithm 7.4.4 follows, with complete proofs. The best reading for Lessons 7.3–7.4; long but rewarding.
    Cited in: overview, 03-generalization-and-complexity, 04-constraint-based-inference

  • [TAPL] Benjamin C. Pierce. Types and Programming Languages. MIT Press, 2002. Read: Ch. 22 (type reconstruction: §22.3 constraint typing, §22.4 unification, §22.5 principal types, §22.6 implicit type annotations, §22.7 let-polymorphism and the value restriction), Ch. 23 (universal types: System F, and §23.6 on the undecidability of its inference).
    Why and when: Core reading. The textbook treatment of this chapter's core: constraint-based inference with unification and let-polymorphism. Read Ch. 22 alongside Lessons 7.1–7.3 when a proof in the lessons feels compressed.
    Cited in: overview, 02-hindley-milner, 03-generalization-and-complexity

Surveys and tutorials

  • [DK21] Jana Dunfield and Neel Krishnaswami. Bidirectional Typing. ACM Computing Surveys 54(5), Article 98, 2021. doi:10.1145/3450952
    Why and when: The survey behind Chapter 6's bidirectional checker; §7–8 cover its combination with inference and polymorphism (Lessons 7.2 §6 and 7.8).
    Cited in: 02-hindley-milner

Theses and technical reports

  • [Dam85] Luis Damas. Type Assignment in Programming Languages. PhD thesis, University of Edinburgh (report CST-33-85), 1985.
    Why and when: The full proofs of W's soundness and completeness that [DM82] only states. Consult it for the Let case of Theorem 7.2.11's proof.
    Note: Edinburgh Research Archive; scanned copies circulate under the report number CST-33-85.
    Cited in: 02-hindley-milner

  • [Hue76] Gérard Huet. Résolution d'équations dans des langages d'ordre 1, 2, …, ω. Thèse de doctorat d'État, Université Paris VII, 1976.
    Why and when: Where union-find unification over term graphs and rational-tree unification come from (Lesson 7.1, Algorithm 7.1.10 and Definition 7.1.11). Most readers should read [BS01]'s account instead; cite Huet for the origin.
    Note: Not online in a stable place; the union-find algorithm is presented in English in [BS01, §3].
    Cited in: 01-unification

  • [Rem92] Didier Rémy. Extending ML Type System with a Sorted Equational Theory. INRIA Research Report 1766, 1992.
    Why and when: Introduces the ranks (levels) of type variables that make generalization a level comparison (Algorithm 7.3.2). Read the part on efficient generalization after Lesson 7.3 §2; [Kis13] is the gentler account.
    Note: INRIA HAL repository, report RR-1766.
    Cited in: 01-unification, 02-hindley-milner, 03-generalization-and-complexity

Source code (pinned versions)

Official documentation and specifications

  • [GHC-Impred] GHC User's Guide: Impredicative polymorphism. GHC 9.4.7. link
    Why and when: What Quick Look accepts in practice (Lesson 7.8 §7).
    Cited in: 08-higher-rank-and-impredicativity

  • [GHC-RankN] GHC User's Guide: Arbitrary-rank polymorphism. GHC 9.4.7. link
    Why and when: The rules GHC applies to RankNTypes programs, including simplified subsumption (Lesson 7.8 §6).
    Cited in: 08-higher-rank-and-impredicativity

  • [KOTLIN-Builders] Kotlin documentation: Using builders with builder type inference. link
    Why and when: What builder inference accepts, with examples like buildList (Algorithm 7.6.4).
    Cited in: 06-local-and-flow-inference

  • [KOTLIN-Spec] Kotlin language specification: Type inference. link
    Why and when: Kotlin's local inference, constraint systems per call and builder inference (Lesson 7.6). Read the overview and the section on builder-style inference.
    Cited in: 06-local-and-flow-inference

  • [RFC1023] Rust RFC 1023: Rebalancing coherence. link
    Why and when: Rust's orphan rules and the reasoning for global coherence across crates (Lesson 7.7 §1, Theorem 7.7.8). Read the motivation and the "orphan rules" section.
    Cited in: 07-type-classes-and-traits

  • [RFC2451] Rust RFC 2451: Re-rebalancing coherence. link
    Why and when: The current orphan rule with "uncovered type parameters" quoted in rustc's E0117 note (Lesson 7.7 §7). Read after RFC 1023.
    Cited in: 07-type-classes-and-traits

  • [RUSTC-DevGuide] Rust Compiler Development Guide: Type inference. link
    Why and when: How rustc's inference context, snapshots and variable kinds fit together (Lesson 7.6).
    Cited in: 06-local-and-flow-inference

  • [SE0326] Swift Evolution SE-0326: Enable multi-statement closure parameter/result type inference. link
    Why and when: How Swift widened its inference scope to closure bodies without letting constraint systems grow (Lesson 7.5 §6).
    Cited in: 05-swift-constraint-solver

  • [SWIFT-TypeCheckerDoc] Swift Type Checker Design and Implementation (docs/TypeChecker.md). Swift 6.3.3 (swift-6.3.3-RELEASE). link
    Why and when: The design document of Swift's constraint-based checker: constraint kinds, disjunctions, solution ranking and default literal types (Lesson 7.5). Read "Approach", "Constraints" and "Constraint Solving".
    Cited in: overview, 05-swift-constraint-solver

  • [TS-Handbook] TypeScript Handbook: Type Inference. link
    Why and when: Best common type and contextual typing (Lesson 7.6). Short; read before the tsc box.
    Cited in: 06-local-and-flow-inference

Blog posts and articles

  • [Kis13] Oleg Kiselyov. How OCaml type checker works — or what polymorphism and garbage collection have in common. 2013. link
    Why and when: A readable walk-through of level-based generalization in OCaml's ctype.ml, from the naive algorithm to levels and lazy level adjustment. Read after Lesson 7.3 §3 (not an origin: cite [Rem92] for that).
    Cited in: 03-generalization-and-complexity