| ... [ GADTs in Haskell ] ... [ << Beispiele für GADTs ] ... [ Fazit >> ] ... | |
 |
Übersicht: Verwandte Themen
Einleitung (Verwandte Themen)In diesem Abschnitt werden zwei Konzepte vorgestellt, welche nicht mehr zu den GADTs gehören. Beide Konzepte verfolgen jedoch eine ähnliche Idee wie die GADTs, nämlich die Erweiterung des Typsystems. Daher werden diese hier kurz vorgestellt.Associated TypesAssociated Types (etwa gekoppelte Typen), sind Funktionen über Typen, welche in verschiedenen Instanzen einer Typklasse verschiedene Werte annehmen können. Da es sich um Funktionen über Typen handelt, sind Werte hier auch wiederum Typen. Solche Funktionen haben Ähnlichkeit zu Typkonstruktoren.
Wir betrachtet zunächst die vordefinierte Num-Typklasse, sowie die Instanz für
den Typ Int:
class Num a where
(+++) :: a -> a -> a
instance Num Int where
(+++) x y = x + y
Wir wählen hier den Operator +++, um dem
vordefinierten +-Operator nicht in die Quere zu
kommen. Dieser Operator hat die Einschränkung, dass alle Parametertypen sowie der Rückgabetyp immer identisch sind. Das bedeutet, dass beispielsweise keine Ints und Floats
addiert werden können.
Mit Associated Types können wir eine Typklasse definieren, welche verschiedene Typen addieren kann:
class MyNum a b where
type Sum a b :: *
(+++) :: a -> b -> Sum a b
Diese Typklasse hat zwei Parameter, so dass wir verschiedene
Typen addieren können. Für den Rückgabetyp wurde eine
Funktion Sum definiert. Diese Funktion bekommt die
Typen a und b als Parameter und gibt
einen Typ, hier syntaktisch als * dargestellt,
zurück.Wir definieren uns nun zunächst eine Instanz für Ints:
instance MyNum Int Int where
type Sum Int Int = Int
(+++) x y = x + y
Da der Rückgabetyp von einer Addition zweier Ints
wieder eine Int sein soll, gibt
die Sum-Funktion Int zurück.Der Rückgabetyp hängt von der jeweiligen Instanz ab; Der Typ ist also an die Instanz gekoppelt. Die Parameter der Typfunktion liegen bereits durch die Typparameter fest. An dieser Stelle ist daher etwas Code-Duplizierung nötig.
Den eigentlichen Nutzen der Typfunktion zeigt das folgende Beispiel:
instance Integral a => MyNum Float a where
type Sum Float a = Float
(+++) x y = x + intToFloat y
Mit dieser Instanz ist es nun möglich, ein Float
und einen Int (genauer: Integral) zu
Addieren. Als Rückgabetyp wurde hier Float
gewählt.Bis jetzt muss allerdings der Float auf der rechten
Seite stehen. Da die Addition kommutativ ist, können wir dies
leicht durch eine zweite Instanz lösen:
instance Integral a => MyNum a Float where
type Sum a Float = Float
(+++) x y = y +++ x
Nun sind auch Ausdrücke wie 42 + 1.5 gültig.
Dependent TypesEine andere Erweiterung des Typsystems bietet die Sprache Agda. Hier werden auch viele Probleme gelöst, welche bei den GADTs entstanden sind.
Unter "Dependent Types" versteht man Typen, die von Werten abhängen. Der tatsächliche Typ steht also erst zur Laufzeit fest.
Ein relativ willkürliches Beispiel verdeutlicht das Prinzip:
q : Σ &8469; (λx → if x = 1 then &8469; else Bool)
q ist hier ein Paar. Das erste Element ist einen
natürliche Zahl (&8469;). Der Typ des zweiten Elements wird durch
eine Funktion bestimmt. Diese Funktion gibt &8469;
zurück, falls der Wert des ersten Elements 1
ist. Ansonsten wird Bool zurückgegeben.q kann nun beispielsweise folgende Werte annehmen:
q = 4, true
q = 1, 42
Mit diesem Konzept sind noch genauere Typüberprüfungen und Invarianten möglich. Anwendungsfälle sind beispielsweise Binäre Suchbäume; hier muss der linke Teilbaum stets kleinere Werte als der rechte Teilbaum enthalten. Auch eine Invariante für Rot-Schwarz-Bäume lässt sich in Agda formulieren.
Problematisch hierbei ist jedoch die Vermischung von Typen und Werten. Dadurch dass beliebige Funktionen definierbar sind kann es zu Endlosschleifen im Typsystem kommen. Das bedeutet, dass ein korrekt implementierter Compiler bei bestimmten Typen in eine Endlosschleife gerät. Die Begründung dafür liefert das Halteproblem: Es ist nicht möglich für alle Programme zu entscheiden, ob diese bei allen Eingaben anhalten. Dies ist nur für triviale Programme möglich. Ein anderes Problem bei Dependent Types ist die Typgleichheit. Es ist nun viel komplizierter zu testen, ob zwei Typen gleich sind. |
| ... [ GADTs in Haskell ] ... [ << Beispiele für GADTs ] ... [ Fazit >> ] ... [ nach oben ] ... | |