Beispiele für GADTs

 ... [ GADTs in Haskell ] ... [ << Von ADTs zu GADTs ] ... [ Verwandte Themen >> ] ...  



Übersicht: Beispiele für GADTs

  Vorwort
  Sichere Listen
  Gemischte Listen
  Abstrakte Syntaxbäume
  Vektoren



Vorwort

Alle im Folgenden erläuterten Beispiele befinden sich in Form einer Literate Haskell-Datei (.lhs) im Archiv und sollten zum besseren Verständnis parallel zum Lesen dieser Arbeit ausprobiert werden.

Sichere Listen

In diesem Abschnitt wird ein Datentyp für Listen definiert, der es ermöglicht Listen unterschiedlicher Länge im Typsystem zu unterscheiden.

Im Folgenden werden leere Listen als "unsicher" und nicht leere Listen als "sicher" bezeichnet. Dies hat den Hintergrund, dass einige Funktionen nur auf nicht leeren Listen funktionieren, also nur partiell definiert und somit "unsicher" sind.



Es folgt der Datentyp für sichere Listen: 
	data Safe a = Safe a
	data NotSafe = NotSafe
	data SafeList a b where
	  Nil :: SafeList a NotSafe
	  Cons :: a -> SafeList a b -> SafeList a (Safe b)
Die Hilfsdatentypen Safe und NotSafe können auch als Peano-Zahlen angesehen werden, wobei NotSafe für die Null steht, und Safe für die Nachfolgerfunktion (+1). Diese Zahl interpretieren wir als Länge der Liste.

Der zweite Typparameter hat also folgende Bedeutung: 
	NotSafe             -- leere Liste
	Safe NotSafe        -- Laenge == 1
	Safe b              -- Laenge >= 1
	Safe (Safe NotSafe) -- Laenge == 2
	Safe (Safe b)       -- Laenge >= 2
	b                   -- Laenge beliebig
Mit dieser Information lassen sich nun auch die Rückgabetypen der Konstruktorfunktionen intepretieren: Nil gibt selbstverständlich eine leere Liste zurück und hat daher den Typ NotSafe. Bei Cons ist es etwas komplizierter. Bei Cons ist nur bekannt, dass eine beliebige Liste nun ein Element länger ist. Daher wählen wir den Typ Safe b, wobei b die Länge der Eingabeliste ist.



Der Vorteil dieser Art der Typdefinition ist, dass wir Listenfunktionen nun noch typsicherer definieren können. Die Funktion safeHead ist der vordefinierten Funktion head nachempfunden: 
	1  safeHead :: SafeList a (Safe b) -> a
	2  safeHead (Cons x _) = x
	3  -- safeHead Nil = ???
safeHead hat als Parameter den gleichen Typ den Cons zurückgibt: Eine Liste mit mindestens einem Element. safeHead benutzt wie bei ADTs auch Patternmatching. Im Gegensatz zu head wurde jedoch die zweite Funktionsgleichung mit dem Pattern Nil weggelassen. Diese ist nun auch nicht mehr nötig, da ja bereits der Typparameter festlegt, dass die Liste nicht leer sein kann. Genaugenommen muss die Gleichung weggelassen werden, da das Pattern Nil nicht auf den Typ SafeList a (Safe b) passt.

Der Versuch, safeHead auf einer leeren Liste aufzurufen führt unweigerlich zu einem Compilerfehler.

Es ist aber immer noch möglich eine unsichere Variante von head zu implementieren: 
	unsafeHead :: SafeList a b -> a
	unsafeHead (Cons x _) = x
	unsafeHead Nil = error "error in head!"
Hier muss für den zweiten Typparameter allerdings eine freie Variable (hier b) gewählt werden, um anzugeben, dass die Länge der Liste unbekannt ist. unsafeHead verhält sich nun genau so wie die vordefinierte head-Funktion.



Analog zu safeHead kann auch safeTail definiert werden: 
	safeTail :: SafeList a (Safe b) -> SafeList a b
	safeTail (Cons _ t) = t
Bei dieser Funktion haben wir durch den GADT einen weiteren Vorteil: Der Typ der Rückgabeliste "weiss", dass die Rückgabeliste ein Element weniger hat als die Eingabeliste: b steht für eine beliebig lange Liste und Safe b steht für eine Liste, die ein Element länger ist, als die Liste vom Typ b.

Der Compiler wird uns nun also auch daran hindern, auf einer ein-elementigen Liste zweifach safeTail aufzurufen.



An den Beispielen safeHead und safeTail sieht man, dass partiell definierten Funktionen leicht in total definierte Funktionen transformiert werden können.

Es stellt sich die Frage, ob dies mit allen Funktionen möglich ist. Dazu betrachtet wir die Funktion accessN, welche den indizierten Zugriff auf ein Listenelement ermöglichen soll. Wir versuchen hier also eine sichere Variante zu definieren: 
	accessN :: Int
	           -> SafeList a (Safe (Safe (Safe ...)))
	           -> a
Die Funktion bekommt den Index und eine Liste und soll eine Element daraus zurückgeben.

Es ist bereits an den drei Punkten erkennbar, dass wir diese Funktion so nicht definieren können. Der Grund dafür ist, dass die Länge der Liste abhängig vom ersten Parameter ist, also erst zur Laufzeit bekannt ist.

Bei der Funktion accessN haben wir also durch die Verwendung von GADTs nichts gewonnen (aber auch nichts verloren). Wir müssen den Parameter so definieren, dass eine beliebige Liste angenommen wird: 
	accessN :: Int
	           -> SafeList a b
	           -> a
	accessN n Nil = error "error in accessN"
	accessN 0 (Cons e _) = e
	accessN n (Cons e l) = accessN (n-1) l
Da eine beliebige Liste als Typ angegeben wurden, müssen alle Fallunterscheidungen implementiert werden.



Betrachten wir als nächstes zwei Funktionen, die bereits ohne GADTs total definiert sind: map und fold. Es stellt sich die Frage, was sich bei diesen Funktionen mit GADTs ändert. 
	fold :: (a -> b -> a) -> a -> SafeList b c -> a
	fold f start (Nil) = start
	fold f start (Cons e t) = fold f (f start e) t
Die fold-Funktion ändert sich also gar nicht. Wir haben an dieser Stelle durch die Verwendung von GADTs weder Vorteile noch Nachteile.

Bei der safeMap-Funktion ist die Situation anders, auch wenn diese der bekannten map-Funktion sehr ähnlich sieht: 
	safeMap :: SafeList a c -> (a -> b) -> SafeList b c
	safeMap (Cons e t) f = Cons (f e) (safeMap t f)
	safeMap (Nil) _ = Nil
Der Unterschied liegt in dem Typparameter c. Anhanddessen steht fest, dass die Rückgabeliste die gleiche Länge hat wie die Eingabeliste. Dies ist eine Bedingung, die jede sinnvolle Implementierung offenbar erfüllen muss.

Die Typklasse Funktor, welche die map-Funktion verallgemeint, stellt genau diese Forderung; allerdings ohne sie im Typsystem festzulegen. Dort ist die Bedingung nur informell hinterlegt.



Eine weitere Funktion, bei der die Typen eine größe Aussagekraft bekommen, ist zip: 
	safeZip :: SafeList a len -> SafeList b len
	           -> SafeList (a,b) len
	safeZip Nil Nil = Nil
	safeZip (Cons e1 l1) (Cons e2 l2) =
	   Cons (e1,e2) (safeZip l1 l2)
Diese Funktion bekommt zwei Listen als Parameter, die zwar unterschiedliche Typen haben dürfen, aber die gleiche Länge len haben müssen. Der Rückgabewert ist eine Liste von Tupeln, welche wiederum die gleiche Länge hat.

Aber auch bei der Implementierung selbst gibt es einen Vorteil: Es sind nur noch zwei Funktionsgleichungen nötig. Andere Patterns als die angegeben (z.B. safeZip Nil (Cons e l)) dürfen nicht aufgeschrieben werden. Der Grund dafür ist, dass bereits durch die Typen festgelegt wurde, dass die Listen die gleiche Länge haben müssen.



Als nächstes werden verschiedene Konvertierungs-Funktionen betrachtet.

Zunächst versuchen wir, eine (möglicherweise) unsichere Liste in eine sichere Liste zu konvertieren: 
	1 makeSafe1 :: SafeList a b
	2              -> Maybe (SafeList a (Safe b))
	3 makeSafe1 Nil = Nothing
	4 makeSafe1 l   = Just l --- ???
Diese auf den ersten Blick sinnvolle Funktion lässt sich nicht kompilieren. Das Problem liegt in der zweiten Funktionsgleichung (Zeile 4). Das Pattern l hat offenbar den Typ des Parameters SafeList a b. Dieser Ausdruck wird auf der rechten Seite wiederverwendet; dort muss er allerdings den Typ SafeList a (Safe b) annehmen. Diese Typen sind jedoch nicht gleich. Dieses Problem lässt sich auch nicht durch eine Änderung der Typsignatur lösen.



Eine Alternative Definition: 
	1 makeSafe2 :: SafeList a b
	2              -> a
	3              -> SafeList a (Safe b)
	4 makeSafe2 l e = Cons e l
Hier wird versucht das Problem zu umgehen, indem immer ein Element an die Liste angehängt wird. Diese Funktion lässt sich kompilieren, bringt aber keinen Vorteil, da sie zur Konstruktorfunktion Cons bis auf die Reihenfolge der Parameter identisch ist.

Eine sinnvolle Implementierung ist offenbar nicht möglich.



Als nächstes betrachten wir eine Funktion für die umgekehrte Konvertierung. 
	1 makeUnsafe :: SafeList a (Safe b)
	2               -> SafeList a b
	3 makeUnsafe (Cons e l) = Cons e l -- ???
makeUnsafe soll eine sichere Liste als Parameter erhalten und eine unsichere Liste zurückgeben. Dies ist aus dem gleichen Grund wie bei der Funktion makeSafe1 nicht möglich: Die Typen des Parameters und des Rückgabewerts sind nicht gleich, jedoch wird in der Funktionsgleichung der gleiche Ausdruck auf der rechten und linken Seite verwendet; ein Widerspruch der in einem Compilierfehler resultiert.

Gemischte Listen

In diesem Unterabschnitt werden Listen mit unterschiedlichen Elementtypen betrachtet. 
	data MixList a b where
	  MNil  :: MixList a ()
 	  MCons :: (Show c, Show b) =>
	           a -> MixList b c -> MixList a (MixList b c)
Die Typeinschränkungen auf die Typklasse Show sind nur nötig, um im GHC-Interpretierer einfacher testen zu können; sie sind nicht wesentlich für die gemischten Listen.

Der Typparameter a steht hier für den Elementtyp des ersten Elements. Der Typparameter b steht für den Typ der Restliste.

So erklärt sich auch die Signatur der Konstruktorfunktion MCons: Ein Element a wird mit einer Liste eines (potentiell) anderen Typs b c zu einer neuen Liste zusammengebaut. Das Ergebnis ist eine Liste bei der a das erste Element darstellt. Der Rest der Liste ist wiederum eine Liste; und zwar vom gleichen Typ wie die übergebene Liste.



Der Ausdruck 
	MCons 42 (MCons "hallo" MNil)
ist also eine Liste, bei der 42 das erste Element und "hallo" das zweite Element sind. Der Typ dieser Liste ist: 
	MixList t (MixList [Char] (MixList b ()))

Abstrakte Syntaxbäume

In diesem Unterabschnitt wird der wohl wichtigste Anwendungsfall von GADTs, der Abstrakte Syntaxbaum (Abstract Syntax Tree, AST), erläutert.

Zunächst werden die Probleme bei Abstrakten Syntaxbäumen ohne Verwendung von GADTs betrachtet.

Wir beschränken uns zunächst auf einen einfachen AST mit zwei Literalen und drei zusammengesetzten Ausdrücken sowie die dazugehörige Invariante: 
	data Expr = IntLiteral Int
	          | BoolLiteral Bool
                  | AndExpr Expr Expr
	          | Equal Expr Expr
	          | Add Expr Expr

	inv :: Expr -> Bool
	inv (BoolLiteral _) = True
	inv (IntLiteral _) = True
	inv (AndExpr l r) = isInt l && isInt r
	                    ‘or‘ isBool l && isBool r
        -- ...
	-- isBool, isInt ...
Die Invariante soll ausdrücken, dass Ints und Bools nicht beliebig gemischt werden dürfen.

Problematisch ist hierbei, dass die Definition der Invariante recht mühselig ist, und zudem auch erst zur Laufzeit überprüft werden kann; voraussgesetzt der Entwickler baut entsprechende Zusicherungen an geeigneten Stellen ein.

Mit GADTs können wir diese Probleme beheben. 
	data Expr a where
	  I     :: Int -> Expr Int
	  B     :: Bool -> Expr Bool
	  And   :: Expr Bool -> Expr Bool -> Expr Bool
	  Equal :: (Show a, Eq a) =>
	           Expr a -> Expr a -> Expr Bool
	  Add   :: Expr Int -> Expr Int -> Expr Int
Die Typeinschränkung auf die Typklasse Show ist auch hier nicht wesentlich.

Bemerkenswert sind hier die Rückgabetypen der Konstruktorfunktionen. Verschiedene Konstruktoren haben hier unterschiedliche Typen: Ein Int-Literal hat beispielsweise den Typ Expr Int.

Da man boolesche Werte nicht sinnvoll addieren kann, erwartet der Add-Konstruktor als Parameter zwei Int-Expressions. Das Ergebnis einer Addition ist wieder ein Int, daher ist der Rückgabetyp von Add wiederum Expr Int.

Der Equal-Konstruktor dagegen bekommt als Parameter zwei beliebige Ausdrücke, die aber vom gleichen Typ (genannt a) sein müssen. Das Ergebnis eines Vergleichs ist ein Wahrheitswert, daher wird Expr Bool zurückgegeben.



Der große Vorteil dieser Definition ist, dass die Invariante automatisch erfüllt ist. Eine Ausdruck wie z.B. 
Equal (I 42) (B True)
wird nun vom Compiler zurückgewiesen, da Bool und Int nicht zuweisungskompatibel sind. Eine Funktion für die Invariante ist nun nicht mehr nötig, da die Invariante immer erfüllt ist. Trotzdem kann ein Baum aus Ints und Bools bestehen.



Auch Funktionen auf Ausdrucksbäumen sind nun einfacher zu definieren.

Häufig möchte man einen Ausdrucksbaum auswerten. Dies geschieht in der Funktion eval: 
	eval :: Expr a -> a
	eval (I i)       = i
	eval (B b)       = b
	eval (And l r)   = eval l && eval r
	eval (Equal l r) = eval l == eval r
	eval (Add l r)   = eval l + eval r
Diese Implementierung ist wesentlich kürzer als eine Implementierung ohne GADts, da viele unsinnige Pattern nicht aufgeschrieben werden müssen, wie z.B. ein Equal mit einem Bool und einem Int.



Eine weitere häufig benutzte Funktion auf Ausdrucksbäumen ist das Optimieren. optimize erhält einen Ausdrucksbaum und gibt einen optimierten Ausdrucksbaum zurück. 
	optimize :: Expr a -> Expr a
	optimize (And (B True) r) = optimize r
	optimize (And l r) = And (optimize l) (optimize r)
	optimize x = x
In dieser Optimierungsfunktion werden einige And-Ausdrücke optimiert. Dabei wird die bekannte Regel (Neutralitätsgesetz) True and b = b angewendet.

Diese Funktion ist natürlich sehr unvollständig. Sie soll nur verdeutlichen, dass alle wesentlichen Funktionen auf Ausdrucksbäumen implementiert werden können.

Vektoren

Anhand von Vektoren wird im Folgenden gezeigt, welche Vor- und Nach-teile GADTs in bestimmten Bereichen haben. Zudem werden weitere Konvertierungsfunktionen diskutiert.



Zunächst werden wir Vektoren analog zu Listen implementieren: 
	data Zero
	data Next a
	data Vec e n where
	  NullVec :: Vec e Zero
	  NextVec :: e -> Vec e n -> Vec e (Next n)
Die rechte Seit der Typen Zero und Next sind hier nicht relevant; daher lassen wir sie weg.

Eine wichtige Fragestellung ist die Konvertierung von Datentypen. Dort bieten sich zunächst die Listen an. 
	v2l :: Vec e n -> [e]
	v2l NullVec = []
	v2l (NextVec e l) = e : v2l l
Diese Funktion konvertiert einen Vektor in eine Liste. Hierbei gibt es keine Probleme.

Die umgekehrte Richtung ist jedoch schwieriger: 
	l2v :: [e] -> Vec e n -- ???
	l2v []    = NullVec
	l2v (e:l) = NextVec e (l2v l)
Diese Funktion lässt sich nicht kompilieren; auch nicht, wenn man die Typsignatur weglässt. Das Problem ist hier, dass die rechten Seiten der Funktionsgleichungen versuchen, zwei unterschiedliche Typen zurückzugeben: NullVec und NextVec.

Das Problem liegt hier in der Rekursion. Der Typ von l2v müsste sich bei jedem rekursiven Aufruf um ein Next erweitern. Der Typ hängt also von dem Eingabewert ab, und steht nicht zur Compilezeit fest.



Eine Funktion für das Skalarprodukt kann jedoch ohne Probleme konstruiert werden: 
	dot :: Vec Int n -> Vec Int n -> Int
	dot NullVec NullVec = 0
	dot (NextVec e1 l1) (NextVec e2 l2) = e1 * e2 + dot l1 l2
Auch hier wird wieder ausgenutzt, dass nur zwei Typgleichungen definiert werden können (genauer: dürfen).



Bei einer Funktion, welche zwei Vektoren konkateniert, haben wir jedoch wieder ein ähnliches Problem wie bei v2l: 
	concatV :: Vec e n1 -> Vec e n2 -> Vec e n3 -- ???
	concatV NullVec x = x
	concatV (NextVec e1 l1) x = NextVec e1 (concatV l1 x)
Der Typ der Rückgabeliste (hier n3), passt nicht zu den Funktionsgleichungen. Problemursache ist auch hier wieder der rekursive Aufruf.

Was wir eigentlich ausdrücken wollen, ist dass n3 = n1 + n2 gilt. Dies ist jedoch nicht möglich.



Wir betrachtet nun einen andere Vektor-Implementierung, welche das Problem der Konvertierung angeht. 
	data Wec e n where
	  Wec :: [e] -> Wec e n
Wir nenne diese Wec, um nicht mit den anderen Vektoren durcheinander zu geraten.

Bei dieser Implementierung können wir die Konvertierungsfunktionen sehr einfach definieren: 
	w2l :: Wec e n -> [e]
	w2l (Wec l) = l

	l2w :: [e] -> Wec e n
	l2w l = Wec l
Problematisch hierbei ist allerdings, dass die Invariante bzw. die Länge der Liste nicht überprüft werden kann.



Wir versuchen uns daher eine dritten Implementierung. Hierbei werden wir für jede Vektor-länge eine eigene Konstruktorfunktion definieren: 
	data WecN e n where
	  Wec1 :: e -> WecN e (Next Zero)
	  Wec2 :: e -> e -> WecN e (Next (Next Zero))
	  Wec3 :: e -> e -> e -> WecN e (Next (Next (Next Zero)))
	  -- ...
Diese Variante bringt (wie man bereits an den drei Punkten erkennen kann) Probleme mit sich. Zwar lässt sie sich ohne Probleme kompilieren, jedoch müssen wir für jede Vektor-länge einen eigenen Konstruktor definieren. Auch lassen sich einige rekursive Funktionen nicht definieren, da unser Datentyp nicht rekursiv ist.


 ... [ GADTs in Haskell ] ... [ << Von ADTs zu GADTs ] ... [ Verwandte Themen >> ] ... [ nach oben ] ...