Im letzten Artikel der Denotational-Design-Reihe hatten wir die
Programmiersprache bzw. den Theorembeweiser
Agda
kennen gelernt. In diesem kleinen Einschub stelle ich einige
Ressourcen vor, mithilfe derer man seine Agda- und
Dependent-Typing-Skills vertiefen kann. Ich stelle die Ressourcen in
einer Reihenfolge vor, von der ich denke, dass sich diese für mich gut
zum Lernen geeignet hätte.
The Little Typer ist ein Buch aus der
„Little“-Reihe von Dan Friedman. Zweitautor ist David Thrane
Christiansen, der mittlerweile an Lean –
einer jüngeren Sprache mit Dependent Types – arbeitet. Es ist schon
einige Zeit her, dass ich das Buch gelesen hatte. Ich kann mich
deshalb nur noch an das Gefühl erinnern, das ich beim Lesen hatte und
das war sehr gut. Das Buch arbeitet mit der eigens entwickelten Sprache
Pie. Wie es sich für
eine Sprache in der Racket-Tradition gehört, ist diese ausdrücklich so
gestaltet, dass sie sich zum Lernen der Konzepte bestens eignet. Im
Appendix „The Way Forward“ wird beschrieben, wie man von Pie aus
weiter Richtung production-ready Dependent Types fortschreitet.
Mein Tipp: Wer ein erstes Gefühl für Dependent Types entwickeln
möchte, ist hier richtig. Ungeduldige, die beispielsweise schon Erfahrung mit
einigen Dependent-Haskell-Features
haben, können aber auch direkt zum nächsten Buch springen.
Die beste Anlaufstelle, um die Theorie hinter Dependent Types zu
verstehen, ist das sogenannte HoTT
Book. Man darf sich dabei nicht
vom Titel des Buchs abschrecken lassen: Um Homotopie geht‘s erst im
zweiten Kapitel. Die lange „Introduction“ kann man überspringen. Das
erste richtige Kapitel „Type theory“ behandelt dann Dependent Types
auf knapp 40 Seiten. Das reicht aus, um von dort weiter Richtung Agda
zu schreiten.
Mein Tipp: Lohnt sich auf jeden Fall und sollte man zwischendurch
immer mal wieder heranziehen.
Die offizielle Website und das Handbuch
Die offizielle Website von Agda ist das
Wiki. Das User
Manual ist ganz ok zum
Nachschlagen. Wenn man aber noch nicht weiß, was da steht, dann wird
man‘s auch nicht durch Lesen erfahren. Am Anfang lohnt es sich
deshalb, die Liste von
Tutorials
zu konsultieren.
Das in die Jahre gekommene Tutorial von 2008 bietet einen okayen
Überblick über die Features der Sprache. Viele der Beispiele
funktionieren allerdings mittlerweile anders. Vor allem der Foreign-Function-Interface-Teil
„Compiling Agda programs“ ist veraltet.
Mein Tipp: Einmal überfliegen und dann weiter.
Denotational-Design-Guru Conal Elliott empfiehlt den ersten Teil
dieses Buchs von Wadler, Kokke und Siek als
Einführung in Agda und da kann ich nicht widersprechen. Man muss sich
vor der Lektüre allerdings bereits davon überzeugt haben, dass es
sinnvoll ist, semantische Sachverhalte in einem Typsystem auszudrücken
und automatisiert zu prüfen. Die Intuition adressiert das Buch kaum.
Mein Tipp: Zusammen mit dem nächsten Buch einmal durch Teil 1 arbeiten.
Die Bücher von Sandy Maguire sind
stets empfehlenswert. Certainty by Construction ist keine reine
Einführung in Agda, verwendet Agda aber als Vehikel für die
Beschreibung von allerlei Schmankerl aus dem Grenzgebiet der
Programmierkunst. Anders als „Programming Language Foundations in
Agda“ erlaubt sich das Buch ab und zu Aussagen, die eher auf die
Bildung einer Intuition abzielen. So klingt beispielsweise die
Einführung in das Thema „Decidability“ in PLFA sehr trocken:
We have a choice as to how to represent relations: as an inductive
data type of evidence that the relation holds, or as a function that
computes whether the relation holds. Here we explore the relation
between these choices.
Bei Sandy Maguire klingt die Einführung in das Kapitel „Decidability“ anders:
Perhaps now we can smugly think that we know all there is to know
about proofs—but this is patently false. For example, we haven’t the
notion of falseness itself! Furthermore, everything we’ve built so
far works only for statically-known values. But is it possible that
we can use dependent types in contexts where we don’t know all the
values we need to work with? Maybe the values came from the user via
an interactive system. Are we forced to throw away everything
we’ve done and degrade our guarantees to those of a weaker
programming language? Thankfully the answer to all of these is „no,“
and we will explore each in this chapter.
Mein Tipp: Eignet sich gut als Begleitung zu PLFA. Die Kapitel bauen
aufeinander auf, aber ich habe das Buch auszugsweise gelesen und das
hat auch hervorragend funktioniert.
Für Haskell-Experten bietet dieser knapp zweieinhalbstündige
Workshop-Mitschnitt eine gute Einführung in Agda. Jesper Cockx ist
einer der Maintainer des Agda-Projekts, hat also Ahnung von den
Interna.
Das Paper von Altenkirch, McBride und McKinna beschreibt die Vorzüge
von Dependent Types anhand von Epigram – einer der Einflüsse von
Agda. Dabei werden einige Merkmale dieser Arten von
Programmiersprachen anders gedreht und gewendet als in den oben
genannten Büchern. Folgenden Absatz fand ich beispielsweise sehr
erhellend (allerdings erst nachdem ich mithilfe von PLFA und Certainty
by Construction ein erstes Verständnis entwickelt hatte):
Type systems without dependency on dynamic data tend to satisfy the
replacement property—any subexpression of a well typed expression
can be replaced by an alternative subexpression of the same type in
the same scope, and the whole will remain well typed. For example,
in Java or Haskell, you can always swap the then and else branches
of conditionals and nothing will go wrong—nothing of any static
significance, anyway. The simplifying assumption is that within any
given type, one value is as good as another. These type systems have
no means to express the way that different data mean different
things, and should be treated accordingly in different ways. That is
why dependent types matter.