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

*Thanks, all, for having come and participated!*

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).

- Lectures 1-2: Intro to monads as notions of computation
- Lectures 3-4: Comonads and monad-comonad interaction laws or how computations can run

Slides and exercise material:

- Lecture 1
- Exercise session 1, Mnd.hs (Monad.hs)
- Lecture 2
- Exercise session 2
- Lecture 2bis (not given)
- Lecture 3
- Exercise session 3, Comnd.hs
- Lecture 4
- Exercise session 4, Interact.hs

*(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.)*

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:

- E. Moggi. Computational lambda-calculus and monads. LICS '89. [doi link]
- G. Plotkin, J. Power. Notions of computation determine monads. FoSSaCS '02. [doi link (open access)]
- G. Plotkin, M. Pretnar. Handlers of algebraic effects. ESOP '09. [doi link (open access)]

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

- S. Katsumata, E. Rivas, T. Uustalu. Interaction laws of monads and comonads. LICS '20. [pdf]
- T. Uustalu, N. Voorneveld. Algebraic and coalgebraic perspectives on interaction laws. APLAS '20. [pdf]

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 UustaluLast update 16 April 2021