Type-level programming is becoming more and more popular in the realm of functional programming. However, the combination of type-level programming and subtyping remains largely unexplored in practical programming languages. This paper presents match types, a type-level equivalent of pattern matching. Match types integrate seamlessly into programming languages with subtyping and, despite their simplicity, offer significant additional expressiveness. We formalize the feature of match types in a calculus based on System F sub and prove its soundness. We practically evaluate our system by implementing match types in the Scala 3 reference compiler, thus making type-level programming readily available to a broad audience of programmers.
Thu 20 JanDisplayed time zone: Eastern Time (US & Canada) change
Thu 20 Jan
Displayed time zone: Eastern Time (US & Canada) change
15:05 - 16:20 | |||
15:05 25mResearch paper | Staging with Class: A Specification for Typed Template HaskellInPerson POPL Ningning Xie University of Toronto, Matthew Pickering Well-Typed LLP, Andres Löh Well-Typed LLP, Nicolas Wu Imperial College London, Jeremy Yallop University of Cambridge, Meng Wang University of Bristol DOI Media Attached | ||
15:30 25mResearch paper | Mœbius: Metaprogramming using Contextual Types: The Stage Where System F Can Pattern Match on ItselfRemote POPL Junyoung Jang McGill University, Samuel Gélineau SimSpace, Stefan Monnier Université de Montréal, Brigitte Pientka McGill University DOI Media Attached | ||
15:55 25mResearch paper | Type-Level Programming with Match TypesRemote POPL Olivier Blanvillain EPFL, Jonathan Immanuel Brachthäuser University of Tübingen, Maxime Kjaer EPFL, Martin Odersky EPFL DOI Media Attached |