M. Widera and C. Beierle. A complete type system for functional languages. Informatik Berichte 240, FernUniversität Hagen, September 1998.

Abstract:

This paper presents a powerful type system for functional programming languages consisting of an expressive type language and a type inference algorithm. In contrast to the usual approach it is complete in the sense that every program which is type correct is recognized as such. We get the advantage that every type error reported by our system is a real error. This is useful in debugging programs, since the programmer can rely on the error messages and need not check whether a returned function call really contains a type error and is not just hard to prove type correct. Soundness is a less important property in this context, because there are usually some more stages of debugging that can catch the other bugs.

Available: PS, BibTeX