TY - JOUR
T1 - Explaining type inference
AU - Duggan, Dominic
AU - Bent, Frederick
PY - 1996/7
Y1 - 1996/7
N2 - Type inference is the compile-time process of reconstructing missing type information in a program based on the usage of its variables. ML and Haskell are two languages where this aspect of compilation has enjoyed some popularity, allowing type information to be omitted while static type checking is still performed. Type inference may be expected to have some application in the prototyping and scripting languages which 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 presented, which allows the specific reasoning which led to a program variable having a particular type to be recorded for type explanation. This approach is close to the intuitive process used in practice for debugging type errors. The algorithm is practical, and has been implemented in the Standard ML of New Jersey compiler. The modified unification algorithm also appears useful in other domains, including logic program debuggers and semantics-based programming environments.
AB - Type inference is the compile-time process of reconstructing missing type information in a program based on the usage of its variables. ML and Haskell are two languages where this aspect of compilation has enjoyed some popularity, allowing type information to be omitted while static type checking is still performed. Type inference may be expected to have some application in the prototyping and scripting languages which 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 presented, which allows the specific reasoning which led to a program variable having a particular type to be recorded for type explanation. This approach is close to the intuitive process used in practice for debugging type errors. The algorithm is practical, and has been implemented in the Standard ML of New Jersey compiler. The modified unification algorithm also appears useful in other domains, including logic program debuggers and semantics-based programming environments.
UR - http://www.scopus.com/inward/record.url?scp=0030192589&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=0030192589&partnerID=8YFLogxK
U2 - 10.1016/0167-6423(95)00007-0
DO - 10.1016/0167-6423(95)00007-0
M3 - Article
AN - SCOPUS:0030192589
SN - 0167-6423
VL - 27
SP - 37
EP - 83
JO - Science of Computer Programming
JF - Science of Computer Programming
IS - 1
ER -