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.

Buch: The Little Typer

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.

Buch: Homotopy Type Theory: Univalent Foundations of Mathematics

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.

Tutorial: Dependently Typed Programming in Agda

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.

Buch: Programming Language Foundations in Agda (kostenlos online)

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.

Buch: Certainty by Construction

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.

Video: Agda Track by Jesper Cockx @ ZuriHac 2024

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.

Paper: Why Dependent Types Matter

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.