Movatterモバイル変換


[0]ホーム

URL:


Jump to content
WikipediaThe Free Encyclopedia
Search

Subtyping

From Wikipedia, the free encyclopedia
Form of type polymorphism
Polymorphism
Ad hoc polymorphism
Parametric polymorphism
Subtyping

Inprogramming language theory,subtyping (also calledsubtype polymorphism orinclusion polymorphism) is a form oftype polymorphism. Asubtype is adatatype that is related to another datatype (thesupertype) by some notion ofsubstitutability, meaning that program elements (typicallysubroutines 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 subtypingrelation (written asS <:T,  ST,[1] or  S ≤:T ) means that any term of type S cansafely be used inany 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 giventype formalism orprogramming language. Thetype system of a programming language essentially defines its own subtyping relation, which may well betrivial, should the language support no (or very little) conversion mechanisms.

Due to the subtyping relation, a term may belong to more than one type. Subtyping is therefore a form of type polymorphism. Inobject-oriented programming the term 'polymorphism' is commonly used to refer solely to thissubtype polymorphism, while the techniques ofparametric polymorphism would be consideredgeneric programming.

Functional programming languages often allow the subtyping ofrecords. 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.[2] 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, supportfunction 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 issystem 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 ofhyponymy andholonymy. It is also related to the concept ofbounded quantification in mathematical logic (seeOrder-sorted logic). 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. In a number of object-oriented languages, subtyping is calledinterface inheritance, with inheritance referred to asimplementation inheritance.

Origins

[edit]

The notion of subtyping in programming languages dates back to the 1960s; it was introduced inSimula derivatives. The first formal treatments of subtyping were given byJohn C. Reynolds in 1980 who usedcategory theory to formalizeimplicit conversions, andLuca Cardelli (1985).[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 theLiskov substitution principle, afterBarbara Liskov who popularized it in akeynote address at a conference on object-oriented programming in 1987. Because it must consider mutable objects, the ideal notion of subtyping defined by Liskov andJeannette Wing, calledbehavioral subtyping is considerably stronger than what can be implemented in atype checker. (See§ Function types below for details.)

Examples

[edit]
Example of subtypes: where bird is the supertype and all others are subtypes as denoted by the arrow inUML notation

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. TheUML 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 (Integer <:Float), or it might define a generic typeNumber as a common supertype of integers and the reals. In this second case, we only haveInteger <:Number andFloat <:Number, butInteger andFloat are not subtypes of each other.

Programmers may take advantage of subtypingto write code in a more abstract manner than would be possible without it. Consider the following example:

functionmax(xasNumber,yasNumber)isifx<ythenreturnyelsereturnxend

If integer and real are both subtypes ofNumber, 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 (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. Rewriting this function so that it would only accept 'x' and 'y' of the same type requiresbounded polymorphism.

Subtyping enables a given type to be substituted for another type or abstraction. Subtyping is said to establish anis-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++

[edit]

The following C++ code establishes an explicit inheritance relationship between classesB andA, whereB is both a subclass and a subtype ofA, and can be used as anA wherever aB is specified (via a reference, a pointer or the object itself).

classA{public:voidmethodOfA()const{// ...}};classB:publicA{public:voidmethodOfB()const{// ...}};voidfunctionOnA(constA&a){a.methodOfA();}intmain(){Bb;functionOnA(b);// b can be substituted for an A.}

[5]

Python

[edit]

The following python code establishes an explicit inheritance relationship between classesB andA, whereB is both a subclass and a subtype ofA, and can be used as anA wherever aB is required.

classA:defmethod_of_a(self)->None:passclassB(A):defmethod_of_b(self)->None:passdeffunction_on_a(a:A)->None:a.method_of_a()if__name__=="__main__":b:B=B()function_on_a(b)# b can be substituted for an A.

The following example,type(a) is a "regular" type, andtype(type(a)) is a metatype. While as distributed all types have the same metatype (PyType_Type, which is also its own metatype), this is not a requirement. The type of classic classes, known astypes.ClassType, can also be considered a distinct metatype.[6]

a = 0print(type(a))# prints: <type 'int'>print(type(type(a)))# prints: <type 'type'>print(type(type(type(a))))# prints: <type 'type'>print(type(type(type(type(a)))))# prints: <type 'type'>

Java

[edit]

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 andimplements clauses.

Using theCollections classes,ArrayList<E> implementsList<E>, andList<E> extendsCollection<E>. SoArrayList<String> is a subtype ofList<String>, which is a subtype ofCollection<String>. The subtyping relationship is preserved between the types automatically. When defining an interface,PayloadList, that associates an optional value ofgeneric type P with each element, its declaration might look like:

interfacePayloadList<E,P>extendsList<E>{voidsetPayload(intindex,Pval);...}

The following parameterizations of PayloadList are subtypes ofList<String>:

PayloadList<String,String>PayloadList<String,Integer>PayloadList<String,Exception>

Subsumption

[edit]

In type theory the concept ofsubsumption[7] is used to define or evaluate whether a typeS is a subtype of typeT.

A type is a set of values. The set can be describedextensionally by listing all the values, or it can be describedintensionally 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 (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.

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".[citation needed]

  • A typeTsubsumesS if the set of valuesT which it defines, is a superset of the setS, so that every member ofS is also a member ofT.
  • A type may be subsumed by more than one type: the supertypes ofS intersect atS.
  • IfS <: T (and thereforeST), thenT, the predicate which circumscribes the setT, must be part of the predicateS (over the same domain) which definesS.
  • IfS subsumesT, andT subsumesS, then the two types are equal (although they may not be the same type if the type system distinguishes types by name).

In 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. This may increase the applicability, orrelevance 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 theprevalence 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 usingSet-builder notation, which uses a predicate to define a set. Predicates can be defined over a domain (set of possible values)D. 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. (List comprehensions are a form of this pattern used in many programming languages.)

If there are two predicates,PT{\displaystyle P_{T}} which applies selection criteria for the typeT, andPs{\displaystyle P_{s}} which applies additional criteria for the typeS, then sets for the two types can be defined:

T={vD PT(v)}{\displaystyle T=\{v\in D\mid \ P_{T}(v)\}}
S={vD PT(v) and Ps(v)}{\displaystyle S=\{v\in D\mid \ P_{T}(v){\text{ and }}P_{s}(v)\}}

The predicateT=PT{\displaystyle \mathbf {T} =P_{T}} is applied alongsidePs{\displaystyle P_{s}} as part of the compound predicateS definingS. The two predicates areconjoined, so both must be true for a value to be selected. The predicateS=TPs=PTPs{\displaystyle \mathbf {S} =\mathbf {T} \land P_{s}=P_{T}\land P_{s}} subsumes the predicateT, soS <: T.

For example: there is a subfamily of cat species calledFelinae, which is part of the familyFelidae. The genusFelis, to which the domestic cat speciesFelis catus belongs, is part of that subfamily.

Felinae={catFelidae ofSubfamily(cat,felinaeSubfamilyName)}{\displaystyle {\mathit {Felinae=\{cat\in Felidae\mid \ ofSubfamily(cat,felinaeSubfamilyName)\}}}}
Felis={catFelinae ofGenus(cat,felisGenusName)}{\displaystyle {\mathit {Felis=\{cat\in Felinae\mid \ ofGenus(cat,felisGenusName)\}}}}

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,Felis <: Felinae <: Felidae.

IfT subsumesS (T :> S) then a procedure, function or expression given a valuesS{\displaystyle s\in S} as an operand (parameter value or term) will therefore be able to operate over that value as one of typeT, becausesT{\displaystyle s\in T}. In the example above, we could expect the functionofSubfamily to be applicable to values of all three typesFelidae,Felinae andFelis.

Subtyping schemes

[edit]

Type theorists make a distinction betweennominal subtyping, in which only types declared in a certain way may be subtypes of each other, andstructural subtyping, in which the structure of two types determines whether or not one is a subtype of the other. The class-based object-oriented subtyping described above is nominal; a structural subtyping rule for an object-oriented language might say that if objects of typeA can handle all of the messages that objects of typeB can handle (that is, if they define all the samemethods), thenA is a subtype ofB regardless of whether eitherinherits from the other. This so-calledduck typing is common in dynamically typed object-oriented languages. Sound structural subtyping rules for types other than object types are also well known.[citation needed]

Implementations of programming languages with subtyping fall into two general classes:inclusive implementations, in which the representation of any value of typeA also represents the same value at typeB ifA <: B, andcoercive implementations, in which a value of typeA can beautomatically converted into one of typeB. The 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.

In almost all type systems that define a subtyping relation, it is reflexive (meaningA <: A for any typeA) and transitive (meaning that ifA <: B andB <: C thenA <: C). This makes it apreorder on types.

Record types

[edit]

Width and depth subtyping

[edit]

Types ofrecords give rise to the concepts ofwidth anddepth subtyping. These express two different ways of obtaining a new type of record that allows the same operations as the original record type.

Recall that a record is a collection of (named) fields. Since 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.

One kind of way to achieve such support, calledwidth subtyping, adds more fields to the record. More formally, every (named) field appearing in the width supertype will appear in the width subtype. Thus, any operation feasible on the supertype will be supported by the subtype.

The second method, calleddepth subtyping, replaces the various fields with their subtypes. That is, the fields of the subtype are subtypes of the fields of the supertype. Since 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. 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 (seeVariance).

Subtyping of records can be defined inSystem F<:, which combinesparametric polymorphism with subtyping of record types and is a theoretical basis for manyfunctional programming languages that support both features.

Some systems also support subtyping of labeleddisjoint union types (such asalgebraic data types). The rule for width subtyping is reversed: every tag appearing in the width subtype must appear in the width supertype.

Function types

[edit]

IfT1T2 is afunction type, then a subtype of it is any function typeS1S2 with the property thatT1 <:S1 andS2 <:T2. This can be summarised using the followingtyping rule:

T1≤:S1S2≤:T2S1S2≤:T1T2{\displaystyle {T_{1}\leq :S_{1}\quad S_{2}\leq :T_{2}} \over {S_{1}\rightarrow S_{2}\leq :T_{1}\rightarrow T_{2}}}

The parameter type ofS1S2 is said to becontravariant because the subtyping relation is reversed for it, whereas the return type iscovariant. Informally, this reversal occurs because the refined type is "more liberal" in the types it accepts and "more conservative" in the type it returns. This is what exactly works inScala: an-ary function is internally a class that inherits theFunctionN(A1,A2,,An,+B){\displaystyle {\mathtt {Function_{N}({-A_{1}},{-A_{2}},\dots ,{-A_{n}},{+B})}}}trait (which can be seen as a generalinterface inJava-like languages), whereA1,A2,,An{\displaystyle {\mathtt {A_{1},A_{2},\dots ,A_{n}}}} are the parameter types, andB{\displaystyle {\mathtt {B}}} is its return type; "−" before the type means the type is contravariant while "+" means covariant.

In 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. Liskov's work in this area focused onbehavioral subtyping, which besides the type system safety discussed in this article also requires that subtypes preserve allinvariants guaranteed by the supertypes in somecontract.[8] This definition of subtyping is generallyundecidable, so it cannot be verified by atype checker.

The subtyping ofmutable references is similar to the treatment of parameter values and return values. Write-only references (orsinks) are contravariant, like parameter values; read-only references (orsources) are covariant, like return values. Mutable references which act as both sources and sinks are invariant.

Relationship with inheritance

[edit]

Subtyping and inheritance are independent (orthogonal) relationships. They may coincide, but none is a special case of the other. In other words, between two typesS andT, all combinations of subtyping and inheritance are possible:

  1. S is neither a subtype nor a derived type ofT
  2. S is a subtype but is not a derived type ofT
  3. S is not a subtype but is a derived type ofT
  4. S is both a subtype and a derived type ofT

The first case is illustrated by independent types, such asBoolean andFloat.

The second case can be illustrated by the relationship betweenInt32 andInt64. In most object oriented programming languages,Int64 are unrelated by inheritance toInt32. HoweverInt32 can be considered a subtype ofInt64 since any 32 bit integer value can be promoted into a 64 bit integer value.

This articlepossibly containsoriginal research. Pleaseimprove it byverifying the claims made and addinginline citations. Statements consisting only of original research should be removed.(July 2022) (Learn how and when to remove this message)

The third case is a consequence offunction subtyping input contravariance. Assume a super class of typeT having a methodm returning an object of the same type (i.e. the type ofm isTT, also note that the first parameter ofm is this/self) and a derived class typeS fromT. By inheritance, the type ofm inS isSS.[citation needed] In order forS to be a subtype ofT the type ofm inS must be a subtype of the type ofm inT[citation needed], in other words:SS ≤:TT. By bottom-up application of the function subtyping rule, this means:S ≤:T andT ≤:S, which is only possible ifS andT are the same. Since inheritance is an irreflexive relation,S can't be a subtype ofT.

Subtyping 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 .[3]

Coercions

[edit]

In coercive subtyping systems, subtypes are defined by explicittype conversion functions from subtype to supertype. For each subtyping relationship (S <:T), a coercion functioncoerce:ST is provided, and any objects of typeS is regarded as the objectcoerceST(s) of typeT. A coercion function may be defined by composition: ifS <:T andT <:U thens may be regarded as an object of typeu under the compound coercion (coerceTUcoerceST). Thetype coercion from a type to itselfcoerceTT is theidentity functionidT.

Coercion functions for records anddisjoint 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. The type coercion for function types may be given byf'(t) =coerceS2T2(f(coerceT1S1(t))), reflecting thecontravariance of parameter values and covariance of return values.

The coercion function is uniquely determined given the subtype andsupertype. Thus, when multiple subtyping relationships are defined, one must be careful to guarantee that all type coercions are coherent. For 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 coercioncoercefloatfloat given bycoerceintfloatcoercefloatint would then be distinct from the identity coercionidfloat.

See also

[edit]
The WikibookAda Programming has a page on the topic of:Subtypes

Notes

[edit]
  1. ^Copestake, Ann. Implementing typed feature structure grammars. Vol. 110. Stanford: CSLI publications, 2002.
  2. ^Cardelli, Luca. A semantics of multiple inheritance. In G. Kahn, D. MacQueen, and G. Plotkin, editors, Semantics of Data Types, volume 173 of Lecture Notes in Computer Science, pages 51–67. Springer-Verlag, 1984. Full version in Information and Computation, 76(2/3):138–164, 1988.
  3. ^abCook, Hill & Canning 1990.
  4. ^Pierce, ch. 15 notes
  5. ^Mitchell, John (2002). "10 "Concepts in object-oriented languages"".Concepts in programming language. Cambridge, UK: Cambridge University Press. p. 287.ISBN 0-521-78098-5.
  6. ^Guido van Rossum."Subtyping Built-in Types". Retrieved2 October 2012.
  7. ^Benjamin C. Pierce,Types and Programming Languages, MIT Press, 2002, 15.1 "Subsumption", p. 181-182
  8. ^Barbara Liskov, Jeannette Wing,A behavioral notion of subtyping, ACM Transactions on Programming Languages and Systems, Volume 16, Issue 6 (November 1994), pp. 1811–1841. An updated version appeared as CMU technical report:Liskov, Barbara;Wing, Jeannette (July 1999)."Behavioral Subtyping Using Invariants and Constraints"(PS). Retrieved2006-10-05.

References

[edit]

Textbooks

  • Benjamin C. Pierce,Types and programming languages, MIT Press, 2002,ISBN 0-262-16209-1, chapter 15 (subtyping of record types), 19.3 (nominal vs. structural types and subtyping), and 23.2 (varieties of polymorphism)
  • C. Szyperski, D. Gruntz, S. Murer,Component software: beyond object-oriented programming, 2nd ed., Pearson Education, 2002,ISBN 0-201-74572-0, pp. 93–95 (a high-level presentation aimed at programming language users)

Papers

Cook, William R.; Hill, Walter; Canning, Peter S. (1990).Inheritance is not subtyping. Proc. 17th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages (POPL). pp. 125–135.CiteSeerX 10.1.1.102.8635.doi:10.1145/96709.96721.ISBN 0-89791-343-4.
  • Reynolds, John C. Using category theory to design implicit conversions and generic operators. In N. D. Jones, editor, Proceedings of the Aarhus Workshop on Semantics-Directed Compiler Generation, number 94 in Lecture Notes in Computer Science. Springer-Verlag, January 1980. Also in Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design (MIT Press, 1994).

Further reading

[edit]
Uninterpreted
Numeric
Pointer
Text
Composite
Other
Related
topics
Retrieved from "https://en.wikipedia.org/w/index.php?title=Subtyping&oldid=1317182842"
Categories:
Hidden categories:

[8]ページ先頭

©2009-2025 Movatter.jp