Subtyping

In programming language theory, subtyping (also called subtype polymorphism or inclusion polymorphism) is a form of type polymorphism. 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 (written as S<: T,  S ⊑ T,^[1] or  S ≤: T ) 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 (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. 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.^[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, 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 (see Order-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 called interface inheritance, with inheritance referred to as implementation inheritance.

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 (1985).^[4]

El concepto de subtipado ha ganado visibilidad (y se ha convertido en sinónimo de polimorfismo en algunos círculos) con la adopción generalizada de la programación orientada a objetos. En este contexto, el principio de sustitución segura se conoce a menudo como principio de sustitución de Liskov , en honor a Barbara Liskov, quien lo popularizó en una conferencia magistral sobre programación orientada a objetos en 1987. Dado que debe considerar objetos mutables, la noción ideal de subtipado definida por Liskov y Jeannette Wing , denominada subtipado conductual , es considerablemente más robusta que la que puede implementarse en un verificador de tipos . (Véase la sección «  Tipos de función» más adelante para más detalles).

En el diagrama se muestra un ejemplo práctico y sencillo de subtipos. El tipo "pájaro" tiene tres subtipos: "pato", "cuco" y "avestruz". Conceptualmente, cada uno de ellos es una variedad del tipo básico "pájaro" que hereda muchas de sus características, pero presenta algunas diferencias específicas. En este diagrama se utiliza la notación UML , donde las flechas abiertas indican la dirección y el tipo de relación entre el supertipo y sus subtipos.

Como ejemplo más práctico, un lenguaje podría permitir el uso de valores enteros donde se esperan valores de punto flotante ( Integer<: Float), o podría definir un tipo genérico.Númerocomo un supertipo común de los enteros y los reales. En este segundo caso, solo tenemos Integer<: Numbery Float<: Number, pero Integery Floatno son subtipos uno del otro.

Los programadores pueden aprovechar el subtipado para escribir código de una manera más abstracta de lo que sería posible sin él. Considere el siguiente ejemplo:

función max ( x como Número , y como Número ) es si x < y entonces devolver y sino devolver x fin

Si tanto entero como real son subtipos de Number, y se define un operador de comparación con un Number arbitrario para ambos tipos, entonces se pueden pasar valores de cualquiera de los dos tipos a esta función. Sin embargo, la mera posibilidad de implementar dicho operador restringe mucho el tipo Number (por ejemplo, no se puede comparar un entero con un número complejo), y en realidad solo tiene sentido comparar enteros con enteros y reales con reales. Reescribir esta función para que solo acepte 'x' e 'y' del mismo tipo requiere polimorfismo acotado .

El subtipado permite sustituir un tipo dado por otro tipo o abstracción. Se dice que el subtipado establece una relación de tipo "es un" entre el subtipo y alguna abstracción existente, ya sea implícita o explícitamente, según lo admita el lenguaje. Esta relación puede expresarse explícitamente mediante herencia en lenguajes que la admiten como mecanismo de subtipado.

clase A { público : void métodoDeA () const { // ... } };clase B : público A { público : void métodoDeB () const { // ... } };void functionOnA ( const A & a ) { a . methodOfA (); }int main () { B b ; functionOnA ( b ); // b puede sustituirse por una A. }

clase A : def método_de_a ( self ) -> Ninguno : pasarclase B ( A ): def método_de_b ( self ) -> Ninguno : pasardef function_on_a ( a : A ) -> None : a . method_of_a ()if __name__ == "__main__" : b : B = B () function_on_a ( b ) # b puede sustituirse por una A.

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

interface PayloadList < E , P > extends List < E > { void setPayload ( int index , P val ); ... }

Lista de carga útil < Cadena , Cadena > Lista de carga útil < Cadena , Entero > Lista de carga útil < Cadena , Excepción >

En la teoría de tipos , el concepto de subsunción ^{[ 7 ]} se utiliza para definir o evaluar si un tipo S es un subtipo del tipo T.

Un tipo es un conjunto de valores. Este conjunto puede describirse extensionalmente enumerando todos los valores, o intensionalmente indicando la pertenencia al conjunto mediante un predicado sobre un dominio de valores posibles. En los lenguajes de programación comunes, los tipos de enumeración se definen extensionalmente enumerando valores. Los tipos definidos por el usuario, como los registros (estructuras, interfaces) o las clases, se definen intensionalmente mediante una declaración de tipo explícita o utilizando un valor existente, que codifica información de tipo, como prototipo para ser copiado o extendido.

Al hablar del concepto de subsunción, el conjunto de valores de un tipo se indica escribiendo su nombre en cursiva matemática: T. El tipo, visto como un predicado sobre un dominio, se indica escribiendo su nombre en negrita: T. El símbolo convencional <: significa "es un subtipo de" y :> significa "es un supertipo de".

• Un tipo T engloba a S si el conjunto de valores T que define es un superconjunto del conjunto S , de modo que cada miembro de S es también un miembro de T.
• Un tipo puede estar subsumido por más de un tipo: los supertipos de S se intersecan en S.
• Si S <: T (y por lo tanto S ⊆ T ), entonces T , el predicado que circunscribe el conjunto T , debe ser parte del predicado S (sobre el mismo dominio) que define S .
• Si S engloba a T y T engloba a S , entonces los dos tipos son iguales (aunque pueden no ser del mismo tipo si el sistema de tipos distingue los tipos por su nombre).

En términos de especificidad informativa, un subtipo se considera más específico que cualquiera de sus supertipos, ya que contiene al menos tanta información como cada uno de ellos. Esto puede aumentar la aplicabilidad o relevancia del subtipo (el número de situaciones en las que puede ser aceptado o introducido), en comparación con sus supertipos "más generales". La desventaja de contar con esta información más detallada es que representa opciones incorporadas que reducen la prevalencia del subtipo (el número de situaciones que pueden generarlo o producirlo).

En el contexto de la subsunción, las definiciones de tipo se pueden expresar mediante la notación de conjuntos , que utiliza un predicado para definir un conjunto. Los predicados se definen sobre un dominio (conjunto de valores posibles) D. Los predicados son funciones parciales que comparan valores con criterios de selección. Por ejemplo: "¿Es un valor entero mayor o igual a 100 y menor que 200?". Si un valor cumple el criterio, la función lo devuelve. Si no, el valor no se selecciona y no se devuelve nada. (Las comprensiones de listas son una forma de este patrón que se utiliza en muchos lenguajes de programación).

Si hay dos predicados,${\displaystyle P_{T}}$que aplica criterios de selección para el tipo T y${\displaystyle P_{s}}$que aplica criterios adicionales para el tipo S , entonces se pueden definir conjuntos para los dos tipos:

${\displaystyle T=\{v\in D\mid \ P_{T}(v)\}}$

${\displaystyle S=\{v\in D\mid \ P_{T}(v){\text{ y }}P_{s}(v)\}}$

El predicado${\displaystyle \mathbf {T} =P_{T}}$se aplica junto con${\displaystyle P_{s}}$como parte del predicado compuesto S que define S. Los dos predicados están unidos , por lo que ambos deben ser verdaderos para que se seleccione un valor. El predicado${\displaystyle \mathbf {S} =\mathbf {T} \land P_{s}=P_{T}\land P_{s}}$subsume el predicado T , por lo que S <: T.

Por ejemplo: existe una subfamilia de especies de gatos llamada Felinae , que forma parte de la familia Felidae . El género Felis , al que pertenece la especie de gato doméstico Felis catus , forma parte de esa subfamilia.

${\displaystyle {\mathit {Felinae=\{cat\in Felidae\mid \ ofSubfamily(cat,felinaeSubfamilyName)\}}}}$

${\displaystyle {\mathit {Felis=\{cat\in Felinae\mid \ ofGenus(cat,felisGenusName)\}}}}$

La conjunción de predicados se ha expresado aquí mediante la aplicación del segundo predicado sobre el dominio de valores que se ajustan al primer predicado. Vistos como tipos, Felis <: Felinae <: Felidae .

Si T engloba a S ( T  :> S ) entonces un procedimiento, función o expresión dado un valor${\displaystyle s\in S}$como operando (valor de parámetro o término) podrá, por lo tanto, operar sobre ese valor como uno de tipo T , porque${\displaystyle s\in T}$. En el ejemplo anterior, podríamos esperar que la función de Subfamilia sea aplicable a valores de los tres tipos Felidae , Felinae y Felis .

Los teóricos de tipos distinguen entre subtipado nominal , en el que solo los tipos declarados de cierta manera pueden ser subtipos entre sí, y subtipado estructural , en el que la estructura de dos tipos determina si uno es o no subtipo del otro. El subtipado orientado a objetos basado en clases descrito anteriormente es nominal; una regla de subtipado estructural para un lenguaje orientado a objetos podría decir que si los objetos de tipo A pueden manejar todos los mensajes que pueden manejar los objetos de tipo B (es decir, si definen todos los mismos métodos ), entonces A es un subtipo de B independientemente de si uno hereda del otro. Este llamado tipado dinámico es común en lenguajes orientados a objetos con tipado dinámico. También se conocen reglas de subtipado estructural sólidas para tipos distintos de los tipos de objetos.

Las implementaciones de lenguajes de programación con subtipado se dividen en dos clases generales: implementaciones inclusivas , en las que la representación de cualquier valor de tipo A también representa el mismo valor de tipo B si A < : B , e implementaciones coercitivas , en las que un valor de tipo A se puede convertir automáticamente en uno de tipo B. El subtipado inducido por la herencia de clases en un lenguaje orientado a objetos suele ser inclusivo; las relaciones de subtipado que relacionan números enteros y de coma flotante, que se representan de forma diferente, suelen ser coercitivas.  

En casi todos los sistemas de tipos que definen una relación de subtipado, esta es reflexiva (lo que significa que A < : A para cualquier tipo A ) y transitiva (lo que significa que si A < : B y B < : C , entonces A < : C ). Esto la convierte en un preorden de tipos.        

Si T ₁ → T ₂ es un tipo de función , entonces un subtipo del mismo es cualquier tipo de función S ₁ → S ₂ con la propiedad de que T ₁ <: S ₁ y S ₂ <: T _2. Esto se puede resumir utilizando la siguiente regla de tipado :

$$${\displaystyle {T_{1}\leq :S_{1}\quad S_{2}\leq :T_{2}} \over {S_{1}\rightarrow S_{2}\leq :T_{1}\rightarrow T_{2}}}$$$

Se dice que el tipo de parámetro de S ₁ → S ₂ es contravariante porque la relación de subtipos se invierte para él, mientras que el tipo de retorno es covariante . Informalmente, esta inversión ocurre porque el tipo refinado es "más liberal" en los tipos que acepta y "más conservador" en el tipo que devuelve. Esto es exactamente lo que funciona en Scala : una función n -aria es internamente una clase que hereda la${\displaystyle {\mathtt {Function_{N}({-A_{1}},{-A_{2}},\dots ,{-A_{n}},{+B})}}}$rasgo (que puede considerarse una interfaz general en lenguajes tipo Java ), donde${\displaystyle {\mathtt {A_{1},A_{2},\dots ,A_{n}}}}$son los tipos de parámetros y${\displaystyle {\mathtt {B}}}$es su tipo de retorno; "−" antes del tipo significa que el tipo es contravariante, mientras que "+" significa covariante.

En lenguajes que permiten efectos secundarios, como la mayoría de los lenguajes orientados a objetos, el subtipado generalmente no es suficiente para garantizar que una función pueda usarse de forma segura en el contexto de otra. El trabajo de Liskov en esta área se centró en el subtipado de comportamiento , que además de la seguridad del sistema de tipos discutida en este artículo también requiere que los subtipos preserven todos los invariantes garantizados por los supertipos en algún contrato . ^{[ 8 ]} Esta definición de subtipado es generalmente indecidible , por lo que no puede ser verificada por un verificador de tipos .

La subtipificación de las referencias mutables es similar al tratamiento de los valores de los parámetros y los valores de retorno. Las referencias de solo escritura (o sumideros ) son contravariantes, al igual que los valores de los parámetros; las referencias de solo lectura (o fuentes ) son covariantes, al igual que los valores de retorno. Las referencias mutables que actúan como fuentes y sumideros son invariantes.

La subtipificación y la herencia son relaciones independientes (ortogonales). Pueden coincidir, pero ninguna es un caso especial de la otra. En otras palabras, entre dos tipos S y T , son posibles todas las combinaciones de subtipificación y herencia:

1. S no es ni un subtipo ni un tipo derivado de T
2. S es un subtipo pero no es un tipo derivado de T.
3. S no es un subtipo, sino un tipo derivado de T.
4. S es tanto un subtipo como un tipo derivado de T.

El primer caso se ilustra con tipos independientes, como Booleany Float.

El segundo caso se puede ilustrar mediante la relación entre Int32y Int64. En la mayoría de los lenguajes de programación orientados a objetos, Int64no están relacionados por herencia con Int32. Sin embargo, Int32puede considerarse un subtipo de Int64ya que cualquier valor entero de 32 bits puede convertirse en un valor entero de 64 bits.

El tercer caso es consecuencia de la contravarianza de entrada del subtipo de función . Supongamos una superclase de tipo T que tiene un método m que devuelve un objeto del mismo tipo ( es decir, el tipo de m es T → T , también observe que el primer parámetro de m es this/self) y un tipo de clase derivada S de T. Por herencia, el tipo de m en S es S → S. Para que S sea un subtipo de T, el tipo de m en S debe ser un subtipo del tipo de m en T , en otras palabras: S → S ≤: T → T. Por aplicación ascendente de la regla de subtipo de función, esto significa: S ≤: T y T ≤: S , lo cual solo es posible si S y T son iguales. Dado que la herencia es una relación irreflexiva, S no puede ser un subtipo de T.

El subtipado y la herencia son compatibles cuando todos los campos y métodos heredados del tipo derivado tienen tipos que son subtipos de los campos y métodos correspondientes del tipo heredado. ^{[ 3 ]}

En los sistemas de subtipado coercitivo, los subtipos se definen mediante funciones de conversión de tipo explícitas de subtipo a supertipo. Para cada relación de subtipado ( S <: T ), se proporciona una función de coerción coerce : S → T , y cualquier objeto s de tipo S se considera como el objeto coerce _{S → T} ( s ) de tipo T . Una función de coerción puede definirse por composición: si S <: T y T <: U entonces s puede considerarse como un objeto de tipo u bajo la coerción compuesta ( coerce _{T → U} ∘ coerce _{S → T} ). La coerción de tipo de un tipo a sí mismo coerce _{T → T} es la función identidad id _T .

Las funciones de coerción para registros y subtipos de unión disjuntos pueden definirse componente por componente; en el caso de registros con ancho extendido, la coerción de tipo simplemente descarta cualquier componente que no esté definido en el supertipo. La coerción de tipo para tipos de función puede darse por f' ( t ) = coerce _{S 2 → T 2} ( f ( coerce _{T 1 → S 1} ( t ))), que refleja la contravarianza de los valores de los parámetros y la covarianza de los valores de retorno.

La función de coerción se determina de forma única dado el subtipo y el supertipo . Por lo tanto, cuando se definen múltiples relaciones de subtipado, se debe tener cuidado de garantizar que todas las coerciones de tipo sean coherentes. Por ejemplo, si un entero como 2  : int se puede convertir a un número de punto flotante (por ejemplo, 2.0  : float ), entonces no es admisible convertir 2.1  : float a 2  : int , porque la coerción compuesta coerce _{float → float} dada por coerce _{int → float} ∘ coerce _{float → int} sería entonces distinta de la coerción identidad id _float .

• Covarianza y contravarianza
• El problema del círculo-elipse (por los peligros de subtipificar los tipos de variables sobre la misma base que los tipos de valor)
• Programación basada en clases
• Tipo superior
• Tipo de refinamiento
• Subtipificación conductual

Libros de texto

Papeles