Type d'intersection

En théorie des types , un type d'intersection peut être attribué à des valeurs auxquelles peuvent être assignées à la fois le type et le type . Cette valeur peut être affectée du type d'intersection dans un système de types d'intersection . Généralement, si les plages de valeurs de deux types se chevauchent, une valeur appartenant à l' intersection des deux plages peut être affectée du type d'intersection de ces deux types. Une telle valeur peut être transmise en toute sécurité comme argument à des fonctions qui attendent l'un des deux types. Par exemple, en Java, la classe implémente à la fois les interfaces et . Par conséquent, un objet de type peut être transmis en toute sécurité à des fonctions qui attendent un argument de type et à des fonctions qui attendent un argument de type . BooleanSerializableComparableBooleanSerializableComparable

Les types d'intersection sont des types de données composites . Similaires aux types de produits , ils sont utilisés pour attribuer plusieurs types à un objet. Cependant, les types de produits sont attribués à des tuples , de sorte que chaque élément de tuple se voit attribuer un composant de type de produit particulier. En comparaison, les objets sous-jacents des types d'intersection ne sont pas nécessairement composites. Une forme restreinte de types d'intersection sont les types de raffinement .

Les types d'intersection sont utiles pour décrire des fonctions surchargées . Par exemple, si est le type de fonction prenant un nombre comme argument et renvoyant un nombre, et est le type de fonction prenant une chaîne comme argument et renvoyant une chaîne, alors l'intersection de ces deux types peut être utilisée pour décrire des fonctions (surchargées) qui font l'une ou l'autre, en fonction du type d'entrée qui leur est donnée. number=>numberstring=>string

Les langages de programmation contemporains, dont Ceylon , Flow, Java , Scala , TypeScript et Whiley (voir la comparaison des langages avec les types d'intersection), utilisent des types d'intersection pour combiner des spécifications d'interface et pour exprimer un polymorphisme ad hoc . En complément du polymorphisme paramétrique , les types d'intersection peuvent être utilisés pour éviter la pollution de la hiérarchie des classes par des problèmes transversaux et réduire le code standard , comme illustré dans l'exemple TypeScript ci-dessous.

L' étude théorique des types d'intersection est appelée discipline des types d'intersection . Il est remarquable que la terminaison d'un programme puisse être caractérisée avec précision à l'aide de types d'intersection.

TypeScript prend en charge les types d'intersection, améliorant l'expressivité du système de types et réduisant la taille potentielle de la hiérarchie des classes, comme illustré ci-dessous.

Le code de programme suivant définit les classes Chicken, Cow, et RandomNumberGeneratorqui ont chacune une méthode producerenvoyant un objet de type Egg, Milk, ou number. De plus, les fonctions eatEgget drinkMilknécessitent des arguments de type Egget Milk, respectivement.

classe Egg { type privé : "Egg" } classe Milk { type privé : "Milk" }
// produit des œufs 
classe Chicken { produce () { return new Egg (); } }
// produit du lait 
classe Cow { produce () { return new Milk (); } }
// produit un nombre aléatoire 
class RandomNumberGenerator { produce () { return Math . random (); } }
// nécessite une 
fonction d'oeuf eatEgg ( egg : Egg ) { return "J'ai mangé un oeuf." ; }
// nécessite 
la fonction milk drinkMilk ( milk : Milk ) { return "J'ai bu du lait." ; }

Le code de programme suivant définit la fonction polymorphe ad hocanimalToFood qui invoque la fonction membre producede l'objet donné animal. La fonction animalToFoodpossède deux annotations de type, à savoir et , connectées via le constructeur de type d'intersection . Plus précisément, lorsqu'elle est appliquée à un argument de type , elle renvoie un objet de type , et lorsqu'elle est appliquée à un argument de type , elle renvoie un objet de type . Idéalement, elle ne devrait pas être applicable à un objet ayant (éventuellement par hasard) une méthode. ((_:Chicken)=>Egg)((_:Cow)=>Milk)&animalToFoodChickenEggCowMilkanimalToFoodproduce

// étant donné un poulet, produit un œuf ; étant donné une vache, produit du lait 
let animalToFood : (( _ : Chicken ) => Egg ) & (( _ : Cow ) => Milk ) = function ( animal : any ) { return animal . produce (); };

Enfin, le code de programme suivant démontre une utilisation sûre des définitions ci-dessus.

var poulet = nouveau poulet ();
var vache = nouvelle vache ();
var randomNumberGenerator = nouveau RandomNumberGenerator ();
console . log ( chicken . produce ()); // Oeuf { }
console . log ( cow . produce ()); // Lait { }
console . log ( randomNumberGenerator . produce ()); //0,2626353555444987
console . log ( animalToFood ( poulet )); // Œuf { }
console . log ( animalToFood ( vache )); // Lait { }
//console.log(animalToFood(randomNumberGenerator)); // ERREUR : l'argument de type « RandomNumberGenerator » n'est pas attribuable au paramètre de type « Vache »
console . log ( eatEgg ( animalToFood ( chicken ))); // J'ai mangé un œuf.
//console.log(eatEgg(animalToFood(cow))); // ERREUR : l'argument de type « Milk » n'est pas assignable au paramètre de type « Egg »
console . log ( drinkMilk ( animalToFood ( cow ))); // J'ai bu du lait.
//console.log(drinkMilk(animalToFood(chicken))); // ERREUR : l'argument de type « Œuf » n'est pas attribuable au paramètre de type « Lait »

Le code du programme ci-dessus possède les propriétés suivantes :

• Les lignes 1 à 3 créent des objets chicken, cowet randomNumberGeneratorde leur type respectif.
• Les lignes 5 à 7 impriment pour les objets créés précédemment les résultats respectifs (fournis sous forme de commentaires) lors de l'appel de produce.
• La ligne 9 (resp. 10) démontre l'utilisation sûre du type de méthode animalToFoodappliquée à chicken(resp. cow).
• La ligne 11, si elle n'est pas commentée, entraînerait une erreur de type au moment de la compilation. Bien que l' implémentation de animalToFoodpuisse invoquer la produceméthode de randomNumberGenerator, l' annotation de type de animalToFoodl'interdit. Ceci est conforme à la signification voulue de animalToFood.
• La ligne 13 (resp. 15) démontre que l'application animalToFoodà chicken(resp. cow) donne un objet de type Egg(resp. Milk).
• La ligne 14 (resp. 16) démontre que l'application animalToFoodà cow(resp. chicken) ne produit pas un objet de type Egg(resp. Milk). Par conséquent, si elle n'est pas commentée, la ligne 14 (resp. 16) produirait une erreur de type au moment de la compilation.

L'exemple minimaliste ci-dessus peut être réalisé en utilisant l'héritage , par exemple en dérivant les classes Chickenet Cowd'une classe de base Animal. Cependant, dans un cadre plus large, cela pourrait être désavantageux. L'introduction de nouvelles classes dans une hiérarchie de classes n'est pas nécessairement justifiée pour des raisons transversales , ou peut-être carrément impossible, par exemple lors de l'utilisation d'une bibliothèque externe. Il est possible d'imaginer que l'exemple ci-dessus puisse être étendu avec les classes suivantes :

• une classe Horsequi n'a pas de produceméthode ;
• une classe Sheepqui a une produceméthode renvoyant Wool;
• une classe Pigqui possède une produceméthode, qui ne peut être utilisée qu'une seule fois, renvoyant Meat.

Cela peut nécessiter des classes supplémentaires (ou des interfaces) spécifiant si une méthode de production est disponible, si la méthode de production renvoie de la nourriture et si la méthode de production peut être utilisée de manière répétée. Globalement, cela peut polluer la hiérarchie des classes.

L'exemple minimaliste ci-dessus montre déjà que le typage canard est moins adapté pour réaliser le scénario donné. Bien que la classe RandomNumberGeneratorcontienne une produceméthode, l'objet randomNumberGeneratorne doit pas être un argument valide pour animalToFood. L'exemple ci-dessus peut être réalisé en utilisant le typage canard, par exemple en introduisant un nouveau champ argumentForAnimalToFooddans les classes Chickenet Cowen signifiant que les objets de type correspondant sont des arguments valides pour animalToFood. Cependant, cela augmenterait non seulement la taille des classes respectives (en particulier avec l'introduction de plus de méthodes similaires à animalToFood), mais constitue également une approche non locale par rapport à animalToFood.

L'exemple ci-dessus peut être réalisé en utilisant la surcharge de fonction , par exemple en implémentant deux méthodes et . En TypeScript, une telle solution est presque identique à l'exemple fourni. D'autres langages de programmation, tels que Java , nécessitent des implémentations distinctes de la méthode surchargée. Cela peut conduire soit à une duplication de code , soit à du code standard . animalToFood(animal:Chicken):EgganimalToFood(animal:Cow):Milk

L'exemple ci-dessus peut être réalisé en utilisant le modèle visiteur . Il faudrait que chaque classe animale implémente une acceptméthode acceptant un objet implémentant l'interface (en ajoutant du code standardAnimalVisitor non local ). La fonction serait réalisée comme la méthode d'une implémentation de . Malheureusement, la connexion entre le type d'entrée ( ou ) et le type de résultat ( ou ) serait difficile à représenter. animalToFoodvisitAnimalVisitorChickenCowEggMilk

D'une part, les types d'intersection peuvent être utilisés pour annoter localement différents types d'une fonction sans introduire de nouvelles classes (ou interfaces) dans la hiérarchie des classes. D'autre part, cette approche nécessite que tous les types d'arguments et de résultats possibles soient spécifiés explicitement. Si le comportement d'une fonction peut être spécifié avec précision par une interface unifiée, un polymorphisme paramétrique ou un typage de canard , alors la nature verbeuse des types d'intersection est défavorable. Par conséquent, les types d'intersection doivent être considérés comme complémentaires aux méthodes de spécification existantes.

Un type d'intersection dépendant , noté , est un type dépendant dans lequel le type peut dépendre de la variable terme . En particulier, si un terme a le type d'intersection dépendant , alors le terme a à la fois le type et le type , où est le type qui résulte du remplacement de toutes les occurrences de la variable terme dans par le terme .

Scala prend en charge les déclarations de type en tant que membres d'objet. Cela permet à un type d'un membre d'objet de dépendre de la valeur d'un autre membre, ce qui est appelé un type dépendant du chemin . Par exemple, le texte de programme suivant définit un trait Scala Witness, qui peut être utilisé pour implémenter le modèle singleton .

trait Témoin { type T val valeur : T {} }

Le trait ci-dessus Witnessdéclare le membre T, auquel un type peut être assigné comme valeur, et le membre value, auquel une valeur de type peut être assignée T. Le texte de programme suivant définit un objet booleanWitnesscomme instance du trait ci-dessus Witness. L'objet booleanWitnessdéfinit le type Tcomme Booleanet la valeur valuecomme true. Par exemple, l'exécution d'impressions sur la console. System.out.println(booleanWitness.value)true

objet booléenTémoin étend Témoin { type T = Booléen val valeur = vrai }

Soit le type (plus précisément, un type d'enregistrement ) des objets ayant le membre de type . Dans l'exemple ci-dessus, l'objet peut se voir attribuer le type d'intersection dépendant . Le raisonnement est le suivant. L'objet a le membre auquel est attribué le type comme valeur. Étant donné que est un type, l'objet a le type . De plus, l'objet a le membre auquel est attribuée la valeur de type . Étant donné que la valeur de est , l'objet a le type . Globalement, l'objet a le type d'intersection . Par conséquent, en présentant l'auto-référence comme une dépendance, l'objet a le type d'intersection dépendant . booleanWitnessbooleanWitnessTBooleanBooleanbooleanWitnessbooleanWitnessvaluetrueBooleanbooleanWitness.TBooleanbooleanWitnessbooleanWitnessbooleanWitness

Alternativement, l'exemple minimaliste ci-dessus peut être décrit en utilisant des types d'enregistrement dépendants . Par rapport aux types d'intersection dépendants, les types d'enregistrement dépendants constituent un concept théorique de type strictement plus spécialisé.

Une intersection d'une famille de types , notée , est un type dépendant dans lequel le type peut dépendre de la variable terme . En particulier, si un terme est de type , alors pour chaque terme de type , le terme est de type . Cette notion est également appelée type Pi implicite , en observant que l'argument n'est pas conservé au niveau du terme.