En la teoría de tipos , un tipo de intersección se puede asignar a valores que se pueden asignar tanto al tipo y el tipo . A este valor se le puede dar el tipo de intersecciónen un sistema de tipo intersección . [1] Generalmente, si los rangos de valores de dos tipos se superponen, a un valor que pertenezca a la intersección de los dos rangos se le puede asignar el tipo de intersección de estos dos tipos. Dicho valor se puede pasar de forma segura como argumento a funciones que esperan cualquiera de los dos tipos. Por ejemplo, en Java, la clase Boolean
implementa Serializable
las Comparable
interfaces y. Por lo tanto, un objeto de tipo Boolean
se puede pasar de forma segura a funciones que esperan un argumento de tipo Serializable
y a funciones que esperan un argumento de tipo Comparable
.
Los tipos de intersección son tipos de datos compuestos . Al igual que los tipos de productos , se utilizan para asignar varios tipos a un objeto. Sin embargo, los tipos de producto se asignan a tuplas , de modo que a cada elemento de tupla se le asigna un componente de tipo de producto en particular. En comparación, los objetos subyacentes de los tipos de intersección no son necesariamente compuestos. Una forma restringida de tipos de intersección son los tipos de refinamiento .
Los tipos de intersección son útiles para describir funciones sobrecargadas . [2] Por ejemplo, si es el tipo de función que toma un número como argumento y devuelve un número, y es el tipo de función que toma una cadena como argumento y devuelve una cadena, entonces se puede utilizar la intersección de estos dos tipos. para describir funciones (sobrecargadas) que hacen una u otra, según el tipo de entrada que reciben.number => number
string => string
Los lenguajes de programación contemporáneos, incluidos Ceylon , Flow, Java , Scala , TypeScript y Whiley (consulte la comparación de lenguajes con tipos de intersección ), utilizan tipos de intersección para combinar especificaciones de interfaz y expresar polimorfismo ad hoc . Como complemento del polimorfismo paramétrico , los tipos de intersección se pueden usar para evitar la contaminación de la jerarquía de clases por preocupaciones transversales y reducir el código estándar , como se muestra en el ejemplo de TypeScript a continuación.
El estudio de la teoría de tipos de los tipos de intersección se denomina disciplina de tipo de intersección . [3] Sorprendentemente, la terminación del programa se puede caracterizar con precisión utilizando tipos de intersección. [4]
Ejemplo de TypeScript
TypeScript admite tipos de intersección, [5] mejorando la expresividad del sistema de tipos y reduciendo el tamaño potencial de la jerarquía de clases, como se demuestra a continuación.
El siguiente código de programa define las clases Chicken
, Cow
y RandomNumberGenerator
que tienen cada uno un método produce
de devolver un objeto de cualquier tipo Egg
, Milk
o number
. Además, las funciones eatEgg
y drinkMilk
requieren argumentos de tipo Egg
y Milk
, respectivamente.
clase Huevo { clase privada : "Huevo" } clase Leche { clase privada : "Leche" } // produce huevos class Chicken { produce () { return new Egg (); } }// produce la clase de leche Vaca { produce () { return new Milk (); } }// produce una clase de número aleatorio RandomNumberGenerator { produce () { return Math . aleatorio (); } }// requiere una función de huevo eatEgg ( egg : Egg ) { return "Me comí un huevo". ; }// Requiere la función de leche drinkMilk ( leche : Leche ) { return "Bebí un poco de leche". ; }
El siguiente código de programa define la función polimórfica ad hocanimalToFood
que invoca la función miembro produce
del objeto dado animal
. La función animalToFood
tiene dos anotaciones de tipo, a saber , y , conectadas a través del constructor de tipo de intersección . Específicamente, cuando se aplica a un argumento de tipo, devuelve un objeto de tipo , y cuando se aplica a un argumento de tipo, devuelve un objeto de tipo . Idealmente, no debería ser aplicable a ningún objeto que tenga (posiblemente por casualidad) un método.((_: Chicken) => Egg)
((_: Cow) => Milk)
&
animalToFood
Chicken
Egg
Cow
Milk
animalToFood
produce
// dado un pollo, produce un huevo; dada una vaca, produce leche let animalToFood : (( _ : Chicken ) => Egg ) & (( _ : Cow ) => Milk ) = function ( animal : any ) { return animal . producir (); };
Finalmente, el siguiente código de programa demuestra el uso seguro de tipos de las definiciones anteriores.
var pollo = nueva pollo ();var vaca = nueva vaca ();var randomNumberGenerator = new RandomNumberGenerator ();consola . log ( pollo . producir ()); //Huevo { }consola . log ( vaca . producir ()); //Leche { }consola . log ( randomNumberGenerator . produce ()); //0.2626353555444987consola . log ( animalToFood ( pollo )); //Huevo { }consola . log ( animalToFood ( vaca )); //Leche { }//console.log(animalToFood(randomNumberGenerator)); // ERROR: El argumento de tipo 'RandomNumberGenerator' no se puede asignar al parámetro de tipo 'Vaca'consola . log ( eatEgg ( animalToFood ( pollo ))); // Me comí un huevo.//console.log(eatEgg(animalToFood(cow))); // ERROR: El argumento de tipo 'Leche' no se puede asignar al parámetro de tipo 'Huevo'consola . log ( drinkMilk ( animalToFood ( vaca ))); // Bebí un poco de leche.//console.log(drinkMilk(animalToFood(chicken))); // ERROR: El argumento de tipo 'Huevo' no se puede asignar al parámetro de tipo 'Leche'
El código de programa anterior tiene las siguientes propiedades:
- Las líneas 1 a 3 crean objetos
chicken
,cow
yrandomNumberGenerator
de su tipo respectivo. - Las líneas 5-7 imprimen para los objetos creados previamente los resultados respectivos (proporcionados como comentarios) al invocar
produce
. - La línea 9 (resp. 10) demuestra el tipo de uso seguro del método
animalToFood
aplicado achicken
(resp.cow
). - La línea 11, si no se confirma, daría como resultado un error de tipo en el momento de la compilación. Aunque la implementación de
animalToFood
podría invocar elproduce
método derandomNumberGenerator
, la anotación de tipo deanimalToFood
no lo permite. Esto está de acuerdo con el significado pretendido deanimalToFood
. - La línea 13 (resp. 15) demuestra que aplicar
animalToFood
achicken
(resp.cow
) Da como resultado un objeto de tipoEgg
(resp.Milk
). - La línea 14 (resp. 16) demuestra que aplicar
animalToFood
acow
(resp.chicken
) No da como resultado un objeto de tipoEgg
(resp.Milk
). Por lo tanto, si no se comenta, la línea 14 (resp. 16) daría como resultado un error de tipo en tiempo de compilación.
Comparación con la herencia
El ejemplo minimalista anterior se puede realizar usando herencia , por ejemplo, derivando las clases Chicken
y Cow
de una clase base Animal
. Sin embargo, en un entorno más grande, esto podría ser una desventaja. La introducción de nuevas clases en una jerarquía de clases no está necesariamente justificada por cuestiones transversales , o tal vez sea completamente imposible, por ejemplo, cuando se utiliza una biblioteca externa. Imagínense, el ejemplo anterior podría extenderse con las siguientes clases:
- una clase
Horse
que no tieneproduce
método; - una clase
Sheep
que tiene unproduce
método que regresaWool
; - una clase
Pig
que tiene unproduce
método, que se puede usar solo una vez, regresandoMeat
.
Esto puede requerir clases (o interfaces) adicionales que especifiquen si un método de producción está disponible, si el método de producción devuelve alimentos y si el método de producción se puede utilizar repetidamente. En general, esto puede contaminar la jerarquía de clases.
Comparación con el tipeo de pato
El ejemplo minimalista anterior ya muestra que la escritura de pato es menos adecuada para realizar el escenario dado. Si bien la clase RandomNumberGenerator
contiene un produce
método, el objeto randomNumberGenerator
no debe ser un argumento válido para animalToFood
. El ejemplo anterior se puede realizar utilizando el tipo de pato, por ejemplo, introduciendo un nuevo campo argumentForAnimalToFood
en las clases Chicken
y Cow
significando que los objetos del tipo correspondiente son argumentos válidos para animalToFood
. Sin embargo, esto no solo aumentaría el tamaño de las clases respectivas (especialmente con la introducción de más métodos similares a animalToFood
), sino que también es un enfoque no local con respecto a animalToFood
.
Comparación con la sobrecarga de funciones
El ejemplo anterior se puede realizar mediante la sobrecarga de funciones , por ejemplo, implementando dos métodos y . En TypeScript, esta solución es casi idéntica al ejemplo proporcionado. Otros lenguajes de programación, como Java , requieren distintas implementaciones del método sobrecargado. Esto puede llevar a la duplicación del código o al código repetitivo .animalToFood(animal: Chicken): Egg
animalToFood(animal: Cow): Milk
Comparación con el patrón de visitantes
El ejemplo anterior se puede realizar utilizando el patrón de visitantes . Requeriría que cada clase de animal implemente un accept
método que acepte un objeto que implemente la interfaz AnimalVisitor
(agregando código repetitivo no local ). La función animalToFood
se realizaría como el visit
método de implementación de AnimalVisitor
. Desafortunadamente, la conexión entre el tipo de entrada ( Chicken
o Cow
) y el tipo de resultado ( Egg
o Milk
) sería difícil de representar.
Limitaciones
Por un lado, los tipos de intersección se pueden usar para anotar localmente diferentes tipos en una función sin introducir nuevas clases (o interfaces) en la jerarquía de clases. Por otro lado, este enfoque requiere que todos los tipos de argumentos y tipos de resultados posibles se especifiquen explícitamente. Si el comportamiento de una función se puede especificar con precisión mediante una interfaz unificada, polimorfismo paramétrico o tipificación de pato , entonces la naturaleza detallada de los tipos de intersección es desfavorable. Por lo tanto, los tipos de intersección deben considerarse complementarios a los métodos de especificación existentes.
Tipo de intersección dependiente
Un tipo de intersección dependiente , denotado, es un tipo dependiente en el que el tipo puede depender del término variable . [6] En particular, si un término tiene el tipo de intersección dependiente , luego el término tiene tanto el tipo y el tipo , dónde es el tipo que resulta de reemplazar todas las apariciones del término variable en por el término .
Ejemplo de Scala
Scala admite declaraciones de tipo [7] como miembros de objeto. Esto permite que un tipo de miembro de un objeto dependa del valor de otro miembro, lo que se denomina tipo dependiente de la ruta . [8] Por ejemplo, el siguiente texto del programa define un rasgo de Scala Witness
, que puede usarse para implementar el patrón singleton . [9]
rasgo Testigo { tipo T val valor : T {} }
El rasgo anterior Witness
declara el miembro T
, al que se le puede asignar un tipo como su valor, y el miembro value
, al que se le puede asignar un valor de tipo T
. El siguiente texto del programa define un objeto booleanWitness
como instancia del rasgo anterior Witness
. El objeto booleanWitness
define el tipo T
como Boolean
y el valor value
como true
. Por ejemplo, ejecutar impresiones en la consola.System.out.println(booleanWitness.value)
true
object booleanWitness extiende Witness { tipo T = Boolean val value = true }
Dejar ser el tipo (específicamente, un tipo de registro ) de objetos que tienen el miembro de tipo . En el ejemplo anterior, al objeto booleanWitness
se le puede asignar el tipo de intersección dependiente. El razonamiento es como sigue. El objeto booleanWitness
tiene el miembro al T
que se le asigna el tipo Boolean
como su valor. Dado que Boolean
es un tipo, el objeto booleanWitness
tiene el tipo. Además, el objeto booleanWitness
tiene el miembro al value
que se le asigna el valor true
de tipo Boolean
. Dado que el valor de es , el objeto tiene el tipobooleanWitness.T
Boolean
booleanWitness
. En general, el objeto booleanWitness
tiene el tipo de intersección. Por lo tanto, al presentar la autorreferencia como dependencia, el objeto booleanWitness
tiene el tipo de intersección dependiente.
Alternativamente, el ejemplo minimalista anterior se puede describir utilizando tipos de registro dependientes . [10] En comparación con los tipos de intersección dependientes, los tipos de registros dependientes constituyen un concepto teórico de tipos estrictamente más especializado. [6]
Intersección de una familia tipográfica
Una intersección de una familia tipográfica, denotada, es un tipo dependiente en el que el tipo puede depender del término variable . [6] En particular, si un término tiene el tipo , luego para cada término de tipo , el termino tiene el tipo . Esta noción también se llama tipo Pi implícito , [11] observando que el argumento no se mantiene a nivel de término.
Comparación de idiomas con tipos de intersección
Idioma | Desarrollado activamente | Paradigma (s) | Estado | Características |
---|---|---|---|---|
C# | Sí [12] |
| En discusión [13] | ? |
Ceilán | Sí [14] |
| Compatible [15] |
|
F# | Sí [16] |
| En discusión [17] | ? |
Flujo | Sí [18] |
| Compatible [19] |
|
Forsythe | No |
| Compatible [20] |
|
Java | Sí [21] |
| Compatible [22] |
|
PHP | Sí [23] |
| Compatible [24] |
|
Scala | Sí [25] |
| Compatible [26] [27] |
|
Mecanografiado | Sí [28] |
| Compatible [5] |
|
Mientras | Sí [29] |
| Compatible [30] | ? |
Referencias
- ^ Barendregt, Henk; Coppo, Mario; Dezani-Ciancaglini, Mariangiola (1983). "Un modelo de filtro lambda y la integridad de la asignación de tipos". Revista de lógica simbólica . 48 (4): 931–940. doi : 10.2307 / 2273659 . JSTOR 2273659 .
- ^ Palsberg, Jens (2012). "La sobrecarga es NP-Complete". Semántica de programa y lógica . Apuntes de conferencias en informática. 7230 . págs. 204–218. doi : 10.1007 / 978-3-642-29485-3_13 . ISBN 978-3-642-29484-6.
- ^ Henk Barendregt; Wil Dekkers; Richard Statman (20 de junio de 2013). Cálculo lambda con tipos . Prensa de la Universidad de Cambridge. págs. 1–. ISBN 978-0-521-76614-2.
- ^ Ghilezan, Silvia (1996). "Fuerte normalización y tipificación con tipos de intersección" . Diario de Notre Dame de lógica formal . 37 (1): 44–52. doi : 10.1305 / ndjfl / 1040067315 .
- ^ a b "Tipos de intersección en TypeScript" . Consultado el 1 de agosto de 2019 .
- ^ a b c Kopylov, Alexei (2003). "Intersección dependiente: una nueva forma de definir registros en la teoría de tipos". 18º Simposio IEEE sobre Lógica en Ciencias de la Computación . LICS 2003. IEEE Computer Society. págs. 86–95. CiteSeerX 10.1.1.89.4223 . doi : 10.1109 / LICS.2003.1210048 .
- ^ "Declaraciones de tipo en Scala" . Consultado el 15 de agosto de 2019 .
- ^ Amin, Nada; Grütter, Samuel; Odersky, Martin; Rompf, Tiark; Stucki, Sandro (2016). "La esencia de los tipos de objetos dependientes". Una lista de éxitos que pueden cambiar el mundo: ensayos dedicados a Philip Wadler con motivo de su 60 cumpleaños . Apuntes de conferencias en Ciencias de la Computación . 9600 . Saltador. págs. 249-272. doi : 10.1007 / 978-3-319-30936-1_14 .
- ^ "Singletons en la biblioteca informe de Scala" . Consultado el 15 de agosto de 2019 .
- ^ Pollack, Robert (2000). "Registros de tipo dependiente para representar la estructura matemática". Demostración de teoremas en lógicas de orden superior, 13ª Conferencia Internacional . TPHOLs 2000. Springer. págs. 462–479. doi : 10.1007 / 3-540-44659-1_29 .
- ^ Stump, Aaron (2018). "De la realizabilidad a la inducción vía intersección dependiente" . Anales de lógica pura y aplicada . 169 (7): 637–655. doi : 10.1016 / j.apal.2018.03.002 .
- ^ "Guía de C #" . Consultado el 8 de agosto de 2019 .
- ^ "Discusión: tipos de unión e intersección en C Sharp" . Consultado el 8 de agosto de 2019 .
- ^ "Eclipse Ceilán: Bienvenidos a Ceilán" . Consultado el 8 de agosto de 2019 .
- ^ "Tipos de intersección en Ceilán" . Consultado el 8 de agosto de 2019 .
- ^ "F # Software Foundation" . Consultado el 8 de agosto de 2019 .
- ^ "Agregar tipos de intersección a F Sharp" . Consultado el 8 de agosto de 2019 .
- ^ "Flujo: un verificador de tipo estático para JavaScript" . Consultado el 8 de agosto de 2019 .
- ^ "Sintaxis del tipo de intersección en el flujo" . Consultado el 8 de agosto de 2019 .
- ^ Reynolds, JC (1988). Diseño preliminar del lenguaje de programación Forsythe.
- ^ "Software Java" . Consultado el 8 de agosto de 2019 .
- ^ "IntersectionType (Java SE 12 y JDK 12)" . Consultado el 1 de agosto de 2019 .
- ^ "php.net" .
- ^ "PHP.Watch - PHP 8.1: Tipos de intersección" .
- ^ "El lenguaje de programación Scala" . Consultado el 8 de agosto de 2019 .
- ^ "Tipos de compuestos en Scala" . Consultado el 1 de agosto de 2019 .
- ^ "Tipos de intersección en Dotty" . Consultado el 1 de agosto de 2019 .
- ^ "TypeScript - JavaScript que escala" . Consultado el 1 de agosto de 2019 .
- ^ "Whiley: un lenguaje de programación de código abierto con comprobación estática extendida" . Consultado el 1 de agosto de 2019 .
- ^ "Especificación del idioma whiley" (PDF) . Consultado el 1 de agosto de 2019 .