The Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Ma...
summary
Proposes Simple-sub, a concrete algorithm that preserves principal types with inclusive subtyping and is implemented as Simple-sub under 500 lines (parser, simplifier, pretty-printer included). Empirically it agrees with MLsub on 1,000,000 expressions and reveals several flaws — the evaluation uncovered bugs in MLsub. Gives the actual constraints used (upper/lower bounds, union/intersection coalescing), explains how let-polymorphism and recursion are handled, and shows when simplification preserves equivalence.
AI-written summary · about
chapters (12)
- 0:00Start
- 0:34Various Forms of Subtyping
- 1:33Subtyping Examples
- 2:28Subtyping in Functional Programming
- 2:50Don't "reasonable" languages avoid subtyping?
- 3:52Traditional Hindley-Milner Type Inference: Example
- 7:36Type Inference With Subtyping: Are We Done?
- 8:39Why the equivalence?
- 10:41Simple-sub Type Inference: Example (Continued)
- 11:19Type Inference With Subtyping: Result
- 13:00Invariance: Not Actually a Problem
- 13:51Conclusions
related talks
26mThe Simple Essence of Boolean-Algebraic Subtyping: Semantic Soundness for Algebraic(…)
16mTowards Algebraic Subtyping for Extensible Records
32mMLstruct: Principal Type Inference in a Boolean Algebra of Structural Types
48mA History of Subtyping
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
20mQuickSub: Efficient Iso-Recursive Subtyping
21mPolymorphic Type Inference for Dynamic Languages
19mMutually Iso-Recursive Subtyping