Type inference gives programmers the benefit of static, compile-time
type checking without the cost of manually specifying types, and has
long been a standard feature of functional programming languages.
However, it has proven difficult to integrate type inference with
subtyping, since the unification engine at the core of classical type
inference accepts only equations, not subtyping constraints.
This thesis presents a type system combining ML-style parametric
polymorphism and subtyping, with type inference, principal types, and
decidable type subsumption. Type inference is based on biunification,
an analogue of unification that works with subtyping constraints.
Making this possible are several contributions, beginning with the
notion of an "extensible" type system, in which an open world of
types is assumed, so that no typeable program becomes untypeable by the
addition of new types to the language. While previous formulations of
subtyping fail to be extensible, this thesis shows that adopting a
more algebraic approach can remedy this. Using such an approach, this
thesis develops the theory of biunification, shows how it is used to
infer types, and shows how it can be efficiently implemented,
exploiting deep connections between the algebra of regular languages
and polymorphic subtyping.