Subtyping

In programming language theory, subtyping (also subtype polymorphism or inclusion polymorphism) is a form of type polymorphism in which a subtype is a datatype that is related to another datatype (the supertype) by some notion of substitutability, meaning that program elements, typically subroutines or functions, written to operate on elements of the supertype can also operate on elements of the subtype. If S is a subtype of T, the subtyping relation is often written S <: T, to mean that any term of type S can be safely used in a context where a term of type T is expected. The precise semantics of subtyping crucially depends on the particulars of what "safely used in a context where" means in a given programming language. The type system of a programming language essentially defines its own subtyping relation, which may well be trivial.

Because the subtyping relation allows a term to have (belong to) more than one type, subtyping is a form of type polymorphism, so it is (properly) called subtype polymorphism. In object-oriented programming subtyping is commonly called just polymorphism (see polymorphism in object-oriented programming). Subtyping is practically never called this way in type theory or in functional programming, where the unqualified use of "polymorphism" usually refers to parametric polymorphism, as in polymorphic lambda calculus. (Mechanisms similar in purpose, but not identical with parametric polymorphism are known by other names in object-oriented programming, e.g. generics in Java or templates in C++.)

Functional programming languages often allow the subtyping of records. Consequently, simply typed lambda calculus extended with record types is perhaps the simplest theoretical setting in which a useful notion of subtyping may be defined and studied. Because the resulting calculus allows terms to have more than one type, it is no longer a "simple" type theory. Since functional programming languages, by definition, support function literals, which can also be stored in records, records types with subtyping provide some of the features of object-oriented programming. (Unless references are added to the language, record "objects" are immutable). Typically, functional programming languages also provide some, usually restricted, form of parametric polymorphism. In a theoretical setting, it is desirable to study the interaction of the two features; a common theoretical setting is system F_<:. Various calculi that attempt to capture the theoretical properties of object-oriented programming may be derived from system F_<:.

The concept of subtyping is related to the linguistic notions of hypernymy and holonymy. It is also related to the concept of bounded quantification in mathematical logic. Subtyping should not be confused with the notion of (class or object) inheritance from object-oriented languages; subtyping is a relation between types (interfaces in object-oriented parlance) whereas inheritance is a relation between implementations stemming from a language feature that allows new objects to be created from existing ones. In a number of object-oriented languages, subtyping is called interface inheritance.