Unterschreiben - Subtyping

In der Programmiersprachentheorie ist die Subtypisierung (auch Subtyp-Polymorphismus oder Inklusions-Polymorphismus ) eine Form des Typ-Polymorphismus, bei der ein Subtyp ein Datentyp ist, der mit einem anderen Datentyp (dem Supertyp ) durch einen Begriff der Ersetzbarkeit verwandt ist , was bedeutet, dass Programmelemente, typischerweise Unterprogramme oder Funktionen, die geschrieben wurden, um mit Elementen des Supertyps zu arbeiten, können auch mit Elementen des Untertyps arbeiten. Wenn S ein Subtyp von T ist, die Subtypisierung Beziehung wird oft geschrieben S <: T, bedeuten , dass jeder Begriff vom Typ S kann sicher in einem Kontext verwendet , wo ein Begriff des Typs T erwartet wird. Die genaue Semantik der Subtypisierung hängt entscheidend davon ab, was "sicher in einem Kontext verwendet" in einer bestimmten Programmiersprache bedeutet . Das Typsystem einer Programmiersprache definiert im Wesentlichen seine eigene Subtyping-Relation, die durchaus trivial sein kann , sollte die Sprache keine (oder nur sehr wenige) Konvertierungsmechanismen unterstützen.

Aufgrund der Subtypisierungsbeziehung kann ein Begriff zu mehr als einem Typ gehören. Die Subtypisierung ist daher eine Form des Typpolymorphismus. In der objektorientierten Programmierung wird der Begriff "Polymorphismus" allgemein verwendet, um sich ausschließlich auf diesen Untertyp Polymorphismus zu beziehen , während die Techniken des parametrischen Polymorphismus als generische Programmierung betrachtet werden .

Funktionale Programmiersprachen erlauben oft die Untertypisierung von Datensätzen . Folglich ist der einfach typisierte Lambda-Kalkül, erweitert um Datensatztypen, vielleicht die einfachste theoretische Einstellung, in der ein nützlicher Begriff der Subtypisierung definiert und untersucht werden kann. Da der resultierende Kalkül zulässt, dass Terme mehr als einen Typ haben, ist es keine "einfache" Typtheorie mehr . Da funktionale Programmiersprachen per Definition Funktionsliterale unterstützen , die auch in Datensätzen gespeichert werden können, bieten Datensatztypen mit Untertypisierung einige der Merkmale der objektorientierten Programmierung. Typischerweise bieten funktionale Programmiersprachen auch einige, normalerweise eingeschränkte Formen von parametrischem Polymorphismus. In einer theoretischen Umgebung ist es wünschenswert, das Zusammenspiel der beiden Merkmale zu untersuchen; eine übliche theoretische Einstellung ist das System F _<: . Aus dem System F _<: können verschiedene Kalküle abgeleitet werden, die versuchen, die theoretischen Eigenschaften der objektorientierten Programmierung zu erfassen .

Das Konzept der Subtypisierung ist mit den linguistischen Begriffen Hyponymie und Holonymie verwandt . Es hängt auch mit dem Konzept der beschränkten Quantifizierung in der mathematischen Logik zusammen (siehe Ordnungssortierte Logik ). Subtyping sollte nicht mit dem Begriff der (Klassen- oder Objekt-) Vererbung von objektorientierten Sprachen verwechselt werden ; Subtyping ist eine Beziehung zwischen Typen (Schnittstellen im objektorientierten Sprachgebrauch), während Vererbung eine Beziehung zwischen Implementierungen ist, die aus einer Sprachfunktion stammen, die es ermöglicht, neue Objekte aus bestehenden zu erstellen. In einer Reihe von objektorientierten Sprachen wird die Subtypisierung als Schnittstellenvererbung bezeichnet , wobei die Vererbung als Implementierungsvererbung bezeichnet wird .

Ursprünge

Der Begriff der Subtypisierung in Programmiersprachen stammt aus den 1960er Jahren; es wurde in Simula- Derivaten eingeführt. Die ersten formalen Behandlungen der Subtypisierung wurden 1980 von John C. Reynolds gegeben, der die Kategorientheorie benutzte , um implizite Konvertierungen zu formalisieren , und Luca Cardelli (1985).

Das Konzept der Subtypisierung hat mit der Einführung der objektorientierten Programmierung durch den Mainstream an Sichtbarkeit gewonnen (und in einigen Kreisen synonym mit Polymorphismus). In diesem Zusammenhang wird das Prinzip der sicheren Substitution oft als Liskov-Substitutionsprinzip bezeichnet , nach Barbara Liskov, die es 1987 in einer Keynote auf einer Konferenz über objektorientierte Programmierung popularisierte Die von Liskov und Jeannette Wing definierte sogenannte Behavioral Subtyping ist wesentlich stärker als das, was in einem Typchecker implementiert werden kann . (Siehe § Funktionstypen unten für Details.)

Beispiele

Beispiel für Untertypen: wobei Vogel der Supertyp ist und alle anderen Untertypen sind, wie durch den Pfeil in der UML- Notation angezeigt

Ein einfaches praktisches Beispiel für Subtypen ist in der Abbildung rechts dargestellt. Der Typ "Vogel" hat drei Untertypen "Ente", "Kuckuck" und "Strauß". Konzeptionell ist jeder von diesen eine Varietät des Grundtyps "Vogel", der viele "Vogel"-Eigenschaften erbt, aber einige spezifische Unterschiede aufweist. In diesem Diagramm wird die UML- Notation verwendet, wobei Pfeile mit offener Spitze die Richtung und den Typ der Beziehung zwischen dem Supertyp und seinen Untertypen anzeigen.

Als praktischeres Beispiel könnte eine Sprache die Verwendung von ganzzahligen Werten überall dort zulassen, wo Gleitkommawerte erwartet werden ( Integer<: Float), oder sie könnte einen generischen Typ definierenNummerals gemeinsamer Supertyp von ganzen Zahlen und den reellen Zahlen. In diesem zweiten Fall haben wir nur Integer<: Numberund Float<: Numberaber Integerund Floatsind nicht Subtypen voneinander.

Programmierer können Subtyping nutzen , um Code auf abstraktere Weise zu schreiben, als dies ohne sie möglich wäre. Betrachten Sie das folgende Beispiel:

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

Wenn integer und real beide Untertypen von Numbersind und für beide Typen ein Vergleichsoperator mit einer beliebigen Zahl definiert ist, können Werte beider Typen an diese Funktion übergeben werden. Die Möglichkeit, einen solchen Operator zu implementieren, schränkt jedoch den Typ Zahl stark ein (zum Beispiel kann man eine ganze Zahl nicht mit einer komplexen Zahl vergleichen), und eigentlich macht nur der Vergleich von ganzen Zahlen mit ganzen Zahlen und reellen mit reellen Zahlen Sinn. Um diese Funktion so umzuschreiben, dass sie nur 'x' und 'y' des gleichen Typs akzeptiert, ist ein beschränkter Polymorphismus erforderlich .

Subsumtion

In der Typentheorie wird das Konzept der Subsumtion verwendet, um zu definieren oder zu bewerten, ob ein Typ S ein Untertyp des Typs T ist .

Ein Typ ist eine Menge von Werten. Die Menge kann extensional beschrieben werden, indem alle Werte aufgelistet werden, oder sie kann intensional beschrieben werden, indem die Zugehörigkeit der Menge durch ein Prädikat über einen Bereich möglicher Werte angegeben wird. In gängigen Programmiersprachen werden Aufzählungstypen durch Auflisten von Werten erweitert definiert. Benutzerdefinierte Typen wie Records (Structs, Interfaces) oder Klassen werden absichtlich durch eine explizite Typdeklaration oder durch die Verwendung eines vorhandenen Werts, der Typinformationen kodiert, als Prototyp zum Kopieren oder Erweitern definiert.

Bei der Diskussion des Konzepts der Subsumtion wird die Menge der Werte eines Typs durch die mathematische Kursivschrift des Namens angegeben: T . Der Typ, der als Prädikat über einer Domäne betrachtet wird, wird durch Fettdruck angezeigt: T . Das konventionelle Symbol <: bedeutet "ist ein Untertyp von" und :> bedeutet "ist ein Supertyp von".

• Ein Typ T subsumiert S, wenn die Menge von Werten T, die er definiert, eine Obermenge der Menge S ist , so dass jedes Mitglied von S auch ein Mitglied von T ist .
• Ein Typ kann von mehr als einem Typ subsumiert werden: Die Supertypen von S schneiden sich bei S .
• Wenn S <: T (und damit S ⊆ T ), dann muss T , das Prädikat, das die Menge T umschreibt , Teil des Prädikats S (über dem gleichen Gebiet) sein, das S definiert .
• Wenn S subsumiert T und T subsumiert S , dann sind die beiden Arten gleich (obwohl sie nicht vom gleichen Typ , wenn der Typ System unterscheidet Typen von Namen sein kann).

Als Faustregel gilt: Ein Subtyp ist wahrscheinlich "größer/breiter/tiefer" (seine Werte enthalten mehr Informationen) und "weniger/kleiner" (der Wertesatz ist kleiner) als einer seiner Supertypen (der stärker eingeschränkt ist) Informationen, und deren Wertemenge eine Obermenge derjenigen des Untertyps ist).

Im Kontext der Subsumtion können die Typdefinitionen mithilfe der Set-Builder-Notation ausgedrückt werden , die ein Prädikat verwendet, um eine Menge zu definieren. Prädikate können über eine Domäne (Menge möglicher Werte) definiert werden D . Prädikate sind Teilfunktionen, die Werte mit Auswahlkriterien vergleichen. Beispiel: "Ist ein ganzzahliger Wert größer oder gleich 100 und kleiner als 200?". Wenn ein Wert den Kriterien entspricht, gibt die Funktion den Wert zurück. Wenn nicht, wird der Wert nicht ausgewählt und es wird nichts zurückgegeben. (Listenverständnisse sind eine Form dieses Musters, die in vielen Programmiersprachen verwendet wird.)

Wenn es zwei Prädikate gibt, die Selektionskriterien für den Typ T anwendet und die zusätzliche Kriterien für den Typ S anwendet , können Mengen für die beiden Typen definiert werden: ${\displaystyle P_{T}}$${\displaystyle P_{s}}$

${\displaystyle T=\{v\in D\mid\P_{T}(v)\}}$

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

Das Prädikat wird daneben als Teil des zusammengesetzten Prädikats S verwendet , das S definiert . Die beiden Prädikate sind verbunden , daher müssen beide wahr sein, damit ein Wert ausgewählt wird. Das Prädikat subsumiert das Prädikat T , also S <: T .${\displaystyle \mathbf{T} =P_{T}}$${\displaystyle P_{s}}$${\displaystyle \mathbf{S} =\mathbf{T} \land P_{s}=P_{T}\land P_{s}}$

Zum Beispiel: Es gibt eine Unterfamilie von Katzenarten namens Felinae , die zur Familie Felidae gehört . Zu dieser Unterfamilie gehört die Gattung Felis , zu der die Hauskatzenart Felis catus gehört.

${\displaystyle {\mathit {Felinae=\{cat\in Felidae\mid\ ofSubfamily(cat,felinaeSubfamilyName)\}}}}$

${\displaystyle {\mathit {Felis=\{Katze\in Felinae\mid\ ofGenus(cat,felisGenusName)\}}}}$

Die Konjunktion der Prädikate wurde hier durch die Anwendung des zweiten Prädikats über den dem ersten Prädikat entsprechenden Wertebereich ausgedrückt. Als Typen betrachtet, Felis <: Felinae <: Felidae .

Wenn T S subsumiert ( T :> S ), dann kann eine Prozedur, Funktion oder ein Ausdruck mit einem Wert als Operand (Eingabeargument oder Term) diesen Wert als einen Wert vom Typ T verarbeiten , weil . Im obigen Beispiel könnten wir erwarten, dass die Funktion der Unterfamilie auf Werte aller drei Typen Felidae , Felinae und Felis anwendbar ist . ${\displaystyle s\in S}$${\displaystyle s\in T}$

Subtyping-Schemata

Typtheoretiker unterscheiden zwischen nominaler Subtypisierung , bei der nur auf eine bestimmte Weise deklarierte Typen Subtypen voneinander sein können, und struktureller Subtypisierung , bei der die Struktur zweier Typen bestimmt, ob einer ein Subtyp des anderen ist oder nicht. Die oben beschriebene klassenbasierte objektorientierte Untertypisierung ist nominell; eine strukturelle Untertypisierungsregel für eine objektorientierte Sprache könnte sagen, dass, wenn Objekte des Typs A alle Nachrichten verarbeiten können, die Objekte des Typs B verarbeiten können ( dh wenn sie alle die gleichen Methoden definieren ), A ein Untertyp von . ist B unabhängig davon, ob einer vom anderen erbt . Dieses sogenannte Duck-Typing ist in dynamisch typisierten objektorientierten Sprachen üblich. Solide strukturelle Subtypisierungsregeln für andere Typen als Objekttypen sind ebenfalls gut bekannt.

Implementierungen von Programmiersprachen mit Subtyping fallen in zwei allgemeine Klassen: inklusive Implementierungen, in denen die Darstellung eines beliebigen Wertes vom Typ A auch den gleichen Wert am Typ B darstellt, wenn A  <:  B , und Zwangsimplementierungen , in denen ein Wert vom Typ A kann automatisch in einen Typ B umgewandelt werden . Die Subtypisierung, die durch die Subklassenbildung in einer objektorientierten Sprache induziert wird, ist normalerweise inklusiv; Subtyping-Beziehungen, die sich auf ganze Zahlen und Gleitkommazahlen beziehen, die unterschiedlich dargestellt werden, sind normalerweise erzwungen.

In fast allen Typsystemen, die eine Subtypisierungsrelation definieren, ist sie reflexiv (was A  <:  A für jeden Typ A bedeutet ) und transitiv (was bedeutet, dass wenn A  <:  B und B  <:  C dann A  <:  C ist ). Dies macht es zu einer Vorbestellung für Typen.

Datensatztypen

Breiten- und Tiefensubtypisierung

Typen von Datensätzen führen zu den Konzepten der Untertypisierung von Breite und Tiefe . Diese drücken zwei verschiedene Möglichkeiten aus, einen neuen Datensatztyp zu erhalten, der dieselben Operationen wie der ursprüngliche Datensatztyp ermöglicht.

Denken Sie daran, dass ein Datensatz eine Sammlung von (benannten) Feldern ist. Da ein Untertyp ein Typ ist, der alle Operationen zulässt, die für den Originaltyp zulässig sind, sollte ein Datensatzuntertyp die gleichen Operationen an den Feldern unterstützen wie der Originaltyp.

Eine Möglichkeit, eine solche Unterstützung zu erreichen, heißt width subtyping , fügt dem Datensatz weitere Felder hinzu. Formaler ausgedrückt, wird jedes (benannte) Feld, das im Supertyp width erscheint, im Subtyp width angezeigt. Somit wird jede Operation, die mit dem Supertyp durchführbar ist, vom Untertyp unterstützt.

Die zweite Methode, die Tiefensubtypisierung genannt wird , ersetzt die verschiedenen Felder durch ihre Untertypen. Das heißt, die Felder des Subtyps sind Subtypen der Felder des Supertyps. Da jede Operation, die für ein Feld im Supertyp unterstützt wird, auch für seinen Subtyp unterstützt wird, wird jede Operation, die für den Datensatz-Supertyp durchführbar ist, vom Datensatz-Subtyp unterstützt. Die Subtypisierung der Tiefe ist nur für unveränderliche Datensätze sinnvoll: Sie können beispielsweise dem 'x'-Feld eines reellen Punktes (einem Datensatz mit zwei reellen Feldern) 1,5 zuweisen, aber nicht dasselbe für das 'x'-Feld von ein ganzzahliger Punkt (der jedoch ein tiefer Untertyp des realen Punkttyps ist), da 1.5 keine ganze Zahl ist (siehe Varianz ).

Die Subtypisierung von Datensätzen kann in System F _{<: definiert werden} , das parametrischen Polymorphismus mit der Subtypisierung von Datensatztypen kombiniert und eine theoretische Grundlage für viele funktionale Programmiersprachen darstellt , die beide Funktionen unterstützen.

Einige Systeme unterstützen auch die Subtypisierung von gekennzeichneten disjunkten Vereinigungstypen (wie algebraische Datentypen ). Die Regel für die Untertypisierung der Breite ist umgekehrt: Jedes Tag, das im Untertyp width vorkommt, muss im Obertyp width erscheinen.

Funktionstypen

Wenn T ₁ → T ₂ ein Funktionstyp ist, dann ist ein Untertyp davon ein beliebiger Funktionstyp S ₁ → S ₂ mit der Eigenschaft, dass T ₁ <: S ₁ und S ₂ <: T ₂ . Dies lässt sich mit der folgenden Typisierungsregel zusammenfassen :

${\displaystyle T_{1}\leq :S_{1}\quad S_{2}\leq :T_{2} \over S_{1}\rightarrow S_{2}\leq :T_{1}\rightarrow T_{ 2}}$

Der Argumenttyp von S ₁ → S ₂ heißt kontravariant, weil für ihn die Subtypisierungsrelation umgekehrt ist, während der Rückgabetyp kovariant ist . Informell tritt diese Umkehrung auf, weil der verfeinerte Typ in den akzeptierten Typen "liberaler" und in dem zurückgegebenen Typ "konservativer" ist. Genau das funktioniert in Scala : Eine n- äre Funktion ist intern eine Klasse, die das Merkmal erbt (das als allgemeine Schnittstelle in Java- ähnlichen Sprachen angesehen werden kann), wo die Parametertypen sind und B der Rückgabetyp ist; " - " vor dem Typ bedeutet, dass der Typ kontravariant ist, während " + " kovariant bedeutet. ${\displaystyle {\mathtt {Funktion_{N}(-A_{1},-A_{2},\dots,-A_{n},+B)}}}$ ${\displaystyle {\mathtt {A_{1},A_{2},\dots A_{n}}}}$

In Sprachen, die Nebeneffekte zulassen, wie die meisten objektorientierten Sprachen, reicht die Subtypisierung im Allgemeinen nicht aus, um zu garantieren, dass eine Funktion sicher im Kontext einer anderen verwendet werden kann. Liskovs Arbeit in diesem Bereich konzentrierte sich auf die verhaltensbezogene Subtypisierung , die neben der in diesem Artikel diskutierten Typsystemsicherheit auch erfordert, dass Subtypen alle Invarianten beibehalten, die von den Supertypen in einem Vertrag garantiert werden . Diese Definition von Subtyping ist im Allgemeinen unentscheidbar und kann daher nicht durch einen Typchecker überprüft werden .

Die Subtypisierung von veränderlichen Referenzen ähnelt der Behandlung von Funktionsargumenten und Rückgabewerten. Schreibgeschützte Referenzen (oder Senken ) sind kontravariant, wie Funktionsargumente; schreibgeschützte Referenzen (oder Quellen ) sind wie Rückgabewerte kovariant. Veränderliche Referenzen, die sowohl als Quellen als auch als Senken fungieren, sind invariant.

Beziehung zum Erbe

Subtyping und Vererbung sind unabhängige (orthogonale) Beziehungen. Sie mögen zusammenfallen, aber keiner ist ein Sonderfall des anderen. Mit anderen Worten, zwischen zwei Typen S und T sind alle Kombinationen von Subtypisierung und Vererbung möglich:

1. S ist weder ein Untertyp noch ein abgeleiteter Typ von T
2. S ist ein Untertyp, aber kein abgeleiteter Typ von T
3. S ist kein Untertyp, sondern ein abgeleiteter Typ von T
4. S ist sowohl ein Untertyp als auch ein abgeleiteter Typ von T

Der erste Fall wird durch unabhängige Typen wie Booleanund veranschaulicht Float.

Der zweite Fall kann durch die Beziehung zwischen Int32und veranschaulicht werden Int64. In den meisten objektorientierten Programmiersprachen Int64sind sie durch Vererbung nicht mit Int32. Jedoch Int32kann einen Untertyp von in Betracht gezogen werden , Int64da jeder 32 - Bit - Integer - Wert in einen 64 - Bit - Integer - Wert gefördert werden.

Der dritte Fall ist eine Folge der Funktionssubtypisierung der Eingabekontravarianz . Angenommen, eine Superklasse vom Typ T mit einer Methode m, die ein Objekt desselben Typs zurückgibt ( dh der Typ von m ist T → T , beachten Sie auch, dass das erste Argument von m this/self ist) und einen abgeleiteten Klassentyp S von T . Durch Vererbung, die Art des m in S ist S → S . Damit S ein Untertyp von T ist, muss der Typ von m in S ein Untertyp des Typs von m in T sein , mit anderen Worten: S → S ≤: T → T . Bei der Bottom-up-Anwendung der Funktionssubtypisierungsregel bedeutet dies: S ≤: T und T ≤: S , was nur möglich ist, wenn S und T gleich sind. Da Vererbung eine irreflexive Beziehung ist, kann S kein Untertyp von T sein .

Subtyping und Vererbung sind kompatibel, wenn alle geerbten Felder und Methoden des abgeleiteten Typs Typen haben, die Untertypen der entsprechenden Felder und Methoden des geerbten Typs sind.

Zwang

In erzwungenen Subtypisierungssystemen werden Subtypen durch implizite Typumwandlungsfunktionen von Subtyp zu Supertyp definiert. Für jede Subtypisierungsbeziehung ( S <: T ) wird eine Zwangsfunktionserzwingung : S → T bereitgestellt, und jedes Objekt s vom Typ S wird als Objektzwang _{S → T} ( s ) vom Typ T angesehen . Eine Zwangs - Funktion kann durch die Zusammensetzung definiert werden: wenn S <: T und T <: U dann s als ein Objekt des Typs angesehen werden können U unter dem Zwang Verbindung ( coerce _{T → U} ∘ coerce _{S → T} ). Die Art Zwang von einem Typ selbst coerce _{T → T} ist die Identitätsfunktion id _T

Zwangsfunktionen für Datensätze und disjunkte Vereinigungsuntertypen können komponentenweise definiert werden; im Fall von Breiten-erweiterten Datensätzen verwirft Typ-Coercion einfach alle Komponenten, die nicht im Supertyp definiert sind. Der Typ-Zwang für Funktionstypen kann durch f' ( s ) = erzwingen _{S 2 → T 2} ( f ( erzwingen _{T 1 → S 1} ( t ))) angegeben werden, was die Kontravarianz von Funktionsargumenten und die Kovarianz von Rückgabewerten widerspiegelt .

Die Zwangsfunktion ist aufgrund des Subtyps und des Supertyps eindeutig bestimmt . Wenn also mehrere Subtypisierungsbeziehungen definiert werden, muss sorgfältig darauf geachtet werden, dass alle Typumwandlungen kohärent sind. Wenn zum Beispiel eine ganze Zahl wie 2 : int in eine Gleitkommazahl umgewandelt werden kann (z. B. 2.0 : float ), dann ist es nicht zulässig, 2.1 : float zu 2 : int zu erzwingen , da die zusammengesetzte Zwangsbedingung erzwungen _{float → float} gegeben durch coerce _{int → float} ∘ coerce _{float → int} wäre dann verschieden von der Identität coercion id _float .

Siehe auch

• Kovarianz und Kontravarianz
• Das Kreis-Ellipsen-Problem (für die Gefahren der Untertypisierung von Variablentypen auf der gleichen Basis wie Werttypen)
• Klassenbasierte Programmierung
• Top-Typ
• Verfeinerungstyp
• Verhaltenssubtypisierung

Anmerkungen

Verweise

Lehrbücher

Papiere

Weiterlesen