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.

Citation as BibTeX

@article{blanvillain21matchtypes,
  author = {Blanvillain, Olivier and Brachthäuser, Jonathan Immanuel and Kjaer, Maxime and Odersky, Martin},
  title = {Type-Level Programming with Match Types},
  issue_date = {January 2022},
  publisher = {Association for Computing Machinery},
  journal = {Proc. ACM Program. Lang.},
  month = {jan},
  articleno = {37},
  numpages = {24},
  address = {New York, NY, USA},
  volume = {6},
  number = {POPL},
  year = {2022},
  url = {https://zenodo.org/record/5568850},
  doi = {10.1145/3498698},
  month_numeric = {1}
}

Talk

Video recording of the talk available on YouTube.

News

November 9

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 groupJonathan 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).