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
-
Compositional explanation of types and algorithmic debugging of type errors.
Olaf Chitil.
In Proceedings of the Sixth ACM SIGPLAN International Conference on
Functional Programming (ICFP'01), pages 193-204, Firenze, Italy,
September 2001. ACM.
-
Typeview:
A Tool for Understanding Type Errors.
Axel Simon, Olaf Chitil, and Frank Huch.
In Markus Mohnen and Pieter Koopman, editors, Draft Proceedings of the
12th International Workshop on Implementation of Functional Languages,
pages 63-69, Aachen, Germany, September 2000. Aachener Informatik-Bericht
00-7, RWTH Aachen.
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.