Subtipificación

En la teoría de los lenguajes de programación , el subtipado (también llamado polimorfismo de subtipos o polimorfismo de inclusión ) es una forma de polimorfismo de tipos . Un subtipo es un tipo de dato relacionado con otro tipo de dato (el supertipo ) mediante algún principio de sustituibilidad , lo que significa que los elementos del programa (normalmente subrutinas o funciones), escritos para operar sobre elementos del supertipo, también pueden operar sobre elementos del subtipo.

Si S es un subtipo de T, la relación de subtipado (escrita como S < : T , S ⊑ T , ^{[ 1 ]} o S ≤: T ) significa que cualquier término de tipo S puede usarse con seguridad en cualquier contexto donde se espere un término de tipo T. La semántica precisa del subtipado aquí depende crucialmente de cómo se definen "usarse con seguridad" y "cualquier contexto" en un formalismo de tipos o lenguaje de programación dado . El sistema de tipos de un lenguaje de programación define esencialmente su propia relación de subtipado, que bien puede ser trivial , si el lenguaje no admite (o admite muy pocos) mecanismos de conversión.   

Debido a la relación de subtipado, un término puede pertenecer a más de un tipo. Por lo tanto, el subtipado es una forma de polimorfismo de tipos. En la programación orientada a objetos, el término "polimorfismo" se usa comúnmente para referirse exclusivamente a este polimorfismo de subtipos , mientras que las técnicas de polimorfismo paramétrico se considerarían programación genérica .

Los lenguajes de programación funcional a menudo permiten el subtipado de registros . En consecuencia, el cálculo lambda de tipado simple extendido con tipos de registro es quizás el entorno teórico más simple en el que se puede definir y estudiar una noción útil de subtipado. ^{[ 2 ]} Debido a que el cálculo resultante permite que los términos tengan más de un tipo, ya no es una teoría de tipos "simple" . Dado que los lenguajes de programación funcional, por definición, admiten literales de función , que también se pueden almacenar en registros, los tipos de registro con subtipado proporcionan algunas de las características de la programación orientada a objetos. Típicamente, los lenguajes de programación funcional también proporcionan alguna forma, generalmente restringida, de polimorfismo paramétrico. En un entorno teórico, es deseable estudiar la interacción de las dos características; un entorno teórico común es el sistema F _{< :} . Varios cálculos que intentan capturar las propiedades teóricas de la programación orientada a objetos se pueden derivar del sistema F _{< :} .

El concepto de subtipado está relacionado con las nociones lingüísticas de hiponimia y holonimia . También está relacionado con el concepto de cuantificación acotada en lógica matemática (véase lógica ordenada ). El subtipado no debe confundirse con la noción de herencia (de clase u objeto) de los lenguajes orientados a objetos; ^{[ 3 ]} el subtipado es una relación entre tipos (interfaces en la terminología orientada a objetos) mientras que la herencia es una relación entre implementaciones que surge de una característica del lenguaje que permite crear nuevos objetos a partir de los existentes. En varios lenguajes orientados a objetos, el subtipado se denomina herencia de interfaz , mientras que la herencia se denomina herencia de implementación .

La noción de subtipado en lenguajes de programación se remonta a la década de 1960; se introdujo en derivados de Simula . Los primeros tratamientos formales del subtipado fueron dados por John C. Reynolds en 1980, quien utilizó la teoría de categorías para formalizar las conversiones implícitas , y por 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 { public : void methodOfA () 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{ and }}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