查看文章

Compilers for programming languages such as Standard ML are able to nd many programming errors at compile time, however the diagnostic messages from the type inference algorithm do not always clearly identify the source of type errors. We argue that an extended type definition, which assigns types to open expressions as well as closed expressions, can serve as the basis for a programming environment that helps programmers debug type errors. We present such a type de nition, which is closely related to the Damas/Milner de nition, but which in addition provides principal typings for open expressions. We present an algorithm that performs type inference with respect to our type system and give a simple direct proof of its correctness. Finally we describe a prototype implementation.