Searching for type-error messages
Searching for type-error messages
复制标题
搜索类型错误消息
DOI：
--
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
C. Chambers
中科院分区：
文献类型：
--
作者：
Benjamin S. Lerner;M. Flower;D. Grossman;C. Chambers
高级类型系统通常需要某种形式的类型推断来减轻显式类型化的负担，但是类型推断通常会导致不良类型程序的错误消息。这项工作追求一种新的方法来构建编译器和提出类型错误的消息，类型检查器本身不产生的消息。相反，它是一个搜索过程的预言机，用于查找进行类型检查的类似程序。我们的双重目标是在简化编译器构造的同时改善错误消息。我们的主要实现和评估是Caml，一种具有全类型推理的语言。我们还提出了一个原型的C++模板函数，类型实例化是隐式的。一个关键的扩展是，即使程序有多个独立的类型错误，我们的方法也是鲁棒的。
Advanced type systems often need some form of type inference to reduce the burden of explicit typing, but type inference often leads to poor error messages for ill-typed programs. This work pursues a new approach to constructing compilers and presenting type-error messages in which the type-checker itself does not produce the messages. Instead, it is an oracle for a search procedure that finds similar programs that do type-check. Our two-fold goal is to improve error messages while simplifying compiler construction. Our primary implementation and evaluation is for Caml, a language with full type inference. We also present a prototype for C++ template functions, where type instantiation is implicit. A key extension is making our approach robust even when the program has multiple independent type errors.