一句话：提出部分类型构造子的语言设计与形式理论，用限定类型刻画其定义域，支持部分数据类型作为一等公民。
函数式编程语言通常假定类型构造子是全域的，但实践中存在大量部分定义的例子，如对内容有额外约束的容器类型，以及只在部分参数上定义方程的类型族。本文提出部分类型构造子的语言设计与形式理论，利用限定类型（qualified types）来刻画类型构造子的定义域。该设计既简单又富有表达力：部分数据类型可作为一等公民使用，包括作为 Haskell Functor、Monad 等参数化抽象的实例；作者给出了一种简单的类型精化算法，避免给程序员带来过重的标注负担。文章证明该类型系统能拒绝定义不良的类型，并可编译到基于 System F 的语义模型。最后，作者通过概念验证实现，对一批 Haskell 代码进行了实验分析，发现虽然在部分情况下需要额外标注，但这些情况在实际 Haskell 代码中很少遇到。
Functional programming languages assume that type constructors are total. Yet functional programmers know better: counterexamples range from container types that make limiting assumptions about their contents (e.g., requiring computable equality or ordering functions) to type families with defining equations only over certain choices of arguments. We present a language design and formal theory of partial type constructors, capturing the domains of type constructors using qualified types. Our design is both simple and expressive: we support partial datatypes as first-class citizens (including as instances of parametric abstractions, such as the Haskell Functor and Monad classes), and show a simple type elaboration algorithm that avoids placing undue annotation burden on programmers. We show that our type system rejects ill-defined types and can be compiled to a semantic model based on System F. Finally, we have conducted an experimental analysis of a body of Haskell code, using a proof-of-concept implementation of our system; while there are cases where our system requires additional annotations, these cases are rarely encountered in practical Haskell code.
@article{paperbot553,
title = {Partial type constructors: or, making ad hoc datatypes less ad hoc},
author = {Mark P. Jones and J. Garrett Morris and Richard A. Eisenberg},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
year = {2019},
doi = {10.1145/3371108}
}