Type-Level Programming with Match Types

by Olivier Blanvillain, Jonathan Immanuel Brachthäuser, Maxime Kjaer, and Martin Odersky

In Proc. ACM Program. Lang. 6(POPL). Association for Computing Machinery, 2022.

Abstract

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<: 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.

Talk

Video recording of the talk available on YouTube.

News

Paper accepted for publication at POPL 2022

Our paper “Type-Level Programming with Match Types” (Olivier Blanvillain, Jonathan Brachthäuser
Head of the SE research group
Jonathan Immanuel Brachthäuser
, Maxime Kjaer, and Martin Odersky) has been accepted for publication at the ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2022).

Read more ...