Let Generalization, Polymorphic Recursion, and Variable Minimization in Boolean-Kinded(…)
summary
Claims practical procedures for equational generalization in arbitrary Boolean rings and for boolean semi-unification decidable via Baz’s method, enabling local let generalization and polymorphic recursion in Boolean-kinded Hindley‑Milner. Methods minimize bound Boolean type variables by computing pairwise one‑minimizers and iterating to a full minimizer, keeping inferred nullable‑reference types compact. Ships a reference ML dialect and an Okamel implementation with artifacts on Zenodo (doi:10.5281/zenodo.17346848) and paper DOI 10.1145/3776644.
AI-written summary · about
chapters (11)
- 0:00Boolean-kinded type systems intro
- 1:46Nullable references and coalescing
- 3:09Tracking properties with boolean kinds
- 4:13Generalization and polymorphic recursion
- 7:42Eliminators and rank-zero reduction
- 9:30Levvenheim’s method for self-match
- 11:16Polymorphic recursion in types
- 13:43Boolean semi-unification and Baz’s method
- 16:51Variable minimization in inference
- 19:17Implementation and future apps
- 20:18Summary and Q&A
related talks
18mFast and Efficient Boolean Unification for Hindley-Milner-Style Type and Effect...
16mPolymorphic Types and Effects with Boolean Unification
59mUnification Modulo Equational Theories in Languages with Binding Operators
24mAll for one and none forall: Compiling polymorphic relations without(…)
21mOmnidirectional type inference for ML
23mBetter Defunctionalization through Lambda Set Specialization
28mTowards Light-Weight Operational Reasoning for Languages with Binders, Categorically
15mQualified Types with Boolean Algebras