Programming Languages and Software Technology

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
Researcher
David Binder
(Office: Room B211)
Ingo Skupin
Researcher
Ingo Skupin
(Office: Room B211)
Prof. Klaus Ostermann
Head
Klaus 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. Diskussionsleiter sind Ingo und David.

Donnerstag, 3. Mai

Wir werden Kapitel 6 + 7 aus dem Buch besprechen. Diskussionsleiter ist Jonas Lingg.

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. Diskussionsleiter ist Daniel Täsch.

Donnerstag, 7. Juni

Wir werden Kapitel 10, 12 und 13 aus dem Buch besprechen. Diskussionsleiter ist Arne Runge.

Donnerstag, 14. Juni

Wir werden Kapitel 18 aus dem Buch besprechen. Diskussionsleiter sind Arne Großelindemann und Patrick Weigert.

Donnerstag, 21. Juni

Wir werden Kapitel 20 und 21 aus dem Buch besprechen. Diskussionsleiterin ist Felicia Saar.

Donnerstag, 28. Juni

Wir werden Kapitel 22 aus dem Buch besprechen. Diskussionsleiter ist Florian Engel.

Donnerstag, 5. Juli

Wir werden Kapitel 24 (ohne 24.6) aus dem Buch besprechen. Diskussionsleiter ist Gabriel Paradzik.

Donnerstag, 12. Juli

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

Donnerstag, 19. Juli

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

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