Type Inference with Constrained Types

Martin Odersky, Martin Sulzmann, Martin Wehr. Type Inference with Constrained Types. TAPOS, 5(1):35-55, 1999.


We present a general framework HM(X) for type systems with constraints. The framework stays in the tradition of the Hindley/Milner type system. Its type system instances are sound under a standard untyped compositional semantics. We can give a generic type inference algorithm for HM(X) so that, under sufficient conditions on X, type inference will always compute the principal type of a term. We discuss instances of the framework that deal with polymorphic records, equational theories, and subtypes.