Was sind die praktischen Probleme mit Schnitt- und Vereinigungstypen?

Ich entwerfe eine einfache statisch typisierte funktionale Programmiersprache als Lernerfahrung.

Es scheint, dass das Typsystem, das ich bisher implementiert habe, (mit ein wenig zusätzlicher Arbeit) Schnitt- und Vereinigungstypen enthalten könnte, z. B .:

• <Union String Integer>
• <Union Integer Foo>
• Der Schnittpunkt der beiden oben genannten Typen wäre eine Ebene Integer
• Die Vereinigung der beiden Typen wäre <Union String Integer Foo>

Die Tatsache, dass dies möglich ist, bedeutet natürlich nicht, dass es sich um eine gute Designidee handelt. Insbesondere bin ich etwas besorgt über die Implementierungsschwierigkeiten, die es mit sich bringt, die Typen disjunkt zu halten und / oder Überschneidungen zu behandeln.

Was sind die Vor- / Nachteile der Aufnahme solcher Merkmale in das Typensystem?

Hier sind ein paar Dinge zu beachten:

• Obwohl wir im Allgemeinen glauben, zu wissen, was wir unter satztheoretischer Schnittmenge und Vereinigung verstehen, gab es verschiedene Ansätze, was genau Schnittmenge und Vereinigungstypen sind . Es lohnt sich also, dies festzuhalten, bevor Sie mit einer Implementierung beginnen.
• $S \sqsubset A$"as" verfeinert ") während die Bildungsregeln für gewöhnliche Produkte und Summen $S$$A$ $$\frac{S\sqsubset A \quad T \sqsubset A}{S\cap T\sqsubset A}\qquad \frac{S\sqsubset A \quad T \sqsubset A}{S\cup T\sqsubset A}$$ $$\frac{S\sqsubset A \quad T \sqsubset B}{S* T\sqsubset A*B}\qquad \frac{S\sqsubset A \quad T \sqsubset B}{S+T\sqsubset A+B}$$
• Da Schnittpunkte und Vereinigungen verwendet werden können, um genauere Aussagen über das Laufzeitverhalten eines Programms zu treffen, ist es normal, dass die Eingabe abhängig von der Auswertungsreihenfolge ist. Zum Beispiel wurde in den Abhandlungen (2) und (4) unten erläutert, warum die "offensichtlichen" (und ziemlich standardmäßigen) Typisierungs- und Subtypisierungsregeln für Kreuzungen und Gewerkschaften für ML-ähnliche Sprachen tatsächlich nicht stimmen (aufgrund von Nebenwirkungen und nicht zutreffenden Begriffen). Beendigung). Du wurdest gewarnt!
• Aus ähnlichen Gründen wird die globale Typinferenz im Allgemeinen unpraktisch oder unentscheidbar. In der Tat ist das gesamte Konzept des "Haupttyps" wohl ein roter Hering, da eine Funktion viele verschiedene Eigenschaften erfüllen kann, die für ihre beabsichtigte Verwendung irrelevant sind (z. B. " foo nimmt ganze Primzahlen zu ganzen Zahlen größer als 7"). Stattdessen basieren praktische Ansätze für Kreuzungen und Vereinigungen (siehe (3) , (4) ) im Allgemeinen auf einer Kombination aus Inferenz und Überprüfung.

Ich nehme an, dass einige der oben genannten Punkte negativ klingen, obwohl ich sie nicht "Nachteile" nennen würde, sondern lediglich "Realitäten" von Schnitt- und Vereinigungstypen. Andererseits ist aus Sicht des Sprachdesigns ein Grund für die Bemühung, Schnittmengen und Gewerkschaften zu unterstützen (und richtig zu machen!), Dass sie es ermöglichen, genauere Eigenschaften von Programmen auf eine ziemlich inkrementelle Weise auszudrücken, die eine bestimmte Anzahl von Zeichen erfordert viel weniger drastische Transformation als zum Beispiel abhängige Typentheorie.

Eine kurze Leseliste:

1. Design der Programmiersprache Forsythe von John C. Reynolds
2. Schnittmengen und rechnerische Effekte von Rowan Davies und Frank Pfenning
3. Praktische Verfeinerungsprüfung von Rowan Davies (Dissertation)
4. Tridirektionales Typechecking von Joshua Dunfield und Frank Pfenning