SPLASH 2023
Sun 22 - Fri 27 October 2023 Cascais, Portugal
Thu 26 Oct 2023 14:54 - 15:12 at Room I - type systems 2 Chair(s): Max S. New

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 toguard'' 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 Oct

Displayed time zone: Lisbon change

14:00 - 15:30
type systems 2OOPSLA at Room I
Chair(s): Max S. New University of Michigan
14:00
18m
Talk
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
18m
Talk
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
18m
Talk
Simple Reference Immutability for System F<:
OOPSLA
Edward Lee University of Waterloo, Ondřej Lhoták University of Waterloo
DOI
14:54
18m
Talk
Mutually Iso-Recursive Subtyping
OOPSLA
Andreas Rossberg Independent
DOI
15:12
18m
Talk
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