Category Theory, Monads, and Computation


Master level course, 4 ECTS. UR1 / ENS Rennes 2021/22 (sif)


Syllabus

The main objective of this course is to introduce a different, yet very rich and powerful, point of view to several constructs and structures the students have already seen. After presenting the basics of category theory, we will investigate the concept of monads in both its theoretical roots and practical use in programming languages. We hope that this course serves as an invitation for master students to enrich their toolbox with open-mindedness, elegance and curiosity.

Keywords Category Theory, Monads, Semantics, Functional Programming, Computation, λ-calculus

Pre-requisite

Licence in mathematics or theoretical computer science or equivalent degree. Functional programming, semantics, programming languages’ theory, logic.

Roadmap (tentative)

All courses will take place in B02B-E110 – don’t forget your mask!

Introduction – Rethinking Set Theory

  • November 18 ETCS revisited (1/2)
  • November 19 ETCS revisited (2/2)

Part 1: Basics of Category Theory [Slides]

  • November 25 Categories
  • November 26 Functors
  • December 2 TD1
  • December 3 Natural transformations
  • December 9 Adjoints, Unit and Counit
  • December 16 Adjoints as initial objects (E209)
  • December 17 Seminar Valeria Vignudelli (ENS Lyon, France) [Webinar]

Part 2: Types as Formulas [Slides]

  • January 6 TD2 (E209)
  • January 7 Monads and Kleisli Categories (E110)
  • January 13 Cartesian Closed Categories TD4 (E110)
  • January 14 Deductive systems and λ-calculus (E208)

Exam

  • January 20 Exam (E110)

Evaluation

The final score will be composed of two marks:

  1. A written exam: January 20, 2 – 4 PM
  2. All TDs will be marked.

Seminars

  • December 17. Valeria Vignudelli (ENS de Lyon, France)

    • Title: Equational reasoning, metrics, and monads for nondeterministic and probabilistic systems

    • Abstract: Programs combining nondeterministic and probabilistic features allow us to account for both the presence of concurrency, where scheduling choices may be unpredictable, and the presence of quantitative or uncertain information. In recent contributions, we have studied methods to reason about the equivalence of systems combining nondeterminism and probability. The quantitative information brought by probabilities moreover allows us to encompass program equivalence and to reason about the finer notion of program distance. This does not only tell us whether two systems are equivalent or not, but also how much they differ. As main reasoning tool, we use equational theories and their analogues for distances, in order to obtain axiomatizations of the systems and properties of interest. By modelling nondeterminism and probabilities via monads, we are able to show our results in the abstract setting of category theory and coalgebra. In this talk I will present our framework and show applications to proving equivalences and distances, e.g. bisimulation-based, of nondeterministic and probabilistic transition systems.

Previous Exams

Bibliography

  • Books
    • William Lawvere, Stephen H. Schanuel. Conceptual Mathematics: A First Introduction to Categories. 1997, 2009
    • Tom Leinster. Basic Category Theory. 2016 pdf
    • Joachim Lambek, Philip J. Scott. Introduction to Higher-Order Categorical Logic. 1986
    • Saunders Mac Lane, Categories for the Working Mathematician. 1972
  • Papers
    • Tom Leinster. Rethinking Set Theory. 2014 pdf
    • William Lawvere, An elementary theory of the category of sets. 1964 pdf
    • Philip Wadler. Propositions as Types. pdf

Office Hours

  • Thursdays, 2–4 PM (Inria)
  • For any request/question, feel free to email me (see address below)