QuickSub: Efficient Iso-Recursive Subtyping
summary
QuickSub is an algorithm for iso-recursive subtyping that is equivalent to the Amber rules but avoids renaming, unfolding and backtracking by tracking polarity modes and by returning either strict-subtype or equivalence results annotated with equality-variable sets. Implementation uses mutable sets for on-the-fly updates, yielding O(nm) worst-case complexity (m = type size, n = recursive binders) yet near-linear performance in practice; Coq proofs, benchmarks against Amber/equi-recursive algorithms, and artifacts are provided.
AI-written summary · about
chapters (9)
- 0:00QuickSub introduction
- 2:07Motivation for QuickSub
- 4:35Iso-recursive subtyping challenges
- 6:22QuickSub design ideas
- 9:12Negative subtyping handling
- 11:37Implementation and complexity
- 12:42Evaluation and performance
- 15:57Conclusion and future
- 16:46Q&A
related talks
13mRevisiting Iso-Recursive Subtyping
19mMutually Iso-Recursive Subtyping
15mThe Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Ma...
48mA History of Subtyping
15mSulfur: Substitution Generation using a Logical Framework
29mUnification Modulo Isomorphisms between Dependent Types for Type-based Library Search
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
26mThe Simple Essence of Boolean-Algebraic Subtyping: Semantic Soundness for Algebraic(…)