Iso-recursive types are often taken as a type-theoretic model for type recursion as present in many programming languages,
e.g., classes in object-oriented languages or algebraic datatypes in functional languages. Their main advantage over an equi-recursive semantics is that they are simpler and algorithmically less expensive, which is an important consideration when the cost of type checking matters, such as for intermediate or low-level code representations, virtual machines, or runtime casts. However, a closer look reveals that iso-recursion cannot, in its standard form, efficiently express essential type system features like mutual recursion or non-uniform recursion. While it has been folklore that mutual recursion and non-uniform type parameterisation can nicely be handled by generalising to higher kinds, this encoding breaks down when combined with subtyping: the classic ``Amber'' rule for subtyping iso-recursive types is too weak to express mutual recursion without falling back to encodings of quadratic size.
We present a foundational core calculus of iso-recursive types with \emph{declared} subtyping that can express both inter- and intra-recursion subtyping without such blowup, including subtyping between constructors of higher or mixed kind. In a second step, we identify a syntactic fragment of this general calculus that allows for more efficient type checking without deep'' substitutions, by observing that higher-kinded iso-recursive types can be inserted to
guard'' against unwanted $\beta$-reductions. This fragment closely resembles the structure of typical nominal subtype systems, but without requiring nominal semantics. It has been used as the basis for a proposed extension of WebAssembly with recursive types.
Thu 26 OctDisplayed time zone: Lisbon change
14:00 - 15:30 | |||
14:00 18mTalk | Greedy Implicit Bounded Quantification OOPSLA Chen Cui University of Hong Kong, Shengyi Jiang University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong DOI | ||
14:18 18mTalk | Structural Subtyping as Parametric Polymorphism OOPSLA Wenhao Tang University of Edinburgh, Daniel Hillerström Huawei Zurich Research Center, James McKinna Heriot-Watt University, Michel Steuwer TU Berlin; University of Edinburgh, Ornela Dardha University of Glasgow, Rongxiao Fu University of Edinburgh, Sam Lindley University of Edinburgh DOI Pre-print | ||
14:36 18mTalk | Simple Reference Immutability for System F<: OOPSLA DOI | ||
14:54 18mTalk | Mutually Iso-Recursive Subtyping OOPSLA Andreas Rossberg Independent DOI | ||
15:12 18mTalk | Getting into the Flow: Towards Better Type Error Messages for Constraint-Based Type Inference OOPSLA Ishan Bhanuka Hong Kong University of Science and Technology, Lionel Parreaux Hong Kong University of Science and Technology, David Binder University of Tübingen, Jonathan Immanuel Brachthäuser University of Tübingen DOI Pre-print |