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.
翻译：模式匹配的安全问题是核实某个功能程序不会因为其功能定义中的非详尽模式而崩溃。 我们提出了一个可用于解决这一问题的精细类型系统。 这个系统以有限的结构亚型和环境级交叉形式扩展具有代数数据类型的ML型系统。 我们描述了这个系统的一个完全自动、健全和完整的类型推断程序,根据合理的假设,这个系统在程序大小方面是最坏的直线时间。 组成性对于获得这一复杂程度的保证至关重要。 哈斯凯尔的原型实施能够在几百毫秒的时间内分析哈卡奇数据库的软件包选择。
相关内容
微信扫码咨询专知VIP会员