Type inference in context

Adam Gundry, Conor Mcbride, James McKinna

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

3 Citations (Scopus)

Abstract

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
Pages43-54
Number of pages12
DOIs
Publication statusPublished - 2010
EventMSFP 2010 - , United Kingdom
Duration: 25 Sep 201025 Sep 2010

Workshop

WorkshopMSFP 2010
CountryUnited Kingdom
Period25/09/1025/09/10

Keywords

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

Cite this

Gundry, A., Mcbride, C., & McKinna, J. (2010). Type inference in context. In MSFP '10 Proceedings of the third ACM SIGPLAN workshop on Mathematically structured functional programming (pp. 43-54) https://doi.org/10.1145/1863597.1863608