The Simple Essence of Boolean-Algebraic Subtyping: Semantic Soundness for Algebraic(…)
summary
Distills BAS to five families of characteristic Boolean homomorphisms and uses them to give a direct semantic soundness proof that subtyping never equates incompatible constructors; derives a new (implemented) subtyping decision procedure that avoids some prior inefficiencies but remains worst-case exponential; proves the subtyping problem co-NP-hard even without recursive types; shows BAS can encode field removal and thus support extensible records with one term form and one typing rule without changing subtyping.
AI-written summary · about
chapters (7)
- 0:00Boolean-Algebraic subtyping intro
- 1:27Unions/intersections over functions
- 3:33Soundness challenges
- 14:15Semantic proof via homomorphisms
- 21:59Homomorphisms and subtyping algorithm
- 23:23Conclusion and future work
- 24:29Q&A on unions/intersections
related talks
15mThe Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Ma...
48mA History of Subtyping
15mQualified Types with Boolean Algebras
16mTowards Algebraic Subtyping for Extensible Records
14mAdequacy for Algebraic Effects Revisited
19mMutually Iso-Recursive Subtyping
12mContextual Algebraic Theories: Generic Boilerplate beyond Abstraction
32mMLstruct: Principal Type Inference in a Boolean Algebra of Structural Types