Monads and interaction

This the page for my course at MGS 2021, Mon-Fri 12-16 April 2021.

Thanks, all, for having come and participated!

Abstract

It is standard in the semantics of programming languages to use monads to model notions of computation that involve effects such as computation with input/output, manipulation of store, nondeterminism. Unlike a purely functional computation, an effectful computation cannot return a value on its own: it issues requests to the outside world and needs these responded to make progress. To run, it thus needs to be paired with an environment that is coeffectful, can service these requests. The two need to understand each other and work together. My message in this course is that environments and interaction are important characters in the act of computations. Notions of coeffectful environment are naturally modelled with comonads. Protocols of communication between computations and environments then admit mathematization by what we have christened interaction laws.

I will give a brief general introduction to monads, comonads and their applications in semantics, but will then focus on interaction specifically. My material involves a fair amount of quite abstract constructions, but all come illustrated with concrete examples and almost all mean something for programming.

I will need to assume basic knowledge of functional programming and some category theory (categories/functors/natural transformations, Cartesian closed categories).

Course plan

Course material

Slides and exercise material:

(All of the above files updated 16 Apr, typos detected fixed. If you find more, please do let me know, I'll be very grateful.)

Background material

I will use various classical and less classical sources for lectures 1-2.

The most seminal papers on monads / algebraic theories as notions of computation are these:

The main sources for lecture 4 on interaction laws are these two recent papers of mine with coauthors:

Functional programmers discovered interaction laws before us, calling them zappings and pairings, but did not work out all of the mathematics. See the blogs of Edward Kmett (post 1, post 2, post 3) and Dan Piponi (post) and especially Phil Freeman (post 1, post 2, post 3, post 4, post 5, post 6, post 7). Arthur Xavier wrote a UFMG Bsc thesis on this topic (part 1, part 2).

For an intro to category theory for programmers I recommend Bartosz Milewski's book.

Tarmo Uustalu
Last update 16 April 2021