一句话：提出 match types——类型级的模式匹配，在基于 System F<: 的演算中形式化并证明可靠性，并在 Scala 3 编译器中实现。
类型级编程在函数式编程领域日益流行，但它与子类型的结合在实用编程语言中仍鲜有探索。本文提出 match types，即模式匹配在类型层面的对应物：它能够无缝融入带子类型的语言，并且尽管形式简单，却显著提升了类型级计算的表达力。作者在基于 System F<: 的演算中形式化了 match types 这一特性，并证明了该系统的可靠性（soundness），从而为其在带子类型语言中的使用提供了理论基础。在实践层面，作者将 match types 实现在 Scala 3 参考编译器中，使类型级编程能够为广泛的程序员群体直接可用，并借此验证了该设计在真实语言实现中的可行性。
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.
@article{paperbot1589,
title = {Type-level programming with match types},
author = {Olivier Blanvillain and Jonathan Immanuel Brachthäuser and Maxime Kjaer and Martin Odersky},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {POPL},
year = {2022},
doi = {10.1145/3498698}
}