一句话：扩展联合/交集类型系统加入 type-case，证明其与联合消除可涵盖 occurrence typing，并给出类型重建算法。
论文研究经典联合与交集类型系统如何涵盖 occurrence typing，并解决其实际类型化问题。作者在系统中加入 type-case 构造，证明联合消除规则与 type-case 定型规则的组合可表达 occurrence typing。为落地，他们定义扩展表达式的规范形式 MSC-form，证明表达式可类型化当且仅当其 MSC-form 可类型化，从而将类型化归约为重建 MSC-form 中的标注。最后给出一个可靠的重建算法，并提供概念验证实现。
We extend classic union and intersection type systems with a type-case construction and show that the combination of the union elimination rule of the former and the typing rules for type-cases of our extension encompasses occurrence typing . To apply this system in practice, we define a canonical form for the expressions of our extension, called MSC-form. We show that an expression of the extension is typable if and only if its MSC-form is, and reduce the problem of typing the latter to the one of reconstructing annotations for that term. We provide a sound algorithm that performs this reconstruction and a proof-of-concept implementation.
@article{paperbot1563,
title = {On type-cases, union elimination, and occurrence typing},
author = {Giuseppe Castagna and Mickaël Laurent and Kim Nguyễn and Matthew Lutze},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {POPL},
year = {2022},
doi = {10.1145/3498674}
}