Revisiting Row Polymorphism for Set-Theoretic Types
This program is tentative and subject to change.
Set-theoretic types support expressive record types through unions, intersections, and negations, but they lack the row polymorphism needed to type operations that propagate unknown fields across records. Prior work addresses this by allowing Boolean combinations of rows in type substitutions, which complicates the formalism and prevents the tallying algorithm from being complete. We propose an alternative: instead of enriching substitutions, we allow Boolean combinations of row variables directly within record type constructors, where the tail of a record has the same shape as any field. This design keeps substitutions simple—a row variable maps to a single row—and yields a natural extension of the subtyping and tallying algorithms. Tallying is complete for all solutions whose rows are constant over labels not mentioned in the constraints. We implement our approach in the set-theoretic type library SSTT and the type checker MLsem, providing the first implementation of a type system that combines semantic subtyping with row polymorphism. We demonstrate the expressiveness of the system by encoding several data structures from the R programming language: heterogeneous lists, variadic function arguments, and class-based dispatch.
This program is tentative and subject to change.
Mon 5 OctDisplayed time zone: Pacific Time (US & Canada) change
15:30 - 17:00 | Effects, Capabilities, and ImmutabilityOOPSLA at East Hall 2 Chair(s): Alex Potanin Australian National University | ||
15:30 18mTalk | Revisiting Row Polymorphism for Set-Theoretic Types OOPSLA Mickaël Laurent Charles University, Pierre Donat-Bouillud Czech Technical University, Filip Křikava Czech Technical University, Jan Vitek Charles University DOI | ||
15:48 18mTalk | Type, Ability, and Effect Systems: Perspectives on Purity, Semantics, and Expressiveness OOPSLA DOI | ||
16:06 18mTalk | Transitive, Abstract, and Class Polymorphic ImmutabilityDistinguished Paper OOPSLA Aosen Xiong University of Waterloo, Yudi Bai University of Waterloo, Haifeng Shi University of Waterloo, Lian Sun University of Waterloo, Mier Ta University of Waterloo, Werner Dietl University of Waterloo DOI | ||
16:24 18mTalk | Handling Exceptions and Effects with Automatic Resource Analysis OOPSLA Ethan Chu Carnegie Mellon University, Yiyang Guo Carnegie Mellon University, Jan Hoffmann Carnegie Mellon University DOI | ||