Kreuzungstyp - Intersection type

In der Typentheorie kann ein Schnittpunkttyp Werten zugeordnet werden, denen sowohl der Typ als auch der Typ zugeordnet werden können . Dieser Wert kann dem Kreuzungstyp in einem Kreuzungstypsystem zugewiesen werden . Wenn sich die Wertebereiche zweier Typen überlappen, kann im Allgemeinen ein Wert, der zum Schnittpunkt der beiden Bereiche gehört, dem Schnittpunkttyp dieser beiden Typen zugewiesen werden. Ein solcher Wert kann sicher als Argument an Funktionen übergeben werden, die einen der beiden Typen erwarten . In Java implementiert die Klasse beispielsweise sowohl die als auch die Schnittstellen. Daher kann ein Objekt vom Typ sicher an Funktionen übergeben werden, die ein Argument vom Typ erwarten, und an Funktionen, die ein Argument vom Typ erwarten . ${\displaystyle \sigma}$${\displaystyle \tau}$${\displaystyle \sigma \cap \tau}$BooleanSerializableComparableBooleanSerializableComparable

Schnittmengentypen sind zusammengesetzte Datentypen . Ähnlich wie Produkttypen werden sie verwendet, um einem Objekt mehrere Typen zuzuordnen. Produkttypen werden jedoch Tupeln zugeordnet , sodass jedem Tupelelement eine bestimmte Produkttypkomponente zugeordnet ist. Im Vergleich dazu sind zugrundeliegende Objekte von Kreuzungstypen nicht notwendigerweise zusammengesetzt. Eine eingeschränkte Form von Schnittpunkttypen sind Verfeinerungstypen .

Schnittmengentypen sind nützlich, um überladene Funktionen zu beschreiben . Wenn beispielsweise der Funktionstyp eine Zahl als Argument annimmt und eine Zahl zurückgibt, und wenn der Funktionstyp einen String als Argument annimmt und einen String zurückgibt, dann kann die Schnittmenge dieser beiden Typen verwendet werden, um ( überladen) Funktionen, die das eine oder andere tun, je nachdem, welche Art von Eingabe sie erhalten. number => numberstring => string

Zeitgenössische Programmiersprachen, einschließlich Ceylon , Flow, Java , Scala , TypeScript und Whiley (siehe Vergleich von Sprachen mit Schnittmengentypen ), verwenden Schnittmengentypen, um Schnittstellenspezifikationen zu kombinieren und Ad-hoc-Polymorphismus auszudrücken . Ergänzend zum parametrischen Polymorphismus können Schnittmengentypen verwendet werden, um eine Verschmutzung der Klassenhierarchie durch Querschnittsprobleme zu vermeiden und Boilerplate-Code zu reduzieren , wie im folgenden TypeScript-Beispiel gezeigt .

Die typentheoretische Untersuchung von Kreuzungstypen wird als Kreuzungstyp-Disziplin bezeichnet . Bemerkenswerterweise kann die Programmbeendigung mit Hilfe von Kreuzungstypen genau charakterisiert werden.

TypeScript-Beispiel

TypeScript unterstützt Schnittmengentypen, verbessert die Ausdruckskraft des Typsystems und reduziert die potenzielle Größe der Klassenhierarchie, wie im Folgenden gezeigt.

Der folgende Programmcode definiert die Klassen Chicken, Cow, und RandomNumberGeneratordie jeweils eine Methode haben, producedie ein Objekt vom Typ Egg, Milk, oder zurückgibt number. Darüber hinaus sind die Funktionen eatEggund drinkMilkerfordern Argumente vom Typ Eggund Milksind.

class Egg { private kind: "Egg" }
class Milk { private kind: "Milk" }

//produces eggs
class Chicken { produce() { return new Egg(); } }

//produces milk
class Cow { produce() { return new Milk(); } }

//produces a random number
class RandomNumberGenerator { produce() { return Math.random(); } }

//requires an egg
function eatEgg(egg: Egg) {
    return "I ate an egg.";
}

//requires milk
function drinkMilk(milk: Milk) {
    return "I drank some milk.";
}

Der folgende Programmcode definiert die polymorphe Ad-hoc- Funktion animalToFood, die die Memberfunktion producedes angegebenen Objekts aufruft animal. Die Funktion animalToFoodhat zwei Typannotationen, nämlich und , die über den Schnitttypkonstruktor verbunden sind . Insbesondere wird bei Anwendung auf ein Argument des Typs ein Objekt des Typs type zurückgegeben und bei Anwendung auf ein Argument des Typs ein Objekt des Typs type zurückgegeben . Im Idealfall sollte es auf kein Objekt anwendbar sein, das (möglicherweise zufällig) eine Methode hat. ((_: Chicken) => Egg)((_: Cow) => Milk)&animalToFoodChickenEggCowMilkanimalToFoodproduce

//given a chicken, produces an egg; given a cow, produces milk
let animalToFood: ((_: Chicken) => Egg) & ((_: Cow) => Milk) =
    function (animal: any) {
        return animal.produce();
    };

Der folgende Programmcode schließlich demonstriert die typsichere Verwendung der obigen Definitionen.

var chicken = new Chicken();
var cow = new Cow();
var randomNumberGenerator = new RandomNumberGenerator();

console.log(chicken.produce()); //Egg { }
console.log(cow.produce()); //Milk { }
console.log(randomNumberGenerator.produce()); //0.2626353555444987

console.log(animalToFood(chicken)); //Egg { }
console.log(animalToFood(cow)); //Milk { }
//console.log(animalToFood(randomNumberGenerator)); //ERROR: Argument of type 'RandomNumberGenerator' is not assignable to parameter of type 'Cow'

console.log(eatEgg(animalToFood(chicken))); //I ate an egg.
//console.log(eatEgg(animalToFood(cow))); //ERROR: Argument of type 'Milk' is not assignable to parameter of type 'Egg'
console.log(drinkMilk(animalToFood(cow))); //I drank some milk.
//console.log(drinkMilk(animalToFood(chicken))); //ERROR: Argument of type 'Egg' is not assignable to parameter of type 'Milk'

Der obige Programmcode hat folgende Eigenschaften:

• Die Zeilen 1–3 erzeugen Objekte chicken, cow, und randomNumberGeneratorihres jeweiligen Typs.
• Die Zeilen 5–7 drucken für die zuvor erstellten Objekte die jeweiligen Ergebnisse (als Kommentare bereitgestellt) beim Aufruf von produce.
• Zeile 9 (bzw. 10) demonstriert die typsichere Anwendung der Methode animalToFoodauf chicken(bzw. cow).
• Zeile 11, wenn sie nicht auskommentiert ist, würde zur Kompilierzeit zu einem Typfehler führen. Obwohl die Implementierung von animalToFooddie produceMethode von aufrufen könnte randomNumberGenerator, lässt die Typannotation von dies animalToFoodnicht zu. Dies entspricht der beabsichtigten Bedeutung von animalToFood.
• Zeile 13 (bzw. 15) demonstriert, dass die Anwendung animalToFoodauf chicken(bzw. cow) zu einem Objekt vom Typ Egg(bzw. Milk) führt.
• Zeile 14 (bzw. 16) zeigt, dass die Anwendung animalToFoodauf cow(bzw. chicken) kein Objekt vom Typ Egg(bzw. ) ergibt Milk. Daher würde Zeile 14 (bzw. 16) unkommentiert zur Compile-Zeit zu einem Typfehler führen.

Vergleich mit Vererbung

Das obige minimalistische Beispiel kann durch Vererbung realisiert werden , zum Beispiel durch Ableiten der Klassen Chickenund Cowvon einer Basisklasse Animal. In einer größeren Umgebung kann dies jedoch nachteilig sein. Das Einfügen neuer Klassen in eine Klassenhierarchie ist nicht unbedingt aus Querschnittsgründen gerechtfertigt oder vielleicht sogar unmöglich, zum Beispiel bei der Verwendung einer externen Bibliothek. Vorstellbar könnte man das obige Beispiel um folgende Klassen erweitern:

• eine Klasse Horse, die keine produceMethode hat;
• eine Klasse Sheep, die eine produceMethode zurückgibt Wool;
• eine Klasse Pigmit einer produceMethode, die nur einmal verwendet werden kann und zurückgibt Meat.

Dies kann zusätzliche Klassen (oder Schnittstellen) erfordern, die angeben, ob eine Produktmethode verfügbar ist, ob die Produktmethode Lebensmittel zurückgibt und ob die Produktmethode wiederholt verwendet werden kann. Insgesamt kann dies die Klassenhierarchie verschmutzen.

Vergleich zur Ententypisierung

Das obige minimalistische Beispiel zeigt bereits, dass Duck-Typing weniger geeignet ist, um das gegebene Szenario zu realisieren. Während die Klasse RandomNumberGeneratoreine produceMethode enthält , sollte das Objekt randomNumberGeneratorkein gültiges Argument für sein animalToFood. Das obige Beispiel kann mit Duck-Typing realisiert werden, indem zum Beispiel ein neues Feld argumentForAnimalToFoodin die Klassen eingeführt Chickenund angegeben wird Cow, dass Objekte des entsprechenden Typs gültige Argumente für sind animalToFood. Dies würde jedoch nicht nur die Größe der jeweiligen Klassen erhöhen (insbesondere mit der Einführung weiterer Methoden ähnlich wie animalToFood), sondern ist auch ein nicht-lokaler Ansatz in Bezug auf animalToFood.

Vergleich zu Funktionsüberlastung

Das obige Beispiel kann durch Funktionsüberladung realisiert werden , zum Beispiel durch die Implementierung von zwei Methoden und . In TypeScript ist eine solche Lösung fast identisch mit dem bereitgestellten Beispiel. Andere Programmiersprachen wie Java erfordern unterschiedliche Implementierungen der überladenen Methode. Dies kann entweder zu Codeduplizierung oder Boilerplate-Code führen . animalToFood(animal: Chicken): EgganimalToFood(animal: Cow): Milk

Vergleich zum Besuchermuster

Das obige Beispiel lässt sich anhand des Besuchermusters realisieren . Es würde erfordern, dass jede Tierklasse eine acceptMethode implementiert , die ein Objekt akzeptiert, das die Schnittstelle implementiert AnimalVisitor(Hinzufügen von nicht-lokalem Boilerplate-Code ). Die Funktion animalToFoodwürde als visitMethode einer Implementierung von realisiert werden AnimalVisitor. Leider wäre der Zusammenhang zwischen dem Eingabetyp ( Chickenoder Cow) und dem Ergebnistyp ( Eggoder Milk) schwer darzustellen.

Einschränkungen

Einerseits können Schnittmengentypen verwendet werden, um unterschiedliche Typen einer Funktion lokal zuzuordnen, ohne neue Klassen (oder Schnittstellen) in die Klassenhierarchie einzuführen. Andererseits erfordert dieser Ansatz, dass alle möglichen Argumenttypen und Ergebnistypen explizit angegeben werden. Wenn das Verhalten einer Funktion entweder durch eine vereinheitlichte Schnittstelle, parametrischen Polymorphismus oder Duck-Typing genau spezifiziert werden kann , dann ist die ausführliche Natur von Schnittmengentypen ungünstig. Daher sollten Kreuzungstypen als Ergänzung zu bestehenden Spezifikationsmethoden betrachtet werden.

Abhängiger Kreuzungstyp

Ein abhängiger Schnittpunkttyp , bezeichnet , ist ein abhängiger Typ , bei dem der Typ vom Begriff Variable abhängen kann . Insbesondere wenn ein Begriff der abhängigen Kreuzungstyp hat , dann ist der Begriff hat , sowohl den Typ und die Art , in der der Typ ist, der aus dem Ersetzen aller Vorkommen des Begriffs unterschiedliche Ergebnisse in durch den Begriff . ${\displaystyle (x:\sigma )\cap \tau }$${\displaystyle \tau}$${\displaystyle x}$${\displaystyle M}$${\displaystyle (x:\sigma )\cap \tau }$${\displaystyle M}$${\displaystyle \sigma}$${\displaystyle \tau [x:=M]}$${\displaystyle \tau [x:=M]}$${\displaystyle x}$${\displaystyle \tau}$${\displaystyle M}$

Scala-Beispiel

Scala unterstützt Typdeklarationen als Objektmember. Dadurch kann ein Typ eines Objektmembers vom Wert eines anderen Members abhängen, der als pfadabhängiger Typ bezeichnet wird . Der folgende Programmtext definiert beispielsweise ein Scala-Trait Witness, mit dem das Singleton-Muster implementiert werden kann .

trait Witness {
  type T
  val value: T {}
}

Das obige Merkmal Witnessdeklariert das Element T, dem ein Typ als Wert zugewiesen werden kann, und das Element value, dem ein Wert vom Typ zugewiesen werden kann T. Der folgende Programmtext definiert ein Objekt booleanWitnessals Instanz des obigen Merkmals Witness. Das Objekt booleanWitnessdefiniert den Typ Tals Booleanund den Wert valueals true. Zum Beispiel das Ausführen von Drucken auf der Konsole. System.out.println(booleanWitness.value)true

object booleanWitness extends Witness {
  type T = Boolean
  val value = true
}

Sei der Typ (insbesondere ein Datensatztyp ) von Objekten mit dem Member vom Typ . Im obigen Beispiel kann dem Objekt der abhängige Kreuzungstyp zugewiesen werden . Die Begründung ist wie folgt. Das Objekt hat das Element , dem der Typ als Wert zugewiesen ist . Da es ein Typ ist, hat das Objekt den Typ . Darüber hinaus verfügt das Objekt über den Member , dem der Wert type zugewiesen ist . Da der Wert von is hat , hat das Objekt den Typ . Insgesamt hat das Objekt den Schnittpunkttyp . Daher hat das Objekt, das die Selbstreferenz als Abhängigkeit darstellt, den abhängigen Schnittpunkttyp . ${\displaystyle \langle {\textsf {x}}:\sigma \rangle }$${\displaystyle {\textsf {x}}}$${\displaystyle \sigma}$booleanWitness${\displaystyle (x:\langle {\textsf {T}}:{\text{Type}}\rangle )\cap \langle {\textsf {value}}:x.{\textsf {T}}\rangle }$booleanWitnessTBooleanBooleanbooleanWitness${\displaystyle \langle {\textsf {T}}:{\text{Typ}}\rangle }$booleanWitnessvaluetrueBooleanbooleanWitness.TBooleanbooleanWitness${\displaystyle \langle {\textsf {value}}:{\textsf {booleanWitness.T}}\rangle }$booleanWitness${\displaystyle \langle {\textsf {T}}:{\text{Type}}\rangle \cap \langle {\textsf {value}}:{\textsf {booleanWitness.T}}\rangle }$booleanWitness${\displaystyle (x:\langle {\textsf {T}}:{\text{Type}}\rangle )\cap \langle {\textsf {value}}:x.{\textsf {T}}\rangle }$

Alternativ kann das obige minimalistische Beispiel mit abhängigen Datensatztypen beschrieben werden . Im Vergleich zu abhängigen Schnittmengentypen stellen abhängige Datensatztypen ein streng spezialisierteres typtheoretisches Konzept dar.

Schnittmenge einer Typenfamilie

Ein Schnittpunkt einer Typfamilie , bezeichnet , ist ein abhängiger Typ , bei dem der Typ vom Begriff Variable abhängen kann . Insbesondere dann , wenn ein Begriff , die Art hat , dann für jeden Begriff des Typs , der Begriff hat den Typen . Dieser Begriff wird auch als impliziter Pi-Typ bezeichnet , wobei zu beachten ist, dass das Argument nicht auf Termebene gehalten wird. ${\displaystyle \bigcap _{x:\sigma}\tau}$${\displaystyle \tau}$${\displaystyle x}$${\displaystyle M}$${\displaystyle \bigcap _{x:\sigma}\tau}$${\displaystyle N}$${\displaystyle \sigma}$${\displaystyle M}$${\displaystyle \tau [x:=N]}$${\displaystyle N}$

Vergleich von Sprachen mit Kreuzungstypen

Verweise