Subtyping

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.

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.

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.

Subtyping should not be confused with the notion of (class or object) inheritance from object-oriented languages;[3] 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.

The notion of subtyping in programming languages dates back to the 1960s; it was introduced in Simula derivatives.

[4] The concept of subtyping has gained visibility (and synonymy with polymorphism in some circles) 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.

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.

Programmers may take advantage of subtyping to write code in a more abstract manner than would be possible without it.

Rewriting this function so that it would only accept 'x' and 'y' of the same type requires bounded polymorphism.

In common programming languages enumeration types are defined extensionally by listing values.

In discussing the concept of subsumption, the set of values of a type is indicated by writing its name in mathematical italics: T. 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".

This may increase the applicability, or relevance of the subtype (the number of situations where it can be accepted or introduced), as compared to its "more general" supertypes.

The disadvantage of having this more detailed information is that it represents incorporated choices which reduce the prevalence of the subtype (the number of situations which are able to generate or produce it).

In the context of subsumption, the type definitions can be expressed using Set-builder notation, which uses a predicate to define a set.

subsumes the predicate T, so S <: T. For example: there is a subfamily of cat species called Felinae, which is part of the family Felidae.

In the example above, we could expect the function ofSubfamily to be applicable to values of all three types Felidae, Felinae and Felis.

Types of records give rise to the concepts of width and depth subtyping.

One kind of way to achieve such support, called width subtyping, adds more fields to the record.

Depth subtyping only makes sense for immutable records: for example, you can assign 1.5 to the 'x' field of a real point (a record with two real fields), but you can't do the same to the 'x' field of an integer point (which, however, is a deep subtype of the real point type) because 1.5 is not an integer (see Variance).

Subtyping of records can be defined in System F<:, which combines parametric polymorphism with subtyping of record types and is a theoretical basis for many functional programming languages that support both features.

This is what exactly works in Scala: a n-ary function is internally a class that inherits the

Liskov's work in this area focused on behavioral subtyping, which besides the type system safety discussed in this article also requires that subtypes preserve all invariants guaranteed by the supertypes in some contract.

[6] This definition of subtyping is generally undecidable, so it cannot be verified by a type checker.

For each subtyping relationship (S <: T), a coercion function coerce: S → T is provided, and any object s of type S is regarded as the object coerceS → T(s) of type T. A coercion function may be defined by composition: if S <: T and T <: U then s may be regarded as an object of type u under the compound coercion (coerceT → U ∘ coerceS → T).

Coercion functions for records and disjoint union subtypes may be defined componentwise; in the case of width-extended records, type coercion simply discards any components which are not defined in the supertype.

Thus, when multiple subtyping relationships are defined, one must be careful to guarantee that all type coercions are coherent.