Discriminative sum types locate the source of type errors
Discriminative sum types locate the source of type errors
复制标题
判别和类型定位类型错误的来源
DOI：
10.1145/944705.944708
复制
发表时间：
2003
影响因子：
2.6
通讯作者：
Peter Thiemann
中科院分区：
文献类型：
--
作者：
Matthias Neubauer;Peter Thiemann
我们提出了一种类型系统，用于在具有ML式多态性的应用的Lambda演算中定位类型误差的来源。该系统基于判别总量类型---从软键入工作中已知 - 带有注释亚型和递归类型。这样，可以在类型中注册类型冲突以供以后报告。注释跟踪每个值的潜在生产者和消费者，以便可以将冲突追溯到其原因。每个术语在我们的系统中都可以打字，并且类型推断是可以决定的。我们系统中的类型派生描述了程序中存在的所有类型错误，因此主推导会产生对所有类型错误的主要描述。错误消息是从完成的类型推导得出的。因此，错误消息独立于用于类型推理的特定算法，前提是它构建了这种推导。
We propose a type system for locating the source of type errors in an applied lambda calculus with ML-style polymorphism. The system is based on discriminative sum types---known from work on soft typing---with annotation subtyping and recursive types. This way, type clashes can be registered in the type for later reporting. The annotations track the potential producers and consumers for each value so that clashes can be traced to their cause.Every term is typeable in our system and type inference is decidable. A type derivation in our system describes all type errors present in the program, so that a principal derivation yields a principal description of all type errors present. Error messages are derived from completed type derivations. Thus, error messages are independent of the particular algorithm used for type inference, provided it constructs such a derivation.