Type inference in context

Adam Gundry, Conor Mcbride, James McKinna

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

8 Citations (Scopus)


We consider the problems of first-order unification and type inference from a 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 for the familiar Hindley-Milner type system, but it can be applied to more advanced type systems. The algorithms depend on well-founded contexts: type variable bindings and type-schemes for terms may depend only on earlier bindings. We ensure that unification yields a most general unifier, and that type inference yields principal types, by advancing definitions earlier in the context only when necessary.
Original languageEnglish
Title of host publicationMSFP '10 Proceedings of the third ACM SIGPLAN workshop on Mathematically structured functional programming
Number of pages12
Publication statusPublished - 2010
EventMSFP 2010 - , United Kingdom
Duration: 25 Sep 201025 Sep 2010


WorkshopMSFP 2010
Country/TerritoryUnited Kingdom


  • algorithms
  • theory
  • type inference
  • first-order unification

Cite this