Polymorphic Type Inference for Languages with Overloading and Subtyping

Other Titles


Many computer programs have the property that they work correctly on a variety of types of input; such programs are called polymorphic. Polymorphic type systems support polymorphism by allowing programs to be given multiple types. In this way, programs are permitted greater flexibility of use, while still receiving the benefits of strong typing. One especially successful polymorphic type system is the system of Hindley, Milner, and Damas, which is used in the programming language ML. This type system allows programs to be given universally quantified types as a means of expressing polymorphism. It has two especially nice properties. First, every well-typed program has a "best" type, called the principal type, that captures all the possible types of the program. Second, principal types can be inferred, allowing programs to be written without type declarations. However, two useful kinds of polymorphism cannot be expressed in this type system: overloading and subtyping. Overloading is the kind of polymorphism exhibited by a function like addition, whose types cannot be captured by a single universally quantified type formula. Subtyping is the property that one type is contained in another, as, for example, intreal. This dissertation extends the Hindley/Milner/Damas type system to incorporate overloading and subtyping. The key device needed is constrained universal quantification, in which quantified variables are allowed only those instantiations, that satisfy a set of constraints. We present an inference algorithm and prove that it is sound and complete; hence it infers principal types. An issue that arises with constrained quantification is the satisfiability of constraint sets. We prove that it is undecidable whether a given constraint set is satisfiable; this difficulty leads us to impose restrictions on overloading. An interesting feature of type inference with subtyping is the necessity of simplifying the inferred types-the unsimplified types are unintelligible. The simplification process involves shape unification, graph algorithms such as strongly connected components and transitive reduction, and simplifications based on the monotonicities of type formulas.

Journal / Series

Volume & Issue



Date Issued



Cornell University


computer science; technical report


Effective Date

Expiration Date




Union Local


Number of Workers

Committee Chair

Committee Co-Chair

Committee Member

Degree Discipline

Degree Name

Degree Level

Related Version

Related DOI

Related To

Related Part

Based on Related Item

Has Other Format(s)

Part of Related Item

Related To

Related Publication(s)

Link(s) to Related Publication(s)


Link(s) to Reference(s)

Previously Published As

Government Document




Other Identifiers


Rights URI


technical report

Accessibility Feature

Accessibility Hazard

Accessibility Summary

Link(s) to Catalog Record