Partial type constructors: or, making ad hoc datatypes less ad hoc
Partial type constructors: or, making ad hoc datatypes less ad hoc
复制标题
部分类型构造函数：或者，使临时数据类型不那么临时
DOI：
10.1145/3371108
复制
发表时间：
2020
影响因子：
--
通讯作者：
Eisenberg, Richard A.
中科院分区：
文献类型：
--
作者：
Jones, Mark P.;Morris, J. Garrett;Eisenberg, Richard A.
函数式编程语言假定类型构造函数是全的。然而，函数式程序员更清楚：反例的范围从容器类型，使其内容的限制性假设（例如，需要可计算的等式或排序函数）来对仅在某些参数选择上定义方程的族进行类型化。我们提出了一种语言设计和形式化理论的部分类型构造器，捕获域的类型构造器使用合格的类型。我们的设计既简单又富有表现力：我们支持部分数据库作为一等公民（包括作为参数抽象的实例，如Haskell Functor和Monad类），并展示了一个简单的类型细化算法，避免给程序员带来不必要的注释负担。我们表明，我们的类型系统拒绝定义不明确的类型，并可以编译成一个语义模型的基础上系统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.