On the Unification of Substitutions in Type-Inference

Bruce J. McAdam


Traditional type-inference and type-checking algorithms work well with correctly typed programs, but their results when given programs containing type-errors can be unpredictable. This leads to a problem with implementations of type-checkers: they are often inaccurate when announcing the apparent locations of mistakes in programs, tending to notice problems towards the end of the the program even if the source occurs much earlier. This is a particular problem with programming languages with Hindley-Milner type-systems such as used in Standard ML.

A common technique in type-inference and type-checking is unification. Unifying types creates a substitution which is applied to a type-environment. The substitutions which have been applied to the type-environment can influence the detection of type-errors in different subexpressions of the program.

This paper defines the operation of unifying substitutions and shows how type-inference algorithms can be modified to use this operation to delay the application of substitutions to the type-environment. This removes the bias to detecting errors towards the end of the program. Two different type-inference algorithms for Hindley-Milner type-inference are modified in this way and the potential for improved error reporting is shown.


This report is available in the following formats:

Previous | Index | Next