Better type errors for the Hindley-Milner type system

The type systems of most typed functional programming languages are based on the Hindley-Milner type system. It combines the unobtrusiveness of not requiring any type annotations in the program with the flexibility of polymorphism. The basic ideas of the type system are intuitive: A function can have many types. The type of a polymorphic function represents all types that can be gained by instantiation of its type variables. Every function has a principal, that is, most general, type which represents all of its types. Practical experience shows that the type checker catches many errors, from trivial oversights to sometimes even deep logical errors. But experience also shows that from a type error message it is often hard to deduce the actual cause of the error and understand it. Numerous solutions to the problem have been proposed. Many of these fail to address the actual problem and most require complex implementations.

Papers

Software

TypeIlluminator
is a prototype tool implementing the ideas presented in the paper Compositional Explanation of Types and Algorithmic Debugging of Type Errors. It constructs the type explanation graph for programs written in a simple Haskell-like language and enables free navigation through the graph in various ways and algorithmic debugging.