Adam Gundry, Conor McBride and James McKinna
We consider the problems of first-order unification and type inference from a very general perspective on problem-solving, namely that of information increase in the problem context. This leads to a powerful technique for implementing type inference algorithms. We describe a unification algorithm and illustrate the technique by applying it to the familiar Hindley-Milner type system, but it can be applied to more advanced type systems. The algorithms depend on a well-founded invariant on contexts in which type variable bindings and type-schemes for terms may depend only on bindings appearing earlier in the context. We ensure that unification produces a most general unifier, and that type inference produces principal types, by advancing definitions earlier in the context only when absolutely necessary.
Latest version: Type Inference in Context (PDF) and source code (LHS), updated 30th July 2010, appeared at MSFP 2010 © ACM 2010. This is the author's version of the work. It is posted here for your personal use. Not for redistribution. The definitive Version of Record can be found in the Proceedings of the third ACM SIGPLAN workshop on Mathematically Structured Functional Programming, doi:10.1145/1863597.1863608.
Slides: MSFP talk (PDF) on 25th September 2010
Previous version: Type Inference in Context (PDF) and source code (LHS), updated 23rd April 2010