MLstruct: Principal Type Inference in a Boolean Algebra of Structural Types
summary
MLstruct claims to combine principal polymorphic inference with first-class unions, intersections and equirecursive structural types by treating type connectives as a Boolean algebra of types and adding a few sound subtyping rules. It uses nominal class tags to get extensible variants without row variables, a constraint solver that moves intersections/negations into bounds, and normal forms for termination. The implementation has a web demo, several thousand lines of tests, and a proof bundle forthcoming; complexity is high in theory but the prototype works on real examples.
AI-written summary · about
chapters (17)
- 0:00Intro
- 2:50TypeScript-style Structural Types
- 5:54Nominal Tags
- 7:45Eliminating Unions by Pattern Matching
- 10:16Unions and Open Pattern Matching (Default Cases)
- 12:00Constructor Difference as Negated Tag Intersection
- 13:06A Boolean Algebra of Structural Types
- 14:05Equirecursive Types
- 16:38Type Inference by Constraint Solving
- 18:16Main Challenges of Constraint Solving
- 19:16Solving the First Problem
- 20:27Consequences of Bending Subtyping
- 21:41Solving the Second Problem
- 22:41Other Important Concepts of MLstruct
- 24:46Implementation
- 26:14Equirecursive Type Inference
- 27:10Conclusion
related talks
15mThe Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Ma...
21mOmnidirectional type inference for ML
21mPolymorphic Type Inference for Dynamic Languages
16mPolymorphic Types and Effects with Boolean Unification
30mConstraint Typing with Boolean Algebra
20mPrincipal Type Inference under a Prefix: A Fresh Look at Static Overloading
24mUnfolding ML Datatype Declarations Without Loops
26mThe Simple Essence of Boolean-Algebraic Subtyping: Semantic Soundness for Algebraic(…)