 |
Übersicht: Von ADTs zu GADTs
ADTs
Algebraische Datentypen (kurz ADT, [aːdeːteː], auch
Summen-Datentypen) sind Datentypen, die eine Verzweigung abbilden.
data X = X1 A | X2 B | ...
Hier ist X der algebraische Datentyp, X1,
X2, ... sind Konstruktorfunktionen. X1
konstruiert aus einem Wert vom Typ A einen Wert
vom Typ X, welcher den Wert vom
Typ A speichert.
Die Menge der Konstruktorfunktionen ist stets endlich. Der
Wertebereich von X kann abhängig von den
Wertebereichen A, B, ... endlich oder unendlich
sein:
|X| = |A| + |B| + ...
X enthält die Werte {a1, a2, a3, ..., b1, b2,
b3}, wobei diese jeweils in ein Konstruktor X1, X2,
... eingepackt werden.
Dies entspricht einer einstufigen Vererbung aus der
Objektorientierung, wobei X die abstrakte
Oberklasse ist, und X1, X2, ... die konkreten
Unterklassen von X.
Für ADTs gibt es viele Anwendungsfälle,
z.B. Abstrakte-Syntax-Bäume oder allgemeiner: rekursive
Datenstrukturen.
Phantomtypen
In ADTs sind beliebig viele Typparameter möglich. Im
vordefinierten Listendatentyp werden sie verwendet, um den
Datentyp Liste vom Elementtyp unabhängig zu machen:
data List a = Nil
| Cons a (List a)
Listenfunktionen können nun auch unabhängig vom Elementtyp
implementiert werden.
Phantomtypen sind solche Typprarameter, die auf
der rechten Seite der Typgleichung nicht verwendet werden:
data PList a b = Nil
| Cons a (List a b)
Natürlich wird b hier auf der rechten Seite
verwendet; allerdings nur bei der Rekursion. Es gibt kein
Attribut, welches tatsächlich den Typ b hat. Daher
nennt man b Phantomtyp.
Mit Phantomtypen ist es möglich, verschiedene Listen mit dem
gleichen Elementtyp voneinander zu unterscheiden. Solche Listen
sind nicht mehr typgleich:
data Euro = ...
data USD = ...
euroToUsd :: PList Int Euro -> PList Int USD
Das Beispiel verdeutlicht, dass nun Int-Listen verschiedene
Semantik haben können: Euro-Listen können nicht mehr mit
USD-Listen vertauscht werden, obwohl beide den Elementtyp Int
haben.
Dieses Ziel kann man auch auf andere Weise erreichen; es geht
hier jedoch zunächst nur um die Verwendung von Phantomtypen, da
diese oft mit GADTs kombiniert werden, um das gewünschte
Ergebnis zu erzielen.
Einschränkung von Typparametern
Eine kleine Erweiterung durch GADTs ist die Möglichkeit der
Einschränkungen von Typprarametern.
Eine Einschränkung wird hier durch eine Typklassen-Zugehörigkeit
angegeben:
data NumList a = NNil
| Num a => NCons a (NumList a)
NCons hat, wie die allgemeine Liste, ein Attribut
von Typ a für das zu speichernde Element und ein
Attribut vom Typ NumList a für die Restliste.
Der Konstruktor NCons akzeptiert nun jedoch nur
noch Elementtypen a, welche die Num
Typklasse instanzieren.
Diese Einschränkung gilt jedoch nur für den
Konstruktor NCons und nicht für den gesamten
Typkonstruktor NumList. Der Typ NumList
String ist daher zulässig. Es gibt jedoch in diesem Fall
nur einen Wert von diesem Typ: NNil.
Erweiterung der Rückgabetypen
Die wichtigste Neuerung durch GADTs ist jedoch die Erweiterung
der Rückgabetypen. In dem Typ List haben alle
Typkonstruktoren (Nil und Cons) den
gleichen Rückgabetyp List a.
Diese Einschränkung wird bei GADTs aufgehoben.
Um verschiedene Rückgabetypen zu ermöglichen, wurde die Syntax
erweitert. Hier ist eine zum bekannten Listen-Typ äquivalente
Definition mit der neuen Syntax:
data List a where
Nil :: List a
Cons :: a -> List a -> List a
Bei dieser Syntax ist die funktionale Sichtweise direkt
erkennbar: Cons ist eine Funktion mit zwei
Parametern a und List a sowie dem
Rückgabetyp List a.
Hier ein Beispiel, welches verdeutlich, welche Möglichkeiten die
neue Syntax bietet:
Cons1 :: a -> List a -> List a
Cons2 :: a -> List a -> List (a,a)
Cons3 :: a -> List a -> List (List a)
Cons4 :: a -> List a -> a -- Fehler
Der Rückgabetyp ist beliebig; solange als Typkonstruktor der
GADT selbst verwendet wird.
Im nächsten Abschnitt wird anhand von Beispielen gezeigt, wie
man diese Erweiterung sinnvoll einsetzen kann.
|
