Mehr Typsicherheit durch GADTs
Statische Typsysteme haben zahlreiche Vorteile. Der naheliegendste Vorteil ist vermutlich, dass mögliche Laufzeitfehler verhindert werden.
Stellen wir uns zum Beispiel vor, wir wollten SQL-Anfragen modellieren. Wählen
wir einen String
als Repräsentation, so können wir ohne weiteres syntaktisch
inkorrekte Anfragen basteln, und haben keinen hohen Grad an Sicherheit. Wählen
wir statt dessen einen spezifischen Datentyp SQL
, der einen abstrakten
Syntaxbaum modelliert, so können wir uns auf syntaktische Korrektheit verlassen,
aber wir können noch immer andere Fehler machen. Was, wenn wir sicherstellen
wollten, dass die verwendeten Namen von Tabellen und Feldern tatsächlich in
unserer Datenbank enthalten sind? Was, wenn wir garantieren wollen, dass wir
SQL-Operatoren in typkorrekter Art und Weise verwenden wollen? Es ist einfach,
sich vorzustellen, dass wir dies durch Tests zur Laufzeit sicherstellen können.
Aber ist es auch möglich, dies bereits durch statische Typen zu garantieren?
Ein einfacheres Beispiel: Wir haben eine Applikation, die Fragebögen und zugehörige Antworten verwaltet. Es gibt verschiedene Sorten von Fragen. Manche Fragen sollten mit „Ja“ oder „Nein“ beantwortet werden, andere mit einer Antwort aus einer vorgegebenen Auswahl, wieder andere mit einer quantitativen Angabe. Sicher können wir Datentypen definieren, die die verschiedenen Sorten von Fragen und die verschiedenen Sorten von Antworten modellieren. Aber wenn wir nun Fragen und zugehörige Antworten haben, wie wissen wir dann, dass die Sorten der Fragen und die Sorten der Antworten zueinander passen? Wiederum ist es einfach, dies zur dynamisch zu testen. Es ist nicht ganz so einfach – aber durchaus möglich – dies auch statisch im Typsystem sicherzustellen.
Das Sprachmittel, welches wir dazu verwenden werden, heißt „GADT“. Die Abkürzung steht für „Generalized Algebraic Data Type“, zu Deutsch „generalisierter algebraischer Datentyp“. GADTs stehen in Haskell bereits seit vielen Jahren als Spracherweiterung zur Verfügung (und werden vermutlich auch irgendwann in den Standard Einzug halten), und sind mittlerweile auch in einigen anderen Programmiersprachen verfügbar.
Im folgenden will ich das Beispiel mit den Fragebögen in Haskell etwas näher beleuchten. Zunächst werden wir mit normalen Sprachmitteln skizzieren, wie man eine solche Applikation in Haskell implementieren könnte. Dann werden wir sehen, an welcher Stelle die Verwendung von GADTs sinnvoll wird, und was GADTs genau sind.
Haskell-Code
Der Code, der in diesem Artikel behandelt wird, ist in zwei separaten Dateien verfügbar. Die erste Version verwendet normale Haskell-Sprachmittel, also keine GADTs. Die zweite Version enthält dann mehr oder weniger denselben Code noch einmal, aber unter Verwendung von GADTs.
Fragen über Fragen
Stellen wir uns also vor, wir wollen ein System zur Erstellung, Verwaltung und Beantwortung von Fragebögen entwickeln. Den Kern eines solchen Systems stellt sicherlich die Repräsentation von Fragebögen und zugehörigen Antworten da.
Eine naheliegende Option in Haskell ist es, einen Fragebogen als eine Liste von Fragen zu sehen, und die Bearbeitung eines solchen Fragebogens als eine Liste von Antworten:
(Die Datentypen Question
und Answer
sind natürlich noch zu definieren.)
Wie schon in der Einleitung skizziert, wollen wir mehrere Sorten von Fragen zulassen. Um unsere Beispiele klein genug zu halten, beschränken wir uns hier auf zwei Sorten Fragen, etwa
Wer wird Fußball-Weltmeister?
Wie endet das Spiel Deutschland – Portugal?
Der erste Fragentyp fragt nach einem Land, hier spezifisch nach einem Teilnehmerland der Fußball-Weltmeisterschaft. Der zweite Typ fragt nach dem Ergebnis eines Fußballspiels.
Zur Unterscheidung dieser beiden Sorten von Fragen definieren wir den
Datentyp Question
wie folgt:
Mit data
definiert man in Haskell einen sogenannten „algebraischen Datentyp“
(der aber noch nicht „generalisiert“ ist). Dieser hat eine Reihe von „Konstruktoren“,
die unterschiedliche (und unterscheidbare) Formen von Fragen erzeugen. Diese
heißen hier CountryQuestion
und ResultQuestion
. Jeder dieser Konstruktoren
erwartet in diesem Fall ein Argument vom Typ String
und erzeugt daraus einen
Wert vom Typ Question
.
Konstruktoren verhalten sich einerseits wie Funktionen. Die beiden obigen Konstruktoren haben folgende Funktionstypen:
Unter Verwendung dieser Konstruktoren können wir jetzt unseren Beispiel-Fragebogen darstellen:
Man kann Konstruktoren aber auch als Muster („patterns“) verwenden, um Unterscheidungen durchzuführen. Zum Beispiel können wir eine Funktion definieren, die den Fragetext extrahiert und um eine vom Fragetyp abhängige Nachricht erweitert:
Wenden wir displayQuestion
auf eine Frage an, wird in Abhängigkeit vom verwendeten
Konstruktor einer der beiden Fälle ausgeführt.
Frage und Antwort
Natürlich benötigen wir Antwort-Möglichkeiten, die zu den Fragetypen passen:
Jetzt können wir zu unseren Beispiel-Fragen auch mögliche Antworten darstellen:
Früher oder später wollen wir die gegebenen Antworten vielleicht an der Wirklichkeit messen. Wir nehmen dazu an, dass unser System zu einem Fragebogen auch Musterlösungen repräsentieren kann. Da in unserem Szenario während der Weltmeisterschaft erst nach und nach die richtigen Antworten vorliegen werden, ermöglichen wir es, dass die Liste der Musterlösungen Lücken enthält:
Zum Beispiel:
Bei Maybe
handelt es sich um einen parametrisierten algebraischen Datentyp,
der in diesem Fall aus dem Datentyp Answer
von Antworten einen Datentypen von
optionalen Antworten macht.
Die Verwendung des Konstruktors Nothing
zeigt an, dass noch keine Antwort
vorliegt, die Verwendung von Just
zeigt an, dass eine Antwort vorliegt, und
bettet einen Wert vom Typ Answer
in den Typ Maybe Answer
ein.
Berechnungen auf Fragebögen
Nachdem wir die Datentypen definiert haben, können wir jetzt einige Funktionen implementieren, wie wir sie auch in einem größeren System in ähnlicher Form gebrauchen könnten. Zum Beispiel können wir die zu einem Fragebogen gehörenden Antworten (interaktiv) einlesen:
Der genaue Code ist nicht besonders wichtig. Natürlich kann man das wesentlich
robuster und besser gestalten. In der Praxis würde man die Antworten z.B.
eventuell über ein Web-Formular oder eine REST-Anfrage erhalten. Darum soll es
hier und heute aber nicht gehen. Interessant allerdings ist die Struktur der
Funktion. Wir durchlaufen durchlaufen die Liste der Fragen und führen auf
jeder Frage die Hilfsfunktion getAnswer
aus. Die Funktion getAnswer
erzeugt
letzlich genau eine Antwort pro Frage aus der Eingabe des Benutzers, und zwar
so, dass der Antworttyp zum Fragetyp passt.
Wir wissen also, dass die Liste von Antworten, die getAnswers
erzeugt, zu der
Liste der Fragen kompatibel ist. Aber das Typsystem drückt diese Kompatibilität
nicht aus. Wir fangen mit Questions
an, und bekommen Answers
zurück. Es gibt
im Typ keine weiteren Informationen über den Zusammenhang zwischen beiden.
Noch eine Funktion: Haben wir sowohl Fragen wie auch zugehörige Antworten, so können wir den Fragebogen mitsamt Antworten auch wieder ausgeben:
Wir durchlaufen beide Listen synchron. Für jede Frage und zugehörige Antwort
rufen wir displayQA
auf.
Wir können das im Interpreter testen:
GHCi> displayQAs exampleQuestions exampleAnswers
Wer wird Fußball-Weltmeister? Germany
Wie endet das Spiel Deutschland -- Portugal? 3 : 1
In der Funktion displayQAs
erwarten wir, dass Frage- und Antwort-Liste dieselbe
Länge haben. In displayQA
erwarten wir, dass Frage- und Antwort-Typ zueinander
passen. Falls nicht, so bleibt uns nichts, als die Ausführung mit error
abzubrechen.
Wir können auch das leicht nachvollziehen, indem wir displayQAs
mit inkompatiblen
Listen aufrufen:
GHCi> displayQAs exampleQuestions []
*** Exception: user error (incompatible questions and answers)
Eine ähnliche Situation ergibt sich, wenn wir Antworten und zugehörige „korrekte“ Antworten haben, und daraus die Anzahl der korrekten Antworten berechnen wollen:
Das Muster ist wiederum sehr ähnlich, und abermals müssen wir zur Laufzeit berücksichtigen, dass die übergebenen Listen evtl. unterschiedlicher Länge sein könnten, oder die Antworttypen nicht zueinander passen.
Dynamisches Testen ist suboptimal
Tatsächlich haben wir unser Program so entwickelt, dass mittels getAnswers
eingelesene Antworten garantiert kompatibel zu dem verwendeten Fragebogen sind.
Aber diese Kompatibilität kommt im Typsystem nicht zum Ausdruck.
In einem größeren Programm hätten wir eventuell mehrere Quellen, aus denen wir externe Daten wie etwa Antworten bekommen, die wir zunächst auf ihre Gültigkeit hin überprüfen sollten, bevor wir sie im Kern unseres Programms weiterverwenden. Wir würden dann vermutlich Funktionen schreiben wie etwa
die zu einem gegebenen Fragebogen ermitteln, ob die Typen der Antworten oder Beispielantworten kompatibel sind.
Aber solche dynamischen Tests von Eigenschaften sind suboptimal, weil wir als Programmierer die Verantwortung tragen, sie an den richtigen Stellen auszuführen. Vergessen wir den Test, schreiben wir ihn in fehlerhafter Weise, oder ändern wir später das Programm und die Bedingungen, so treten Laufzeitfehler auf, ohne dass der Compiler uns gewarnt hätte.
Folglich müssen wir eigentlich eine vernünftige Fehlerbehandlung für Funktionen
wie displayQAs
oder computeTotalScore
schreiben, obwohl wir lieber voraussetzen
würden, dass zu diesem Zeitpunkt die Kompatibilität der Daten bereits sichergestellt
ist.
Dies alles ist nicht wirklich zufriedenstellend. Es wäre viel schöner, wenn
beim Testen mit validateAnswers
bzw. beim Einlesen mit getAnswers
nicht nur
wir wüssten, dass bei erfolgreichem Abschluss die Kompatibilität der
Antworten mit den Fragen sichergestellt ist, sondern auch der Haskell-Compiler
bzw. das Typsystem. Konsequenterweise würde das Typsystem beim Aufruf von
displayQAs
und computeTotalScore
dann auch erwarten, dass wir kompatible
Listen übergeben, was uns beim Programmieren wiederum erlauben würde, bei der
Implementierung dieser Funktionen vorauszusetzen, dass die Eingaben den
Anforderungen genügen.
Alles noch einmal, aber mit GADTs
Die gerade beschriebene zusätzliche Präzision in den Typen ist genau das, was GADTs, also generalisierte algebraische Datentypen, uns ermöglichen.
Dazu werden wir im folgenden die Datentypen, die wir für die obige Entwicklung verwendet
haben, leicht abändern und verfeinern, so dass zum Beispiel eine leere Liste von Fragen
nicht mehr denselben Typ hat wie unser Beispielfragebogen exampleQuestions
, sondern
dass wir am Typ ablesen können
-
wie viele Fragen ein Fragebogen enthält,
-
und von welcher Art jede Frage ist.
Um dies zu erreichen, definieren wir zunächst einen neuen Datentyp
der den Typ einer einzelnen Frage (oder Antwort) beschreibt, ohne weitere Informationen zu enthalten. Es ist ein einfacher Aufzählungstyp mit genau zwei Elementen.
Jedem Fragebogen, aber auch jeder Antwortliste, wollen wir jetzt eine Liste mit Elementen
vom Typ QuestionType
zuordnen, die ihre Form präzise beschreibt. Die
Form unseres Beispielfragebogens exampleQuestions
ist etwa
da die erste Frage einen Teilnehmer sucht, und die zweite ein Spielergebnis. Dem leeren
Fragebogen wäre entsprechend die leere Liste []
zugeordnet.
Diese „Zuordnung“ ist das, wozu wir GADTs benötigen. Wir beginnen mit einzelnen Fragen
und definieren Question
neu, und zwar so, dass jeder Frage ein
(einzelner) QuestionType
zugeordnet wird:
Die Syntax der Datentypdefinition hat sich geändert. Statt Alternativen mit |
voneinander zu trennen, listen wir nun die Typsignaturen der Konstruktoren untereinander
auf. Der Typ Question
ist jetzt parametrisiert über einen Wert vom Typ QuestionType
,
und je nach Konstruktor nimmt dieser Parameter einen anderen spezifischen Wert an.
Diese Parametrisierung und Einschränkung des Parameters für verschiedene Konstruktoren
ist es, was GADTs ausmacht.
Der Teil QuestionType -> *
der ersten Zeile ist eine Art „Typsignatur“ für den Datentyp,
die explizit macht, dass der Datentyp einen Parameter vom Typ QuestionType
nimmt und
darau einen ganz normalen Datentyp formt – diese werden durch *
repräsentiert.
Wenn wir im Interpreter nachfragen, können wir jetzt am Typ ablesen, welchen Konstruktor wir verwendet haben. Bislang hatten wir:
GHCi> :t CountryQuestion "Wer wird Fußball-Weltmeister?"
CountryQuestion "Wer wird Fußball-Weltmeister?" :: Question
Jetzt bekommen wir:
GHCi> :t CountryQuestion "Wer wird Fußball-Weltmeister?"
CountryQuestion "Wer wird Fußball-Weltmeister?" :: Question 'CountryType
(Einen Apostroph wie in der Ausgabe von GHCi vor CountryType
werden wir im weiteren
Verlauf noch häufiger sehen. Diese sind im Prinzip optional, deuten aber explizit an,
dass hier der Konstruktor eines Datentyps als Parameter für einen anderen Datentyp
verwendet wird – etwas, das in der Standard-Haskell-Welt eher ungewöhnlich ist.)
Deutlich interessanter wird es, sobald wir uns Listen von Fragen zuwenden:
Wir verwenden nicht mehr die eingebauten Haskell-Listen für eine Liste von Fragen,
sondern definieren uns unseren eigenen listenähnlichen Datentyp. Eine Liste von Fragen
ist entweder leer (QNil
), und dann ist ihre Form auch die leere Liste []
. Haben
wir bereits eine Liste der Form ts
und eine einzelne Frage vom Typ t
, dann können
wir mittels QCons
die Frage vorne an den Fragebogen anfügen und erhalten insgesamt
einen Fragebogen, der die Form t : ts
hat.
Unseren Beispielfragebogen können wir nun wie folgt definieren:
Das ist weniger schön als zuvor, weil die Syntax für die eingebauten Listen
unschlagbar einfach ist. Man kann das auch hier noch etwas aufhübschen, aber darauf
will ich mich im Moment nicht konzentrieren. Wichtig ist, dass wir noch immer eine
listenartige Struktur haben, die wir durch das Anfügen zweier einzelner Fragen an
die leere Liste QNil
erzeugen. Ich habe die Typsignatur für exampleQuestions
weggelassen. Den Typ soll der Typinferenz-Algorithmus von Haskell für uns ermitteln.
Im Interpreter erfragen wir diesen wie folgt:
GHCi> :t exampleQuestions
exampleQuestions :: Questions '['CountryType, 'ResultType]
Dies zeigt, dass der Typparameter von Questions
uns nun wie gewünscht anzeigt, wie viele
und welche Art von Fragen der Fragebogen enthält.
Ein GADT für Antworten
Für Antworten können wir nun ganz entsprechend vorgehen und diese ebenfalls mit
einem Wert vom Typ QuestionType
assoziieren:
Der entscheidende Punkt ist, dass wir für unsere Beispielantworten
nun dieselbe Form erhalten wie für die Beispielfragen:
GHCi> :t exampleAnswers
exampleAnswers :: Answers '[CountryType, ResultType]
Jetzt haben wir endlich die Möglichkeit, klar und deutlich auszudrücken, was es heisst, dass wir kompatible Fragen und Antworten erwarten: sowohl Fragen als auch Antworten müssen dieselbe Form haben.
Verarbeitende Funktionen können diese Annahme jetzt explizit machen:
Die Typen von displayQAs
sowie displayQA
drücken jetzt aus, dass wir kompatible
Fragen und Antworten erwarten. Das Typsystem prüft dies. Ein Aufruf wie etwa
GHCi> displayQAs exampleQuestions ANil
erzeugt jetzt einen Typfehler zum Zeitpunkt des Übersetzens:
Couldn't match type ‘'[]’ with ‘'['CountryType, 'ResultType]’
Expected type: Answers '['CountryType, 'ResultType]
Actual type: Answers '[]
In der Implementation können wir uns als Konsequenz darauf verlassen, dass die beiden Argumente durch kompatible Konstruktoren erzeugt wurden. Wir müssen den Fehlerfall nicht mehr überprüfen – er kann zur Laufzeit nicht mehr eintreten.
In ähnlicher Weise können wir auch computeTotalScore
und computeScore
mit
präziseren Typen reimplementieren und uns die Fehlerüberprüfungen sparen:
Als letzten Schritt können wir nun auch unsere Datenquellen anpassen, so dass
etablierte Invarianten im Resultattyp sichtbar werden. Zum Beispiel lässt sich
getAnswers
so umschreiben, dass es den Typ
hat. Auch hier ist nun sichtbar, dass getAnswers
sich zwar auf einen Fragebogen
beliebiger Form ts
anwenden lässt, dass aber sichergestellt ist, dass die resultierenden
Antworten exakt dieselbe Form ts
haben.
Der Code bleibt abermals fast unverändert:
Eine Bilanz
Wie wir an unserem Frage- und Antwortbeispiel stellvertretend gesehen haben, haben wir oft mit Daten zu tun, die gewisse Zusatzanforderungen erfüllen müssen, oder die in gewisser Hinsicht zueinander kompatibel sein sollten.
Mit Hilfe von GADTs können wir solche Zusatzanforderungen präzise(r) ausdrücken, indem wir Datentypen zusätzliche Parameter geben, die von den Konstruktoren des Datentyps eingeschränkt werden. Auf diese Art und Weise können wir zum Beispiel sicherstellen, dass Frage- und Antworttypen zueinander passen.
Durch die Verwendung von GADTs sind unsere Typen etwas komplizierter geworden.
Wir mussten auch auf die Schönheit eingebauter Typen wie etwa der Standard-Listen
verzichten. Allerdings kann man die Version, die ich oben gezeigt habe, auch noch
wieder etwas verschönern, da man aus Questions
und Answers
, die sich ja recht
ähnlich sind, auch wieder auf einen einzigen, allerdings eben um Zusatzinformationen
angereicherten, listenartigen Typ reduzieren kann. Der Code hat sich allerdings
nur unwesentlich geändert, und ist sogar einfacher geworden! Die unerwünschten
Fehlerfälle können wir uns jetzt sparen, da sie unmöglich geworden sind.
Generell ist festzuhalten, dass man mit Hilfe von GADTs eine klare Typ-Unterscheidung treffen kann zwischen geprüften und ungeprüften Daten. Während eine Validierungsfunktion normalerweise einen Bool zurückliefert:
können wir mit GADTs besser einen Validator der Form
schreiben. Damit ist an jeder Stelle des Programms klar und deutlich, ob wir mit
UntrustedData
arbeiten, also auf alles gefasst sein müssen, oder mit TrustedData
und auf redundante Tests verzichten können.