Category Theory, Monads, and Computation

Master level course, 4 ECTS. UR1 / ENS Rennes 2023/24 (sif)

Syllabus

The main objective of this course is to introduce a unifying, yet expressive and powerful, point of view to several constructs and structures, many of which 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. open-mindedness and curiosity.

Roadmap (tentative)

All courses will take place in B02B-E208. Two classes per week: Tuesday and Wednesday.

Introduction – Rethinking Set Theory

  • November 14 ETCS revisited (1/2) (8–9:30am)
  • November 21 ETCS revisited (2/2) (3–4:30pm)

Part 1: Basics of Category Theory [Slides]

  • November 22 Categories and Functors (3–4:30pm)
  • November 28 Natural transformations (8–9:30am)
  • November 29 TD1 (3–4:30pm)
  • December 5 Adjoints (3–4:30pm)
  • December 6 Monads and Kleisli Categories (3–4:30pm)
  • December 12 Cartesian Closed Categories (8–9:30am)
  • December 13 TD23 (3–4:30pm)

Part 2: Types as Formulas [Slides]

  • December 19 Deductive systems (3–4:30pm)
  • December 20 Monads in programming languages (3–4:30pm)
  • January 9 λ-calculus (8–9:30am)

Exam

  • January 16 Exam (3–5pm) E208
  • January 17 Seminar. TBA (3–4:30pm)

Evaluation

The final score will be composed of two marks:

  1. A written exam: January 16, 3:00 – 4:30 AM
  2. All TDs will be marked.

Seminars

  • Samuel Mimram (Ecole Polytechnique, France)

    • Title: A type-theoretical definition of weak ω-categories [Slides]

    • Abstract: Higher-dimensional categories generalize the traditional notion of category by taking in account higher-dimensional cells. In the most general setting, we want their operations to be weak, in the sense that their coherence laws should hold up to higher dimensional cells, which should themselves be coherent. In this talk, I will present a type theory which describe those structures: it allows deriving precisely all the operations and coherence which are expected to be found in those. This work is based on a categorical definition due to Malstiniotis. Our main contribution is to provide a canonical type-theoretical characterization of pasting schemes as contexts which can be derived from inference rules. An implementation of a corresponding proof system will also be presented. This is joint work with Eric Finster and Thibaut Benjamin.

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)