Repairing Type Errors in Functional Programs

Abstract

Type systems for programming languages can be used by compilers to reject programs which are found to be unsound and which may, therefore, fail to execute successfully. When a program is rejected the programmer must repair it so that it can be type-checked correctly and then executed safely. Diagnostic error messages are essential to help the programmer repair the program.

Hindley-Milner type systems give the programmer a great deal of flexibility (polymorphism and implicit typing) while ensuring type safety. As a consequence of this flexibility repairing mistakes can be difficult and programmers have previously observed that type error messages produced by compilers are not helpful enough.

This thesis examines the problem of producing more helpful error messages for ill-typed programs written in programming languages with a Hindley-Milner typing discipline. Three main results are described. Firstly, type inference algorithms which infer types in different orders are described, and the ability of these to produce more meaningful error messages is investigated. Secondly, the results of several other authors on helping to explain type inference are condensed into a single generalisation. Thirdly, error messages which suggest concrete changes to the program to remove type errors are produced using the theory of linear type isomorphisms. This theory is implemented as an extension to the MLj compiler. Finally, extensions to Hindley-Milner are explored, taking the type system of MLj as an example.