Mutually Iso-Recursive Subtyping - OOPSLA 2023

Explore a foundational core calculus of iso-recursive types with declared subtyping in this conference talk from OOPSLA2 2023. Delve into the challenges of expressing mutual recursion and non-uniform recursion efficiently with iso-recursive types, particularly when combined with subtyping. Learn how the presented calculus overcomes limitations of the classic "Amber" rule, allowing for both inter- and intra-recursion subtyping without quadratic size encodings. Discover a syntactic fragment of the calculus that enables more efficient type checking without deep substitutions, resembling nominal subtype systems without requiring nominal semantics. Understand the potential applications of this approach, including its use as a basis for extending WebAssembly with recursive types. Gain insights into type systems, recursive types, subtyping, and higher-order subtyping from independent researcher Andreas Rossberg's presentation.