Picture of two heads

Open Access research that challenges the mind...

The Strathprints institutional repository is a digital archive of University of Strathclyde research outputs. Strathprints provides access to thousands of Open Access research papers by University of Strathclyde researchers, including those from the School of Psychological Sciences & Health - but also papers by researchers based within the Faculties of Science, Engineering, Humanities & Social Sciences, and from the Strathclyde Business School.

Discover more...

Type inference in context

Gundry, Adam and Mcbride, Conor and McKinna, James (2010) Type inference in context. In: MSFP '10 Proceedings of the third ACM SIGPLAN workshop on Mathematically structured functional programming. ACM, New York, NY, pp. 43-54. ISBN 978-1-4503-0255-5

Full text not available in this repository. (Request a copy from the Strathclyde author)


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.