Thu 20 Jan 2022 15:55 - 16:20 at Salon III - Metaprogramming Chair(s): Stephanie Weirich

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 Jan

Displayed time zone: Eastern Time (US & Canada) change

15:05 - 16:20
MetaprogrammingPOPL at Salon III
Chair(s): Stephanie Weirich University of Pennsylvania
15:05
25m
Research paper
Staging with Class: A Specification for Typed Template HaskellInPerson
POPL
Ningning Xie University of Cambridge, 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
25m
Research 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
25m
Research paper
Type-Level Programming with Match TypesRemote
POPL
DOI Media Attached