Revisiting Iso-Recursive Subtyping
summary
Proposes that iso-recursive subtyping is equivalent to checking all finite n-times unfolding inclusions, and then shows an algorithmic reduction: only 1- and 2-time checks suffice, the double unfolding rule, making subtyping decidable without Amber’s messy transitivity work. Proves soundness and completeness between the declarative and algorithmic systems, proves Amber derivations embed into the new system, and ships a machine-checked Coq formalization of the metatheory and proofs.
AI-written summary · about
chapters (9)
- 0:00Start
- 0:59Recursive Types in FP
- 2:05Iso-Recursive Types
- 2:38Existing Solution: Amber rules
- 3:39Flaws of Folklore Amber Rules
- 5:17Examples of Iso-Recursive Subtyping
- 6:25Example 3: Analysis
- 10:49Two Subtyping Rules are Equivalent
- 11:06Translation from Amber
related talks
19mMutually Iso-Recursive Subtyping
20mQuickSub: Efficient Iso-Recursive Subtyping
48mA History of Subtyping
14mA Limited Case for Reification by Type Inference
29mType Checking with Rewriting Rules
19mExtensible Metatheory Mechanization via Family Polymorphism
26mThe Simple Essence of Boolean-Algebraic Subtyping: Semantic Soundness for Algebraic(…)
15mA systematic approach to "Well-founded recursion done right"