{"history":[],"article":{"id":"a5fe982a-d8e2-4445-913a-c94145cc9c38","title":"Subtyping","slug":"subtyping","content":":::summary\n:::\n\n# \nIn [programming language theory](https://bliptext.com/articles/programming-language-theory), **subtyping** (also called **sub[type polymorphism](https://bliptext.com/articles/polymorphism-computer-science)** or **inclusion polymorphism**) is a form of [type polymorphism](https://bliptext.com/articles/polymorphism-computer-science).\nA **subtype** is a [datatype](https://bliptext.com/articles/datatype) that is related to another [datatype](https://bliptext.com/articles/datatype) (the **supertype**) by some notion of [substitutability](https://bliptext.com/articles/substitutability), meaning that program elements (typically [subroutines](https://bliptext.com/articles/subroutines) or functions), written to operate on elements of the **supertype**, can also operate on elements of the **subtype**.\nIf S is a subtype of T, the subtyping [relation](https://bliptext.com/articles/binary-relation) (written as\nS <: T\n,\nS ⊑ T\n, or\nS ≤: T\n) 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](https://bliptext.com/articles/formal-language) or [programming language](https://bliptext.com/articles/programming-language). The [type system](https://bliptext.com/articles/type-system) of a [programming language](https://bliptext.com/articles/programming-language) essentially defines its own subtyping relation, which may well be [trivial](https://bliptext.com/articles/identity-relation), should the language support no (or very little) conversion mechanisms.\nDue to the subtyping relation, a term may belong to more than one type.\nSubtyping is therefore a form of type polymorphism.\nIn [object-oriented programming](https://bliptext.com/articles/object-oriented-programming) the term 'polymorphism' is commonly used to refer solely to this subtype polymorphism, while the techniques of [parametric polymorphism](https://bliptext.com/articles/parametric-polymorphism) would be considered [generic programming](https://bliptext.com/articles/generic-programming).\n[Functional programming languages](https://bliptext.com/articles/functional-programming-languages) often allow the subtyping of [records](https://bliptext.com/articles/record-computer-science).\nConsequently, [simply typed lambda calculus](https://bliptext.com/articles/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.\nBecause the resulting calculus allows terms to have more than one type, it is no longer a \"simple\" [type theory](https://bliptext.com/articles/type-theory).\nSince functional programming languages, by definition, support [function literals](https://bliptext.com/articles/function-literals), which can also be stored in records, records types with subtyping provide some of the features of object-oriented programming.\nTypically, functional programming languages also provide some, usually restricted, form of parametric polymorphism.\nIn a theoretical setting, it is desirable to study the interaction of the two features; a common theoretical setting is [system F<:](https://bliptext.com/articles/system-f-sub).\nVarious calculi that attempt to capture the theoretical properties of object-oriented programming may be derived from system F<:.\nThe concept of subtyping is related to the linguistic notions of [hyponymy](https://bliptext.com/articles/hyponymy) and [holonymy](https://bliptext.com/articles/holonymy).\nIt is also related to the concept of [bounded quantification](https://bliptext.com/articles/bounded-quantification) in mathematical logic (see [Order-sorted logic](https://bliptext.com/articles/order-sorted-logic)).\nSubtyping should not be confused with the notion of (class or object) [inheritance](https://bliptext.com/articles/inheritance-object-oriented-programming) from object-oriented languages; subtyping is a relation between types (interfaces in object-oriented parlance) whereas [inheritance](https://bliptext.com/articles/inheritance-object-oriented-programming) is a relation between implementations stemming from a language feature that allows new objects to be created from existing ones.\nIn a number of object-oriented languages, subtyping is called **interface inheritance**, with inheritance referred to as implementation inheritance.\n\n# Origins\nThe notion of subtyping in programming languages dates back to the 1960s; it was introduced in [Simula](https://bliptext.com/articles/simula) derivatives.\nThe first formal treatments of subtyping were given by [John C. Reynolds](https://bliptext.com/articles/john-c-reynolds) in 1980 who used [category theory](https://bliptext.com/articles/category-theory) to formalize [implicit conversions](https://bliptext.com/articles/implicit-conversion), and [Luca Cardelli](https://bliptext.com/articles/luca-cardelli) (1985).\nThe concept of subtyping has gained visibility (and synonymy with polymorphism in some circles) with the mainstream adoption of object-oriented programming.\nIn this context, the principle of safe substitution is often called the [Liskov substitution principle](https://bliptext.com/articles/liskov-substitution-principle), after [Barbara Liskov](https://bliptext.com/articles/barbara-liskov) who popularized it in a [keynote](https://bliptext.com/articles/keynote) address at a conference on object-oriented programming in 1987.\nBecause it must consider mutable objects, the ideal notion of subtyping defined by Liskov and [Jeannette Wing](https://bliptext.com/articles/jeannette-wing), called [behavioral subtyping](https://bliptext.com/articles/behavioral-subtyping) is considerably stronger than what can be implemented in a [type checker](https://bliptext.com/articles/type-checker).\n(See below for details.)\n\n# Examples\nA simple practical example of subtypes is shown in the diagram.\nThe type \"bird\" has three subtypes \"duck\", \"cuckoo\" and \"ostrich\".\nConceptually, each of these is a variety of the basic type \"bird\" that inherits many \"bird\" characteristics but has some specific differences.\nThe [UML](https://bliptext.com/articles/unified-modeling-language) notation is used in this diagram, with open-headed arrows showing the direction and type of the relationship between the supertype and its subtypes.\nAs 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.\nIn this second case, we only have <: and <: , but and are not subtypes of each other.\nProgrammers may take advantage of subtyping [to write code in a more abstract manner](https://bliptext.com/articles/abstraction-principle-programming) than would be possible without it.\nConsider the following example:\nIf integer and real are both subtypes of, 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.\nHowever, the very possibility of implementing such an operator highly constrains the Number type (for example, one can't compare an integer with a complex number), and actually only comparing integers with integers, and reals with reals, makes sense.\nRewriting this function so that it would only accept 'x' and 'y' of the same type requires [bounded polymorphism](https://bliptext.com/articles/bounded-polymorphism).\n# [Example of subtypes: where bird is the supertype and all others are subtypes as denoted by the arrow in UML notation | upload.wikimedia.org/wikipedia/commons/d/d1/Inheritance.svg]\n\n# Subsumption\nIn type theory the concept of subsumption is used to define or evaluate whether a type **S** is a subtype of type **T**.\nA type is a set of values.\nThe 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.\nIn common programming languages enumeration types are defined extensionally by listing values.\n[User-defined types](https://bliptext.com/articles/user-defined-type) like records (structs, interfaces) 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.\nIn discussing the concept of subsumption, the set of values of a type is indicated by writing its name in mathematical italics: **T**. **T**he type, viewed as a predicate over a domain, is indicated by writing its name in bold: **T**.\nThe conventional symbol **<:** means \"is a subtype of\", and **:>** means \"is a supertype of\".\nS ⊆ T\n), then **T**, the predicate which circumscribes the set **T**, must be part of the predicate **S** (over the same domain) which defines **S**.\nIn terms of information specificity, a subtype is considered more specific than any one of its supertypes, because it holds at least as much information as each of them.\nThis 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.\nThe 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).\nIn the context of subsumption, the type definitions can be expressed using [Set-builder notation](https://bliptext.com/articles/set-builder-notation), which uses a predicate to define a set.\nPredicates can be defined over a domain (set of possible values) D. Predicates are partial functions that compare values to selection criteria.\nFor example: \"is an integer value greater than or equal to 100 and less than 200?\".\nIf a value matches the criteria then the function returns the value.\nIf not, the value is not selected, and nothing is returned.\n(List comprehensions are a form of this pattern used in many programming languages.)\nIf there are two predicates, P_**T** which applies selection criteria for the type **T**, and P_s which applies additional criteria for the type **S**, then sets for the two types can be defined:\nThe predicate is applied alongside P_s as part of the compound predicate **S** defining **S**. The two predicates are conjoined, so both must be true for a value to be selected.\n**T**he predicate subsumes the predicate **T**, so S <: **T**.\nFor example: there is a subfamily of cat species called Felinae, which is part of the family Felidae.\nThe genus Felis, to which the domestic cat species Felis catus belongs, is part of that subfamily.\nThe conjunction of predicates has been expressed here through application of the second predicate over the domain of values conforming to the first predicate.\nViewed as types, Felis <: Felinae <: Felidae.\nIf ****T**** subsumes **S** (****T**** :> **S**) then a procedure, function or expression given a value s \\in **S** as an operand (parameter value or term) will therefore be able to operate over that value as one of type ****T****, because s \\in ****T****. In the example above, we could expect the function of**S**ubfamily to be applicable to values of all three types **Felidae**, **Felinae** and **Felis**.\n\n# Subtyping schemes\nType theorists make a distinction between **[nominal subtyping](https://bliptext.com/articles/nominal-type-system)**, in which only types declared in a certain way may be subtypes of each other, and **[structural subtyping](https://bliptext.com/articles/structural-type-system)**, in which the structure of two types determines whether or not one is a subtype of the other.\nThe class-based object-oriented subtyping described above is nominal; a structural subtyping rule for an object-oriented language might say that if objects of type A can handle all of the messages that objects of type B can handle (that is, if they define all the same [methods](https://bliptext.com/articles/method-computer-science)), then A is a subtype of B regardless of whether either [inherits](https://bliptext.com/articles/inheritance-object-oriented-programming) from the other.\nThis so-called [duck typing](https://bliptext.com/articles/duck-typing) is common in dynamically typed object-oriented languages.\nSound structural subtyping rules for types other than object types are also well known.\nImplementations of programming languages with subtyping fall into two general classes: inclusive implementations, in which the representation of any value of type A also represents the same value at type B if A <: B, and coercive implementations, in which a value of type A can be automatically converted into one of type B.\nThe subtyping induced by subclassing in an object-oriented language is usually inclusive; subtyping relations that relate integers and floating-point numbers, which are represented differently, are usually coercive.\nIn almost all type systems that define a subtyping relation, it is reflexive (meaning A <: A for any type A) and transitive (meaning that if A <: B and B <: C then A <: C).\nThis makes it a [preorder](https://bliptext.com/articles/preorder) on types.\n\n# Record types\n\n## Width and depth subtyping\nTypes of [records](https://bliptext.com/articles/record-computer-science) give rise to the concepts of width and depth subtyping.\nThese express two different ways of obtaining a new type of record that allows the same operations as the original record type.\nRecall that a record is a collection of (named) fields.\nSince a subtype is a type which allows all operations allowed on the original type, a record subtype should support the same operations on the fields as the original type supported.\nOne kind of way to achieve such support, called width subtyping, adds more fields to the record.\nMore formally, every (named) field appearing in the width supertype will appear in the width subtype.\nThus, any operation feasible on the supertype will be supported by the subtype.\nThe second method, called depth subtyping, replaces the various fields with their subtypes.\nThat is, the fields of the subtype are subtypes of the fields of the supertype.\nSince any operation supported for a field in the supertype is supported for its subtype, any operation feasible on the record supertype is supported by the record subtype.\nDepth 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](https://bliptext.com/articles/covariance-and-contravariance-computer-science)).\nSubtyping of records can be defined in [System F<:](https://bliptext.com/articles/system-f-sub), which combines [parametric polymorphism](https://bliptext.com/articles/parametric-polymorphism) with subtyping of record types and is a theoretical basis for many [functional programming languages](https://bliptext.com/articles/functional-programming-languages) that support both features.\nSome systems also support subtyping of labeled [disjoint union](https://bliptext.com/articles/disjoint-union) types (such as [algebraic data types](https://bliptext.com/articles/algebraic-data-type)).\nThe rule for width subtyping is reversed: every tag appearing in the width subtype must appear in the width supertype.\n\n# Function types\nIf\nT1 → T2\nis a function type, then a subtype of it is any function type\nS1 → S2\nwith the property that\nT1 <: S1\nand\nS2 <: T2.\nThis can be summarised using the following [typing rule](https://bliptext.com/articles/typing-rule):\nThe parameter type of\nS1 → S2\nis said to be [contravariant](https://bliptext.com/articles/covariance-and-contravariance-computer-science) because the subtyping relation is reversed for it, whereas the return type is [covariant](https://bliptext.com/articles/covariance-and-contravariance-computer-science).\nInformally, this reversal occurs because the refined type is \"more liberal\" in the types it accepts and \"more conservative\" in the type it returns.\nThis is what exactly works in [Scala](https://bliptext.com/articles/scala-programming-language): a n-ary function is internally a class that inherits the [trait](https://bliptext.com/articles/trait-computer-programming) (which can be seen as a general [interface](https://bliptext.com/articles/application-programming-interface) in [Java](https://bliptext.com/articles/java-programming-language)-like languages), where are the parameter types, and \\mathtt{B} is its return type; \"−\" before the type means the type is contravariant while \"+\" means covariant.\nIn languages that allow side effects, like most object-oriented languages, subtyping is generally not sufficient to guarantee that a function can be safely used in the context of another.\nLiskov's work in this area focused on [behavioral subtyping](https://bliptext.com/articles/behavioral-subtyping), which besides the type system safety discussed in this article also requires that subtypes preserve all [invariants](https://bliptext.com/articles/invariant-computer-science) guaranteed by the supertypes in some [contract](https://bliptext.com/articles/design-by-contract).\nThis definition of subtyping is generally [undecidable](https://bliptext.com/articles/undecidable-problem), so it cannot be verified by a [type checker](https://bliptext.com/articles/type-checker).\nThe subtyping of [mutable references](https://bliptext.com/articles/immutable-object) is similar to the treatment of parameter values and return values.\nWrite-only references (or sinks) are contravariant, like parameter values; read-only references (or sources) are covariant, like return values.\nMutable references which act as both sources and sinks are invariant.\n\n# Relationship with inheritance\nSubtyping and inheritance are independent (orthogonal) relationships.\nThey may coincide, but none is a special case of the other.\nIn other words, between two types S and T, all combinations of subtyping and inheritance are possible:\nThe first case is illustrated by independent types, such as and.\nThe second case can be illustrated by the relationship between and.\nIn most object oriented programming languages, are unrelated by inheritance to.\nHowever can be considered a subtype of since any 32 bit integer value can be promoted into a 64 bit integer value.\nThe third case is a consequence of [function subtyping input contravariance](https://bliptext.com/articles/subtyping-of-functions).\nAssume a super class of type T having a method m returning an object of the same type (i.e. the type of m is T → T, also note that the first parameter of m is this/self) and a derived class type S from T.\nBy inheritance, the type of m in S is S → S.\nIn order for S to be a subtype of T the type of m in S must be a subtype of the type of m in T, in other words: S → S ≤: T → T.\nBy bottom-up application of the function subtyping rule, this means: S ≤: T and T ≤: S, which is only possible if S and T are the same.\nSince inheritance is an irreflexive relation, S can't be a subtype of T.\nSubtyping and inheritance are compatible when all inherited fields and methods of the derived type have types which are subtypes of the corresponding fields and methods from the inherited type.\n\n# Coercions\nIn coercive subtyping systems, subtypes are defined by implicit [type conversion](https://bliptext.com/articles/type-conversion) functions from subtype to supertype.\nFor 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.\nA 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).\nThe [type coercion](https://bliptext.com/articles/type-coercion) from a type to itself coerceT → T is the [identity function](https://bliptext.com/articles/identity-function) idT.\nCoercion functions for records and [disjoint union](https://bliptext.com/articles/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.\nThe type coercion for function types may be given by f'(t) = coerceS 2 → T2 (f(coerceT 1 → S1 (t))), reflecting the [contravariance](https://bliptext.com/articles/covariance-and-contravariance-computer-science) of parameter values and covariance of return values.\nThe coercion function is uniquely determined given the subtype and [supertype](https://bliptext.com/articles/supertype).\nThus, when multiple subtyping relationships are defined, one must be careful to guarantee that all type coercions are coherent.\nFor instance, if an integer such as 2 : int can be coerced to a floating point number (say, 2.0 : float), then it is not admissible to coerce 2.1 : float to 2 : int, because the compound coercion coercefloat → float given by coerceint → float ∘ coercefloat → int would then be distinct from the identity coercion idfloat.","current_revision":null,"created_by":"kACnuQmH5k9Nr5VNVEpVeg7XpvUmMctD","created_at":"2025-01-25T18:42:51.203Z","updated_at":"2025-01-25T18:42:51.203Z","search_vector":"'subtyp':1","search_content":" \n \n\n# \nIn [programming language theory](https://bliptext.com/articles/programming-language-theory), **subtyping** (also called **sub[type polymorphism](https://bliptext.com/articles/polymorphism-computer-science)** or **inclusion polymorphism**) is a form of [type polymorphism](https://bliptext.com/articles/polymorphism-computer-science).\nA **subtype** is a [datatype](https://bliptext.com/articles/datatype) that is related to another [datatype](https://bliptext.com/articles/datatype) (the **supertype**) by some notion of [substitutability](https://bliptext.com/articles/substitutability), meaning that program elements (typically [subroutines](https://bliptext.com/articles/subroutines) or functions), written to operate on elements of the **supertype**, can also operate on elements of the **subtype**.\nIf S is a subtype of T, the subtyping [relation](https://bliptext.com/articles/binary-relation) (written as\nS <: T\n,\nS ⊑ T\n, or\nS ≤: T\n) 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](https://bliptext.com/articles/formal-language) or [programming language](https://bliptext.com/articles/programming-language). The [type system](https://bliptext.com/articles/type-system) of a [programming language](https://bliptext.com/articles/programming-language) essentially defines its own subtyping relation, which may well be [trivial](https://bliptext.com/articles/identity-relation), should the language support no (or very little) conversion mechanisms.\nDue to the subtyping relation, a term may belong to more than one type.\nSubtyping is therefore a form of type polymorphism.\nIn [object-oriented programming](https://bliptext.com/articles/object-oriented-programming) the term 'polymorphism' is commonly used to refer solely to this subtype polymorphism, while the techniques of [parametric polymorphism](https://bliptext.com/articles/parametric-polymorphism) would be considered [generic programming](https://bliptext.com/articles/generic-programming).\n[Functional programming languages](https://bliptext.com/articles/functional-programming-languages) often allow the subtyping of [records](https://bliptext.com/articles/record-computer-science).\nConsequently, [simply typed lambda calculus](https://bliptext.com/articles/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.\nBecause the resulting calculus allows terms to have more than one type, it is no longer a \"simple\" [type theory](https://bliptext.com/articles/type-theory).\nSince functional programming languages, by definition, support [function literals](https://bliptext.com/articles/function-literals), which can also be stored in records, records types with subtyping provide some of the features of object-oriented programming.\nTypically, functional programming languages also provide some, usually restricted, form of parametric polymorphism.\nIn a theoretical setting, it is desirable to study the interaction of the two features; a common theoretical setting is [system F<:](https://bliptext.com/articles/system-f-sub).\nVarious calculi that attempt to capture the theoretical properties of object-oriented programming may be derived from system F<:.\nThe concept of subtyping is related to the linguistic notions of [hyponymy](https://bliptext.com/articles/hyponymy) and [holonymy](https://bliptext.com/articles/holonymy).\nIt is also related to the concept of [bounded quantification](https://bliptext.com/articles/bounded-quantification) in mathematical logic (see [Order-sorted logic](https://bliptext.com/articles/order-sorted-logic)).\nSubtyping should not be confused with the notion of (class or object) [inheritance](https://bliptext.com/articles/inheritance-object-oriented-programming) from object-oriented languages; subtyping is a relation between types (interfaces in object-oriented parlance) whereas [inheritance](https://bliptext.com/articles/inheritance-object-oriented-programming) is a relation between implementations stemming from a language feature that allows new objects to be created from existing ones.\nIn a number of object-oriented languages, subtyping is called **interface inheritance**, with inheritance referred to as implementation inheritance.\n\n# Origins\nThe notion of subtyping in programming languages dates back to the 1960s; it was introduced in [Simula](https://bliptext.com/articles/simula) derivatives.\nThe first formal treatments of subtyping were given by [John C. Reynolds](https://bliptext.com/articles/john-c-reynolds) in 1980 who used [category theory](https://bliptext.com/articles/category-theory) to formalize [implicit conversions](https://bliptext.com/articles/implicit-conversion), and [Luca Cardelli](https://bliptext.com/articles/luca-cardelli) (1985).\nThe concept of subtyping has gained visibility (and synonymy with polymorphism in some circles) with the mainstream adoption of object-oriented programming.\nIn this context, the principle of safe substitution is often called the [Liskov substitution principle](https://bliptext.com/articles/liskov-substitution-principle), after [Barbara Liskov](https://bliptext.com/articles/barbara-liskov) who popularized it in a [keynote](https://bliptext.com/articles/keynote) address at a conference on object-oriented programming in 1987.\nBecause it must consider mutable objects, the ideal notion of subtyping defined by Liskov and [Jeannette Wing](https://bliptext.com/articles/jeannette-wing), called [behavioral subtyping](https://bliptext.com/articles/behavioral-subtyping) is considerably stronger than what can be implemented in a [type checker](https://bliptext.com/articles/type-checker).\n(See below for details.)\n\n# Examples\nA simple practical example of subtypes is shown in the diagram.\nThe type \"bird\" has three subtypes \"duck\", \"cuckoo\" and \"ostrich\".\nConceptually, each of these is a variety of the basic type \"bird\" that inherits many \"bird\" characteristics but has some specific differences.\nThe [UML](https://bliptext.com/articles/unified-modeling-language) notation is used in this diagram, with open-headed arrows showing the direction and type of the relationship between the supertype and its subtypes.\nAs a more practical example, a language might allow integer values to be used wherever floating point values are expected ( ** means \"is a supertype of\".\nS ⊆ T\n), then **T**, the predicate which circumscribes the set **T**, must be part of the predicate **S** (over the same domain) which defines **S**.\nIn terms of information specificity, a subtype is considered more specific than any one of its supertypes, because it holds at least as much information as each of them.\nThis 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.\nThe 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).\nIn the context of subsumption, the type definitions can be expressed using [Set-builder notation](https://bliptext.com/articles/set-builder-notation), which uses a predicate to define a set.\nPredicates can be defined over a domain (set of possible values) D. Predicates are partial functions that compare values to selection criteria.\nFor example: \"is an integer value greater than or equal to 100 and less than 200?\".\nIf a value matches the criteria then the function returns the value.\nIf not, the value is not selected, and nothing is returned.\n(List comprehensions are a form of this pattern used in many programming languages.)\nIf there are two predicates, P_**T** which applies selection criteria for the type **T**, and P_s which applies additional criteria for the type **S**, then sets for the two types can be defined:\nThe predicate is applied alongside P_s as part of the compound predicate **S** defining **S**. The two predicates are conjoined, so both must be true for a value to be selected.\n**T**he predicate subsumes the predicate **T**, so S **S**) then a procedure, function or expression given a value s \\in **S** as an operand (parameter value or term) will therefore be able to operate over that value as one of type ****T****, because s \\in ****T****. In the example above, we could expect the function of**S**ubfamily to be applicable to values of all three types **Felidae**, **Felinae** and **Felis**.\n\n# Subtyping schemes\nType theorists make a distinction between **[nominal subtyping](https://bliptext.com/articles/nominal-type-system)**, in which only types declared in a certain way may be subtypes of each other, and **[structural subtyping](https://bliptext.com/articles/structural-type-system)**, in which the structure of two types determines whether or not one is a subtype of the other.\nThe class-based object-oriented subtyping described above is nominal; a structural subtyping rule for an object-oriented language might say that if objects of type A can handle all of the messages that objects of type B can handle (that is, if they define all the same [methods](https://bliptext.com/articles/method-computer-science)), then A is a subtype of B regardless of whether either [inherits](https://bliptext.com/articles/inheritance-object-oriented-programming) from the other.\nThis so-called [duck typing](https://bliptext.com/articles/duck-typing) is common in dynamically typed object-oriented languages.\nSound structural subtyping rules for types other than object types are also well known.\nImplementations of programming languages with subtyping fall into two general classes: inclusive implementations, in which the representation of any value of type A also represents the same value at type B if A <: B, and coercive implementations, in which a value of type A can be automatically converted into one of type B.\nThe subtyping induced by subclassing in an object-oriented language is usually inclusive; subtyping relations that relate integers and floating-point numbers, which are represented differently, are usually coercive.\nIn almost all type systems that define a subtyping relation, it is reflexive (meaning A <: A for any type A) and transitive (meaning that if A <: B and B <: C then A <: C).\nThis makes it a [preorder](https://bliptext.com/articles/preorder) on types.\n\n# Record types\n\n## Width and depth subtyping\nTypes of [records](https://bliptext.com/articles/record-computer-science) give rise to the concepts of width and depth subtyping.\nThese express two different ways of obtaining a new type of record that allows the same operations as the original record type.\nRecall that a record is a collection of (named) fields.\nSince a subtype is a type which allows all operations allowed on the original type, a record subtype should support the same operations on the fields as the original type supported.\nOne kind of way to achieve such support, called width subtyping, adds more fields to the record.\nMore formally, every (named) field appearing in the width supertype will appear in the width subtype.\nThus, any operation feasible on the supertype will be supported by the subtype.\nThe second method, called depth subtyping, replaces the various fields with their subtypes.\nThat is, the fields of the subtype are subtypes of the fields of the supertype.\nSince any operation supported for a field in the supertype is supported for its subtype, any operation feasible on the record supertype is supported by the record subtype.\nDepth 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](https://bliptext.com/articles/covariance-and-contravariance-computer-science)).\nSubtyping of records can be defined in [System F<:](https://bliptext.com/articles/system-f-sub), which combines [parametric polymorphism](https://bliptext.com/articles/parametric-polymorphism) with subtyping of record types and is a theoretical basis for many [functional programming languages](https://bliptext.com/articles/functional-programming-languages) that support both features.\nSome systems also support subtyping of labeled [disjoint union](https://bliptext.com/articles/disjoint-union) types (such as [algebraic data types](https://bliptext.com/articles/algebraic-data-type)).\nThe rule for width subtyping is reversed: every tag appearing in the width subtype must appear in the width supertype.\n\n# Function types\nIf\nT1 → T2\nis a function type, then a subtype of it is any function type\nS1 → S2\nwith the property that\nT1 <: S1\nand\nS2 <: T2.\nThis can be summarised using the following [typing rule](https://bliptext.com/articles/typing-rule):\nThe parameter type of\nS1 → S2\nis said to be [contravariant](https://bliptext.com/articles/covariance-and-contravariance-computer-science) because the subtyping relation is reversed for it, whereas the return type is [covariant](https://bliptext.com/articles/covariance-and-contravariance-computer-science).\nInformally, this reversal occurs because the refined type is \"more liberal\" in the types it accepts and \"more conservative\" in the type it returns.\nThis is what exactly works in [Scala](https://bliptext.com/articles/scala-programming-language): a n-ary function is internally a class that inherits the [trait](https://bliptext.com/articles/trait-computer-programming) (which can be seen as a general [interface](https://bliptext.com/articles/application-programming-interface) in [Java](https://bliptext.com/articles/java-programming-language)-like languages), where are the parameter types, and \\mathtt{B} is its return type; \"−\" before the type means the type is contravariant while \"+\" means covariant.\nIn languages that allow side effects, like most object-oriented languages, subtyping is generally not sufficient to guarantee that a function can be safely used in the context of another.\nLiskov's work in this area focused on [behavioral subtyping](https://bliptext.com/articles/behavioral-subtyping), which besides the type system safety discussed in this article also requires that subtypes preserve all [invariants](https://bliptext.com/articles/invariant-computer-science) guaranteed by the supertypes in some [contract](https://bliptext.com/articles/design-by-contract).\nThis definition of subtyping is generally [undecidable](https://bliptext.com/articles/undecidable-problem), so it cannot be verified by a [type checker](https://bliptext.com/articles/type-checker).\nThe subtyping of [mutable references](https://bliptext.com/articles/immutable-object) is similar to the treatment of parameter values and return values.\nWrite-only references (or sinks) are contravariant, like parameter values; read-only references (or sources) are covariant, like return values.\nMutable references which act as both sources and sinks are invariant.\n\n# Relationship with inheritance\nSubtyping and inheritance are independent (orthogonal) relationships.\nThey may coincide, but none is a special case of the other.\nIn other words, between two types S and T, all combinations of subtyping and inheritance are possible:\nThe first case is illustrated by independent types, such as and.\nThe second case can be illustrated by the relationship between and.\nIn most object oriented programming languages, are unrelated by inheritance to.\nHowever can be considered a subtype of since any 32 bit integer value can be promoted into a 64 bit integer value.\nThe third case is a consequence of [function subtyping input contravariance](https://bliptext.com/articles/subtyping-of-functions).\nAssume a super class of type T having a method m returning an object of the same type (i.e. the type of m is T → T, also note that the first parameter of m is this/self) and a derived class type S from T.\nBy inheritance, the type of m in S is S → S.\nIn order for S to be a subtype of T the type of m in S must be a subtype of the type of m in T, in other words: S → S ≤: T → T.\nBy bottom-up application of the function subtyping rule, this means: S ≤: T and T ≤: S, which is only possible if S and T are the same.\nSince inheritance is an irreflexive relation, S can't be a subtype of T.\nSubtyping and inheritance are compatible when all inherited fields and methods of the derived type have types which are subtypes of the corresponding fields and methods from the inherited type.\n\n# Coercions\nIn coercive subtyping systems, subtypes are defined by implicit [type conversion](https://bliptext.com/articles/type-conversion) functions from subtype to supertype.\nFor 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.\nA 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).\nThe [type coercion](https://bliptext.com/articles/type-coercion) from a type to itself coerceT → T is the [identity function](https://bliptext.com/articles/identity-function) idT.\nCoercion functions for records and [disjoint union](https://bliptext.com/articles/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.\nThe type coercion for function types may be given by f'(t) = coerceS 2 → T2 (f(coerceT 1 → S1 (t))), reflecting the [contravariance](https://bliptext.com/articles/covariance-and-contravariance-computer-science) of parameter values and covariance of return values.\nThe coercion function is uniquely determined given the subtype and [supertype](https://bliptext.com/articles/supertype).\nThus, when multiple subtyping relationships are defined, one must be careful to guarantee that all type coercions are coherent.\nFor instance, if an integer such as 2 : int can be coerced to a floating point number (say, 2.0 : float), then it is not admissible to coerce 2.1 : float to 2 : int, because the compound coercion coercefloat → float given by coerceint → float ∘ coercefloat → int would then be distinct from the identity coercion idfloat.","revisionCount":0},"hasMore":false,"nextCursor":null}

History