Intensional datatype refinement: with application to scalable verification of pattern-match safety
Intensional datatype refinement: with application to scalable verification of pattern-match safety
复制标题
内涵数据类型细化：应用于模式匹配安全性的可扩展验证
DOI：
10.1145/3434336
复制
发表时间：
2021
影响因子：
--
通讯作者：
Jones E
中科院分区：
文献类型：
--
作者：
Jones E
模式匹配安全问题是验证给定的功能程序永远不会因其函数定义中的非详尽模式而崩溃。我们提出了一个可以用来解决这个问题的细化类型系统。该系统通过有限形式的结构子类型和环境级交集，用代数数据类型扩展了 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.