Polymorphic Type Inference for Languages with Overloading and Subtyping

Abstract

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, $int \subseteq real$. 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.