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, GBR, pp. 43-54. ISBN 978-1-4503-0255-5 (https://doi.org/10.1145/1863597.1863608)

Full text not available in this repository.Request a copy

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.

ORCID iDs

Gundry, Adam, Mcbride, Conor ORCID logoORCID: https://orcid.org/0000-0003-1487-0886 and McKinna, James;
CORE (COnnecting REpositories)