This paper proposes a novel language design that combines extensible data types, implemented through row types and row polymorphism, with ad-hoc polymorphism, implemented through type classes. Our design introduces several new constructs and constraints useful for generic operations over rows. We formalize our design in a source calculus λ⇒ρ, which elaborates into a target calculus F⊗⊕ω. We prove that the target calculus is type-safe and that the elaboration is sound, thus establishing the soundness of λ⇒ρ. All proofs are mechanized in the Lean 4 proof assistant. Furthermore, we evaluate our type system using the Brown Benchmark for Table Types, demonstrating the utility of extensible rows with type classes for table types.
Wed 14 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
Wed 14 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change
14:00 - 15:40 | |||
14:00 25mTalk | Extensible Data Types with Ad-Hoc Polymorphism POPL Matthew Toohey University of Toronto, Yanning Chen University of Toronto, Ara Jamalzadeh University of Toronto, Ningning Xie University of Toronto DOI Pre-print | ||
14:25 25mTalk | Let Generalization, Polymorphic Recursion, and Variable Minimization in Boolean-Kinded Type Systems POPL Joseph Zullo Purdue University DOI | ||
14:50 25mTalk | Local Contextual Type Inference POPL Xu Xue University of Hong Kong, Chen Cui University of Hong Kong, Shengyi Jiang The University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong DOI | ||
15:15 25mTalk | Typing Strictness POPL Daniel Sainati University of Pennsylvania, Joseph W. Cutler University of Pennsylvania, Benjamin C. Pierce University of Pennsylvania, Stephanie Weirich University of Pennsylvania DOI | ||