Mutually Iso-Recursive Subtyping
summary
Shows the classic Amber rule forces an exponential encoding for mutually recursive iso-recursive types and instead defines a core calculus with declared upper bounds on mu that expresses inter- and intra-recursion subtyping (including higher- and mixed-kinded constructors) without blowup. Proves soundness and decidability, identifies a shallow-substitution fragment that avoids deep β-substitutions so subtype checks stay efficient, and reports this fragment underpins the proposed WebAssembly recursive-type/GC extension.
AI-written summary · about
chapters (11)
- 0:00Mutually iso-recursive subtyping intro
- 1:25Equi- vs iso-recursive types
- 3:54Mutual recursion challenges
- 6:46Higher-kinded types limits
- 7:29Subtyping in recursive systems
- 10:59Bounds for recursive types
- 13:09Bounded recursive types example
- 14:56Higher-order subtyping extension
- 15:58Efficient subtype checks fragment
- 17:00Structural vs nominal-like behavior
- 17:27Summary & Q&A
related talks
13mRevisiting Iso-Recursive Subtyping
20mQuickSub: Efficient Iso-Recursive Subtyping
48mA History of Subtyping
15mLiberating Merges via Apartness and Guarded Subtyping
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
15mThe Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Ma...
26mThe Simple Essence of Boolean-Algebraic Subtyping: Semantic Soundness for Algebraic(…)
21mPolymorphic Type Inference for Dynamic Languages