Programming Languages

Kategorientheorie für Programmierer

Objektorientierte Programmierung nutzt Design-Patterns für die Konzeption von Programmen. Funktionale Programmierer können stattdessen auf die Begriffswelt der Kategorientheorie, einer mathematischen Disziplin, zurückgreifen um ihre Programme auf abstrakter Ebene zu entwerfen. In diesem Seminar sollen grundlegende Konzepte der Kategorientheorie anhand von Beispielen in Haskell erarbeitet werden.

Dozenten

David Binder
ResearcherDavid Binder (Office: Room B211)
Ingo Skupin
AlumniIngo Skupin (Office: Room B211)
Prof. Klaus Ostermann
HeadKlaus Ostermann

Vorbesprechung

Die Vorbesprechung fand am Montag, 16. April um 18:00 im Pausenraum B226 statt. Die Folien der Vorbesprechung stehen hier zum Download bereit.

Wir haben eine Einladung zu einer Doodle Umfrage an alle Teilnehmer der Vorbesprechung geschickt. Sobald wir die Umfrage ausgewertet haben wird der endgültige Termin und Raum bekannt gegeben werden. Die Umfrage ist beendet und ein Termin wurde festgelegt.

Struktur der Veranstaltung

Wir werden gemeinsam das Buch von Bartosz Milewski “Category Theory for Programmers” lesen, welches hier kostenlos in pdf-Form verfügbar ist. Eine kostengünstige gedruckte Ausgabe des Buches kann man von dem Print-On-Demand Dienstleister Lulu.com beziehen. Zusätzlich werden wir evtl. noch weitere wissenschaftliche Artikel zum Thema lesen.

Die Teilnehmer lesen jede Woche das Kapitel des Buches das beim kommenden Treffen besprochen wird (jeweils von der Länge eines längeren Blogposts). Die Rolle des Diskussionsleiters rotiert wöchentlich unter den Teilnehmern. Die Aufgabe des Diskussionsleiters ist es sich intensiver auf das Thema vorzubereiten um die Diskussion zu moderieren. Ausserdem gibt es wöchentliche Übungsblätter von geringem Umfang, deren Bearbeitung notwendig ist, um die besprochenene Konzepte zu verinnerlichen.

Termine

Das Seminar findet immer donnerstags, um 12:15 im Raum A104 auf dem Sand statt.

Donnerstag, 26. April

Wir werden Kapitel 3 + 5 aus dem Buch besprechen.

Donnerstag, 3. Mai

Wir werden Kapitel 6 + 7 aus dem Buch besprechen.

Entpacken Sie das Stack Projekt in einen Ordner ihrer Wahl. Danach können Sie in diesem Ordner mit den Befehlen

stack build
stack exec Isomorphisms

die Tests für den schon implementierten Isomorphismus durchlaufen lassen. Falls ein Fehler

AesonException "Error in $.packages.cassava.constraints.flags['bytestring--lt-0_10_4']: Invalid flag name: \"bytestring--lt-0_10_4\""

auftaucht müsst ihr zuvor stack auf die neueste Version aktualisieren. (Mit stack upgrade). Der gesamte Code befindet sich in Main.hs.

Donnerstag, 17. Mai

Wir werden Kapitel 8 + 9 aus dem Buch besprechen.

Donnerstag, 7. Juni

Wir werden Kapitel 10, 12 und 13 aus dem Buch besprechen.

Donnerstag, 14. Juni

Wir werden Kapitel 18 aus dem Buch besprechen.

Donnerstag, 21. Juni

Wir werden Kapitel 20 und 21 aus dem Buch besprechen.

Donnerstag, 28. Juni

Wir werden Kapitel 22 aus dem Buch besprechen.

Donnerstag, 5. Juli

Wir werden Kapitel 24 (ohne 24.6) aus dem Buch besprechen.

Donnerstag, 12. Juli

Wir werden die Abschnitte 1 bis 4 (inklusive) des Artikels “Reason Isomorphically!” von Ralf Hinze und Daniel W. H. James lesen.

Donnerstag, 19. Juli

Wir werden die Abschnitte 5 bis zum Ende des Artikels “Reason Isomorphically!” von Ralf Hinze und Daniel W. H. James lesen.

Final Projects

Die Vorstellung der Projekte findet an den folgenden beiden Terminen statt:

  • Donnerstag, 2. August ab 13:00 im Raum A302.
  • Donnerstag, 16. August ab 13:00 im Raum A301.

ETCS - Elementary Theory of the Category of Sets

  • ETCS im nLab: nLab
  • Tom Leinster, Rethinking Set Theory: arxiv.org

String Diagramme für Kategorien von Funktoren und natürlichen Transformationen

  • Seite 55/56 im Buch “Basic Category Theory”: arxiv.org
  • TheCatsters Videos String diagrams 1-5: youtube.com

String Diagramme für monoidale Kategorien

  • Peter Selinger, A survey of graphical languages for monoidal categories, sec. 2 to 3.2: arxiv.org

Yoneda / Co-Yoneda

  • Kapitel 14-16 im Buch
  • Das Diagramm in der subsection “Proof” der Wikipedia Seite: Wikipedia
  • Das obige Diagramm wird ab min ~10 von Bartosz Milewski konstruiert: Youtube

Programmieren mit Applicatives

  • Conor McBride, Ross Paterson, Applicative programming with effects: staff.city.ac.uk

Continuation Passing Style

  • Eintrag im nLab: nLab
  • Blogpost von Mike Stay: Link

Presheaves

  • z.B. Robert Goldblatt, Topoi, the categorical analysis of logic, sec. 4.5 Amazon

Fixpunkte in kartesisch geschlossenen Kategorien

  • Eintrag im nLab: nLab
  • Noson Yanofsky, A universal approach to self-referential paradoxes, incompleteness and fixed points arxiv.org
  • Bill Lawvere, Diagonal arguments and cartesian closed categories. tac.mta.ca