Compositional Type Checking for Hindley-Milner Type Systems with Ad-hoc Polymorphism

Abstract

Statically typed functional programming languages usually employ a version of the Hindley-Milner type system extended with ad-hoc polymorphism. When the type checker detects an error, it has to report it to the programmer, to help in fixing the bug. However, usage of algorithms W and M, commonly used to type-check languages with Hindley-Milner type systems, can result in cryptic error messages. We argue that the holistic nature of these algorithms is a cause of this. Next, we describe a type checking algorithm originally presented by Olaf Chitil in 2001, that, by its compositional nature, claims to produce error messages that are more suitable for human processing — a property that type systems for imperative programming languages usually have. The main part of the thesis is extending the compositional algorithm for languages supporting ad-hoc polymorphism. A proof of concept implementation is presented for the Haskell 98 programming language, interfacing the Glasgow Haskell Compiler. In conclusion, we present this implementation and ideas for future work.