一句话：提出用于模式匹配安全验证的内涵数据类型精化类型系统，其推断可靠、完备且接近线性时间。
论文研究函数式程序的模式匹配安全问题：验证程序不会因函数定义中模式非穷尽而崩溃。作者提出一种精化类型系统，在 ML 风格代数数据类型类型系统上引入受限的结构子类型和环境级交集，从而描述数据构造子的存在与缺失等内涵信息。该系统支持全自动、可靠且完备的类型推断；在合理假设下，推断的最坏时间复杂度关于程序规模线性，组合性是获得该保证的关键。作者为 Haskell 实现原型，可分析 Hackage 数据库中的若干包，通常在数百毫秒内完成，展示了可扩展性。
The pattern-match safety problem is to verify that a given functional program will never crash due to non-exhaustive patterns in its function definitions. We present a refinement type system that can be used to solve this problem. The system extends ML-style type systems with algebraic datatypes by a limited form of structural subtyping and environment-level intersection. We describe a fully automatic, sound and complete type inference procedure for this system which, under reasonable assumptions, is worst-case linear-time in the program size. Compositionality is essential to obtaining this complexity guarantee. A prototype implementation for Haskell is able to analyse a selection of packages from the Hackage database in a few hundred milliseconds.
@article{paperbot1169,
title = {Intensional datatype refinement: with application to scalable verification of pattern-match safety},
author = {Eddie Jones and Steven Ramsay},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {POPL},
year = {2021},
doi = {10.1145/3434336}
}