EXPLAINING TYPE INFERENCE

Type inference is the compile-time process of reconstructing missing t ype information in a program based on the usage of its variables. ML a nd Haskell are two languages where this aspect of compilation has enjo yed some popularity, allowing type information to be omitted while sta tic type checking is still performed. Type inference may be expected t o have some application in the prototyping and scripting languages whi ch are becoming increasingly popular. A difficulty with type inference is the confusing and sometimes counter-intuitive diagnostics produced by the type checker as a result of type errors. A modification of the unification algorithm used in Hindley-Milner type inference is presen ted, which allows the specific reasoning which led to a program variab le having a particular type to be recorded for type explanation. This approach is close to the intuitive process used in practice for debugg ing type errors. The algorithm is practical, and has been implemented in the Standard ML of New Jersey compiler. The modified unification al gorithm also appears useful in other domains, including logic program debuggers and semantics-based programming environments.