Omnidirectional type inference for ML
summary
Proposes omnidirectional type inference: constraints can suspend on unification variables and resume when shape information arrives via suspended match constraints, restoring principality for ML extensions. Introduces partial generalization and incremental instantiation so let‑bindings can be generalized and later refined without backtracking. Implements an efficient solver using levels, union‑find and waitlists, demonstrates principal inference for OCaml features (static record/constructor overloading and semi‑explicit first‑class polymorphism), and reports no regressions on existing checked code though benchmarks are pending.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 1:25Bidirectional typing limitations
- 4:59Constraint-based typing
- 6:26Omnidirectional type inference
- 8:11Implementing omnidirectionality
- 8:31Lambda calculus implementation
- 9:11Let polymorphism scaling
- 14:32Summary
- 15:35Q&A: Higher rank polymorphism
- 16:17Q&A: Efficiency benchmarks
- 17:26Q&A: Okamel integration
- 18:57Q&A: Formal expressivity
- 20:09Q&A: Functional logic programming
related talks
21mPolymorphic Type Inference for Dynamic Languages
32mMLstruct: Principal Type Inference in a Boolean Algebra of Structural Types
23mA Type Inferencer for ML in 200 Lines of Scala
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
30mDotty and types: the story so far
39mEverything You Always Wanted to Know About Type Inference
20mPrincipal Type Inference under a Prefix: A Fresh Look at Static Overloading
15mA compilation method for dynamic typing in ML