Invited Talk: Type inference in OCaml and GHC using Levels
summary
Claim: both OCaml and GHC implement let-generalization using lexical levels on types or levels on variables, and those levels also power other checks (escape, constructor disambiguation, principal-mode warnings). OCaml keeps mutable levels on type graphs and represents "generic" as infinity (practically 100_000_000), eagerly unifies, and uses instance to copy-and-lower types; GHC stores TCLevel on type variables (adds an Infinity constructor), delays unification into the constraint solver when needed, and enforces the rule: generalize, promote, or error.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:03Talk format and levels overview
- 9:58Motivating example
- 15:58Levels in type inference
- 24:48Levels in OCaml compiler
- 33:34Generalization in OCaml
- 40:29Unification in OCaml
- 47:11Levels in GHC compiler
- 53:54Generalization in GHC
- 58:06Conclusion
related talks
26mAn Invitation to OCaml
41mThe Dialectics of Type-Level Programming
20mInteractive Haskell Type Inference Exploration (Extended Abstract)
38mWhat Haskell Taught Us When We Weren't Looking
15mLogic Programming with Extensible Types (Lightning talk)
31mTotal Type Classes
36mGoing Higher
01h 18mA Tale of Two Lambdas: A Haskeller's Journey into OCaml