Subtipado - Subtyping

En la teoría del lenguaje de programación , el subtipo (también polimorfismo de subtipo o polimorfismo de inclusión ) es una forma de polimorfismo de tipo en el que un subtipo es un tipo de datos que está relacionado con otro tipo de datos (el supertipo ) por alguna noción de sustituibilidad , lo que significa que los elementos del programa, típicamente subrutinas o funciones, escritas 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 subtipo a menudo se escribe S <: T, para significar que cualquier término de tipo S puede usarse con seguridad en un contexto donde se espera un término de tipo T. La semántica precisa de la subtipificación depende fundamentalmente de los detalles de lo que significa "utilizado con seguridad en un contexto donde" en un lenguaje de programación dado . El sistema de tipos de un lenguaje de programación esencialmente define su propia relación de subtipificación, que bien puede ser trivial , si el lenguaje no soporta (o muy pocos) mecanismos de conversión.

Debido a la relación de subtipificación, un término puede pertenecer a más de un tipo. La subtipificación es, por tanto, una forma de polimorfismo de tipos. En la programación orientada a objetos, el término 'polimorfismo' se usa comúnmente para referirse únicamente a este subtipo de polimorfismo , 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 la subtipificación de registros . En consecuencia, el cálculo lambda simplemente tipado extendido con tipos de registro es quizás el escenario teórico más simple en el que se puede definir y estudiar una noción útil de subtipificación. 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 registros con subtipos proporcionan algunas de las características de la programación orientada a objetos. Por lo general, los lenguajes de programación funcionales también proporcionan alguna forma, generalmente restringida, de polimorfismo paramétrico. En un escenario teórico, es deseable estudiar la interacción de las dos características; un entorno teórico común es sistema de F _<: . Varios cálculos que intentan capturar las propiedades teóricas de programación orientada a objetos pueden ser derivados de sistema de F _<: .

El concepto de subtipificación 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 (ver Lógica ordenada por orden ). La subtipificación no debe confundirse con la noción de herencia (de clase u objeto) de los lenguajes orientados a objetos; la subtipificación es una relación entre tipos (interfaces en el lenguaje orientado a objetos) mientras que la herencia es una relación entre implementaciones derivadas de una característica del lenguaje que permite crear nuevos objetos a partir de los existentes. En varios lenguajes orientados a objetos, la subtipificación se denomina herencia de interfaz , y la herencia se denomina herencia de implementación .

Orígenes

La noción de subtipificación en lenguajes de programación se remonta a la década de 1960; se introdujo en derivados de Simula . Los primeros tratamientos formales de la subtipificación fueron dados por John C. Reynolds en 1980, quien utilizó la teoría de categorías para formalizar conversiones implícitas , y Luca Cardelli (1985).

El concepto de subtipificación ha ganado visibilidad (y sinonimia con 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 a menudo se denomina principio de sustitución de Liskov , en honor a Barbara Liskov, quien lo popularizó en un discurso de apertura en una conferencia sobre programación orientada a objetos en 1987. Debido a que debe considerar objetos mutables, la noción ideal de subtipificación definido por Liskov y Jeannette Wing , llamado subtipo de comportamiento es considerablemente más fuerte que lo que se puede implementar en un verificador de tipos . (Consulte § Tipos de funciones a continuación para obtener más detalles).

Ejemplos de

Ejemplo de subtipos: donde pájaro es el supertipo y todos los demás son subtipos como lo indica la flecha en notación UML

En el diagrama de la derecha se muestra un ejemplo práctico simple de subtipos. El tipo "pájaro" tiene tres subtipos "pato", "cuco" y "avestruz". Conceptualmente, cada uno de estos es una variedad del tipo básico "pájaro" que hereda muchas características de "pájaro" pero tiene algunas diferencias específicas. En este diagrama se utiliza la notación UML , con flechas de cabeza abierta que muestran 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 que se usen valores enteros siempre que se esperen valores de punto flotante ( Integer<:) Float, o podría definir un tipo genéricoNúmerocomo un supertipo común de enteros y reales. En este segundo caso, solo tenemos Integer<: Numbery Float<:, Numberpero Integery Floatno son subtipos entre sí.

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

function max (x as Number, y as Number) is
    if x < y then
        return y
    else
        return x
end

Si integer y real son ambos subtipos de Number, y se define un operador de comparación con un número arbitrario para ambos tipos, entonces se pueden pasar valores de cualquier tipo a esta función. Sin embargo, la posibilidad misma de implementar un operador de este tipo restringe en gran medida el tipo de Número (por ejemplo, no se puede comparar un número 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 .

Subsunción

En teoría el concepto de tipo subsunción se utiliza para definir o evaluar si un tipo S es un subtipo del tipo T .

Un tipo es un conjunto de valores. El conjunto se puede describir extensivamente enumerando todos los valores, o puede describirse 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 de forma extensiva enumerando valores. Los tipos definidos por el usuario, como registros (estructuras, interfaces) o clases, se definen intencionalmente mediante una declaración de tipo explícita o mediante el uso de un valor existente, que codifica la información del tipo, como un prototipo que se copiará o ampliará.

Al discutir el concepto de subsunción, el conjunto de valores de un tipo se indica escribiendo su nombre en cursiva matemáticos: 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".

• Tipo A T subsume 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 ser subsumido por más de un tipo: los supertipos de S se cortan en S .
• Si S <: T (y por lo tanto S ⊆ T ), entonces T , el predicado que circunscribe el conjunto T , deben ser parte del predicado S (en el mismo dominio) que define S .
• Si S subsume a T y T subsume 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).

Sigue una regla general: es probable que un subtipo sea "más grande / más ancho / más profundo" (sus valores contienen más información) y "menos / más pequeño" (el conjunto de valores es más pequeño) que uno de sus supertipos (que tiene más información, y cuyo conjunto de valores es un superconjunto de los del subtipo).

En el contexto de la subsunción, las definiciones de tipo se pueden expresar utilizando la notación del constructor de conjuntos , que utiliza un predicado para definir un conjunto. Los predicados se pueden definir más de 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 que 100 y menor que 200?". Si un valor coincide con los criterios, la función devuelve el valor. De lo contrario, el valor no se selecciona y no se devuelve nada. (Las listas por comprensión son una forma de este patrón que se utiliza en muchos lenguajes de programación).

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

${\ Displaystyle T = \ {v \ en D \ mid \ P_ {T} (v) \}}$

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

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

Por ejemplo: existe una subfamilia de especies de gatos llamada Felinae , que es 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 = \ {gato \ en Felidae \ mid \ ofSubfamily (gato, felinaeSubfamilyName) \}}}}$

${\ displaystyle {\ mathit {Felis = \ {gato \ en Felinae \ mid \ ofGenus (gato, felisGenusName) \}}}}$

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

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

Esquemas de subtipificación

Los teóricos de tipos hacen una distinción entre subtipos nominales , en los que solo los tipos declarados de cierta manera pueden ser subtipos entre sí, y subtipos estructurales , en los que la estructura de dos tipos determina si uno es un subtipo del otro. El subtipo orientado a objetos basado en clases descrito anteriormente es nominal; una regla de subtipo estructural para un lenguaje orientado a objetos podría decir que si los objetos de tipo A pueden manejar todos los mensajes que los objetos de tipo B pueden manejar (es decir, si definen los mismos métodos ), entonces A es un subtipo de B independientemente de si alguno hereda del otro. Esta denominada escritura pato es común en los lenguajes orientados a objetos de escritura dinámica. También son bien conocidas reglas sólidas de subtipificación estructural para tipos distintos de los tipos de objeto.

Las implementaciones de lenguajes de programación con subtipos 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 en el tipo B si A  <:  B , e implementaciones coercitivas , en las que un valor de tipo A puede ser convertido automáticamente en una de tipo B . La subtipificación inducida por la subclasificación en un lenguaje orientado a objetos suele ser inclusiva; las relaciones de subtipificación que relacionan números enteros y de coma flotante, que se representan de manera diferente, suelen ser coercitivas.

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

Tipos de registro

Subtipado de ancho y profundidad

Los tipos de registros dan lugar a los conceptos de subtipificación de ancho y profundidad . Estos expresan dos formas diferentes de obtener un nuevo tipo de registro que permite las mismas operaciones que el tipo de registro original.

Recuerde que un registro es una colección de campos (con nombre). Dado que un subtipo es un tipo que permite todas las operaciones permitidas en el tipo original, un subtipo de registro debe admitir las mismas operaciones en los campos que el tipo original admitido.

Un tipo de forma de lograr dicho soporte, llamado subtipo de ancho , agrega más campos al registro. Más formalmente, cada campo (con nombre) que aparece en el supertipo de ancho aparecerá en el subtipo de ancho. Por lo tanto, cualquier operación factible en el supertipo será compatible con el subtipo.

El segundo método, llamado subtipo de profundidad , reemplaza los distintos campos con sus subtipos. Es decir, los campos del subtipo son subtipos de los campos del supertipo. Dado que cualquier operación admitida para un campo en el supertipo es compatible con su subtipo, cualquier operación factible en el supertipo de registro es compatible con el subtipo de registro. El subtipo de profundidad solo tiene sentido para registros inmutables: por ejemplo, puede asignar 1.5 al campo 'x' de un punto real (un registro con dos campos reales), pero no puede hacer lo mismo con el campo 'x' de un punto entero (que, sin embargo, es un subtipo profundo del tipo de punto real) porque 1.5 no es un número entero (ver Varianza ).

El subtipo de registros se puede definir en System F _<:, que combina el polimorfismo paramétrico con el subtipo de tipos de registro y es una base teórica para muchos lenguajes de programación funcionales que admiten ambas características.

Algunos sistemas también admiten el subtipo de tipos de unión disjuntos etiquetados (como los tipos de datos algebraicos ). La regla para el subtipo de ancho se invierte: todas las etiquetas que aparecen en el subtipo de ancho deben aparecer en el supertipo de ancho.

Tipos de funciones

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 ₂ . Esto se puede resumir usando la siguiente regla de escritura :

${\ 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 argumento de S ₁ → S ₂ es contravariante porque la relación de subtipo se invierte para él, mientras que el tipo de retorno es covariante . De manera informal, esta inversión se produce 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 -ary es internamente una clase que hereda el rasgo (que puede verse como una interfaz general en lenguajes similares a Java ), donde están los tipos de parámetros, y B es su tipo de retorno; " - " antes del tipo significa que el tipo es contravariante mientras que " + " significa covariante. ${\ displaystyle {\ mathtt {Función_ {N} (- A_ {1}, - A_ {2}, \ puntos, -A_ {n}, + B)}}}$ ${\ Displaystyle {\ mathtt {A_ {1}, A_ {2}, \ dots A_ {n}}}}$

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

El subtipo de referencias mutables es similar al tratamiento de argumentos de función y valores de retorno. Las referencias (o sumideros ) de solo escritura son contravariantes, como los argumentos de función; Las referencias (o fuentes ) de solo lectura son covariantes, como los valores de retorno. Las referencias mutables que actúan como fuentes y sumideros son invariables.

Relación con la herencia

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

1. S no es 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 pero es 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 puede ilustrarse 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, Int32se puede considerar un subtipo de, Int64ya que cualquier valor entero de 32 bits se puede promover a un valor entero de 64 bits.

El tercer caso es una consecuencia de la función de subtipificación de la contravarianza de entrada . Suponga 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 tenga en cuenta que el primer argumento de m es this / self) y una clase derivada tipo S de T . Por herencia, el tipo de m en S es S → S . A fin de que S sea un subtipo de T del 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 , que solo es posible si S y T son lo mismo. Desde herencia es una relación de irreflexive, S no puede ser un subtipo de T .

El subtipo 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.

Coacciones

En los sistemas de subtipificación coercitiva, los subtipos se definen mediante funciones de conversión de tipos implícitas de subtipo a supertipo. Para cada relación de subtipos ( S <: T ), una función coacción coerce : S → T se proporciona, y cualquier objeto s de tipo S es considerado 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 ( coerción _{T → U} ∘ coerción _{S → T} ). La coerción de tipo de un tipo a sí mismo coacciona _{T → T} es la función de identidad id _T

Las funciones de coerción para registros y subtipos de unión disjuntos pueden definirse por componentes; en el caso de registros de ancho extendido, la coerción de tipo simplemente descarta cualquier componente que no esté definido en el supertipo. La coerción de tipos para los tipos de función puede estar dada por f ' ( s ) = coaccionar _{S 2 → T 2} ( f ( coaccionar _{T 1 → S 1} ( t ))), lo que refleja la contravarianza de los argumentos de la función 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 subtipificación, se debe tener cuidado de garantizar que todas las coacciones de tipo sean coherentes. Por ejemplo, si un entero como 2: int puede ser coaccionado a un número de coma flotante (digamos, 2.0: float ), entonces no es admisible coaccionar 2.1: float a 2: int , porque la coerción compuesta coerce _{float → float} dado por coerce _{int → float} ∘ coerce _{float → int} entonces sería distinto de la coerción de identidad id _float .

Ver también

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

Notas

Referencias

Libros de texto

Documentos

Otras lecturas