Erweiterungen

Subtypen

Betrachten wir unsere selOrt Funktion aus dem letzten Abschnitt. Sie hat den Typ {strasse:String, ort:String} → String. Nehmen wir einmal an Globalisierungssbestrebungen in unserem Unternehmen hätten dazu geführt, dass wir von nun an einige Adressen mit einem zusätzlichen Länderkennzeichen bestücken. Diese hätten dann zum Beispiel den Typ {strasse:String, ort:String, land:String}. Unsere wertvolle selOrt Funktion würde mit diesen neuen Adressen nicht mehr funktionieren. Es würde zu einem Typfehler kommen, obwohl eigentlich alle nötigen Informationen zur Verfügung stehen. Es wäre schön, wenn man auch mehr Informationen als gefordert liefern könnte, ohne das es zu einem Typfehler kommt. In anderen Worten wenn das Argument einer Funktion einen spezielleren Typ als gefordert haben dürfte. Diese Intuition wollen wir im folgenden mit Hilfe einer operationalen Semantik formalisieren.

In einem ersten Schritt haben wir eine neue Typregel eingeführt, die folgendes besagt: Lässt sich im Kontext Γ der Typ S für dem Term t ableiten, dann darf für den Term t auch ein Typ T eingesetzt werden, solange wie T mindestens so allgemein wie S ist. Statt T ist mindestens so allgemein wie S wird gesagt S ist ein Subtyp von T. Kurz S<:T.

Nun wollen wir die Subtyp-Relation S<:T näher beschreiben. Sie ist reflexiv (Regel 1), transitiv (Regel 2) und es gibt einen allgemeinsten Typ Top (Regel 3). Wir werden noch Gründe für das Einführen des Typs Top kennenlernen. Intuitiv entspricht er der Klasse Object, wie wir sie zum Beispiel aus Java kennen. Die Formulierung der zweiten Regel ist ausserordentlich elegant, macht eine direkte Umsetzung in einem Typprüfer allerdings unmöglich, da wir einen beliebigen Typ U raten müßten. Aus diesem Grund wird unsere Formulierung auch als deklarativ bezeichnet. Für die konkrete Umsetzung müßten wir zunächst ein algorithmisches Subtyping-Regelwerk entwickeln.

In unserem Beispiel ist die Regel (5) ausreichend um den folgenden Ausdruck wohlgetypt werden zu lassen.

(λx:{strasse:String, ort:String}. (x.ort)) {strasse="Feldstraße 143",ort="22880 Wedel", land="D"}

Kovarianz, Contravarianz und Invarianz

Interessanter wird es, wenn wir die Regeln (4) und (6) betrachten. Wir werden dazu die Begriffe kovariant, contravariant und invariant einführen.

Die Typen der Felder eines Records verhalten sich zu dem Typ des Records kovariant. Bekommen die Felder einen spezielleren Typ wird auch der Typ des Records spezieller.
Beispiel: Unit <: Top und {x:Unit,y:Unit} <: {x:Top,y:Unit}.

Die Rückgabetypen einer Funktion verhalten sich kovariant zum Typ der Funktion.
Beispiel: {name:String,strasse:String} <: {name:String} und Unit→{name:String,strasse:String} <: Unit→{name:String}

Die Parametertypen einer Funktion verhalten sich contravariant zu dem Typ der Funktion. In anderen Worten speziellere Funktionen dürfen allgemeinere Parameter haben.
Beispiel: {name:String,strasse:String} <: {name:String} und {name:String}→Unit <: {name:String,strasse:String}→Unit

Die meisten objektorientierten Programmiersprachen (seit Version 1.5 auch Java) unterstützen kovariante Rückgabetypen von dynamisch gebundenen Methoden. Dies ermöglicht es zum Beispiel die clone()-Methode einer Klasse mit einem konkreteren Rückgabetyp als den der Basisklasse zu versehen. Die Programmiersprache Eiffel unterstützt entgegen der typtheoretischen Bedenken kovariante Parametertypen. Dies kann in der Praxis zu Laufzeittypfehlern führen, die auch als catcalls (lustiges Wortspiel, ohne Übersetzung) bezeichnet werden.

Nehmen wir einmal an wir hätten ein Konstrukt für veränderbare Arrays eingeführt. Hier wären die Argumenttypen invariant zum Typ des Arrays.
Technisch: [U]<:[T] ≡ (U<:T ∧ T<:U) .
Beispiel: [{x:Unit,y:Unit}] <: [{y:Unit,x:Unit}] aber nicht [{x:Unit,y:Unit}] <: [{x:Unit}]

Grund ist, dass sonst Elemente eines falschen Typs in ein Array eingefügt werden könnten. Die Sprache Java unterstützt kovarianz bei Arrays, was zu Laufzeittypfehlern führt:

class BrokenArray { public static void main(String [] argv) { String [] strings = {"Hallo", "Welt"}; Object [] objects = strings; objects[0]=new Integer(5); } } Exception in thread "main" java.lang.ArrayStoreException at BrokenArray.main(brokenarray.java:5)

Die falsche Subtypregel in Java führt auch dazu, dass Arrays nicht so effizient arbeiten können, wie das normalerweise möglich wäre. Bei jedem Einfügen eines Elementes muss eine Laufzeittypprüfung stattfinden. Darüberhinaus gestaltet sich das Zusammenspiel von Java 1.5 Generics und Arrays aufgrund dieser Subtypregel problematisch.

Joins und Meets

Ein Typ J wird als Join der Typen S und T bezeichnet (J=S∨T) wenn S<:J und T<:J und fur alle Typen U mit S<:U und T<:U gilt: J<:U.

Ein Typ M wird als Meet der Typen S und T bezeichnet (M=S∧T) wenn M<:S und M<:T und fur alle Typen L mit L<:S und L<:T gilt: L<:M.

In unserem Kalkül gibt es für zwei beliebige Typen imme einen Join. So ist beispielsweise {x:Unit} ∨ {y:Unit} = {} oder {x:unit} ∨ Unit→Unit = Top. (Dieses Beispiel zeigt einen Nutzen vom Typ Top). Der Join muss allerdings nicht eindeutig sein. So sind beispielsweise {x:Unit,z:Unit} und {z:Unit,x:Unit} Join der Typen {x:Unit,z:Unit} und {x:Unit,y:Unit,z:Unit}.

Joins können dazu benutzt werden einen Typ für bedingte Ausdrücke zu bestimmen. Der Ausdruck if b then t else u würde den Typ T∨U bekommen. In Java bekommt der Ausdruck b ? t : u den Typ T, wenn U<:T und den Typ U wenn T<:U. Gilt weder U<:T noch T<:U ist der Ausdruck falsch getypt. Grund dafür ist, dass es in Java für zwei beliebige Typen keinen Join gibt. Erben die Klassen A und B jeweils von den Interfaces I und J ( wobei weder I von J erbt, noch umgekehrt), dann haben sie die gemeinsamen Übertypen I, J und Object. Object kann nicht der Join von A und B sein, da Object nicht spezieller als I ist. I kann nicht der Join sein, da I nicht spezieller als J ist. J kann nicht der Join sein, da J nicht spezieller als I ist. Folglich haben A und B keinen Join.