Subtyping
In programming language theory, subtyping is a form of type polymorphism. A subtype is a datatype that is related to another datatype by some notion of substitutability, meaning that program elements, 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 means that any term of type S can safely be used in any context where a term of type T is expected. The precise semantics of subtyping here crucially depends on the particulars of how "safely be used" and "any context" are defined by a given type formalism or programming language. The type system of a programming language essentially defines its own subtyping relation, which may well be trivial, should the language support no conversion mechanisms.
Due to the subtyping relation, a term may belong to more than one type. Subtyping is therefore a form of type polymorphism. In object-oriented programming the term 'polymorphism' is commonly used to refer solely to this subtype polymorphism, while the techniques of parametric polymorphism would be considered generic programming.
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. 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 hyponymy and holonymy. It is also related to the concept of bounded quantification in mathematical logic. Subtyping should not be confused with the notion of inheritance from object-oriented languages; subtyping is a relation between types 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, with inheritance referred to as implementation inheritance.
Origins
The notion of subtyping in programming languages dates back to the 1960s; it was introduced in Simula derivatives. The first formal treatments of subtyping were given by John C. Reynolds in 1980 who used category theory to formalize implicit conversions, and Luca Cardelli.The concept of subtyping has gained visibility with the mainstream adoption of object-oriented programming. In this context, the principle of safe substitution is often called the Liskov substitution principle, after Barbara Liskov who popularized it in a keynote address at a conference on object-oriented programming in 1987. Because it must consider mutable objects, the ideal notion of subtyping defined by Liskov and Jeannette Wing, called behavioral subtyping is considerably stronger than what can be implemented in a type checker.
Examples
A simple practical example of subtypes is shown in the diagram. The type "bird" has three subtypes "duck", "cuckoo" and "ostrich". Conceptually, each of these is a variety of the basic type "bird" that inherits many "bird" characteristics but has some specific differences. The UML notation is used in this diagram, with open-headed arrows showing the direction and type of the relationship between the supertype and its subtypes.As a more practical example, a language might allow integer values to be used wherever floating point values are expected, or it might define a generic type Number as a common supertype of integers and the reals. In this second case, we only have
Integer <: Number and Float <: Number, but Integer and Float are not subtypes of each other.Programmers may take advantage of subtyping to write code in a more abstract manner than would be possible without it. Consider the following example:
function max is
if x < y then
return y
else
return x
end
If integer and real are both subtypes of
Number, and an operator of comparison with an arbitrary Number is defined for both types, then values of either type can be passed to this function. However, the very possibility of implementing such an operator highly constrains the Number type, and actually only comparing integers with integers, and reals with reals, makes sense. Rewriting this function so that it would only accept 'x' and 'y' of the same type requires bounded polymorphism.Subtyping enables a given type to be substituted for another type or abstraction. Subtyping is said to establish an is-a relationship between the subtype and some existing abstraction, either implicitly or explicitly, depending on language support. The relationship can be expressed explicitly via inheritance in languages that support inheritance as a subtyping mechanism.
C++
The following C++ code establishes an explicit inheritance relationship between classes B and A, where B is both a subclass and a subtype of A, and can be used as an A wherever a B is specified.class A ;
class B : public A ;
void functionOnA
int main
Python
The following python code establishes an explicit inheritance relationship between classes and, where is both a subclass and a subtype of, and can be used as an wherever a is required.class A:
def method_of_a -> None:
pass
class B:
def method_of_b -> None:
pass
def function_on_a -> None:
a.method_of_a
if __name__ "__main__":
b: B = B
function_on_a # b can be substituted for an A.
The following example, is a "regular" type, and is a metatype. While as distributed all types have the same metatype, this is not a requirement. The type of classic classes, known as, can also be considered a distinct metatype.
a = 0
- prints:
- prints:
- prints:
- prints:
Java
In Java, is-a relation between the type parameters of one class or interface and the type parameters of another are determined by the extends and implements clauses.Using the classes, implements, and extends. So is a subtype of, which is a subtype of. The subtyping relationship is preserved between the types automatically. When defining an interface,, that associates an optional value of generic type P with each element, its declaration might look like:
interface PayloadList
The following parameterizations of PayloadList are subtypes of :
PayloadList
PayloadList
PayloadList
Subsumption
In type theory the concept of subsumption is used to define or evaluate whether a type S is a subtype of type T.A type is a set of values. The set can be described extensionally by listing all the values, or it can be described intensionally by stating the membership of the set by a predicate over a domain of possible values. In common programming languages enumeration types are defined extensionally by listing values. User-defined types like records or classes are defined intensionally by an explicit type declaration or by using an existing value, which encodes type information, as a prototype to be copied or extended.
In discussing the concept of subsumption, the set of values of a type is indicated by writing its name in mathematical italics:. The type, viewed as a predicate over a domain, is indicated by writing its name in bold: T. The conventional symbol <: means "is a subtype of", and :> means "is a supertype of".
- A type T subsumes S if the set of values which it defines, is a superset of the set, so that every member of is also a member of.
- A type may be subsumed by more than one type: the supertypes of S intersect at.
- If S <: T, then T, the predicate which circumscribes the set, must be part of the predicate S which defines.
- If S subsumes T, and T subsumes S, then the two types are equal.
In the context of subsumption, the type definitions can be expressed using Set-builder notation, which uses a predicate to define a set. Predicates can be defined over a domain . Predicates are partial functions that compare values to selection criteria. For example: "is an integer value greater than or equal to 100 and less than 200?". If a value matches the criteria then the function returns the value. If not, the value is not selected, and nothing is returned.
If there are two predicates, which applies selection criteria for the type T, and which applies additional criteria for the type S, then sets for the two types can be defined:
The predicate is applied alongside as part of the compound predicate S defining. The two predicates are conjoined, so both must be true for a value to be selected. The predicate subsumes the predicate T, so
For example: there is a subfamily of cat species called Felinae, which is part of the family Felidae. The genus Felis, to which the domestic cat species Felis catus belongs, is part of that subfamily.
The conjunction of predicates has been expressed here through application of the second predicate over the domain of values conforming to the first predicate. Viewed as types,.
If T subsumes S then a procedure, function or expression given a value as an operand will therefore be able to operate over that value as one of type T, because. In the example above, we could expect the function ofSubfamily to be applicable to values of all three types Felidae, Felinae and Felis.