Abstracts.2020.Monads

Notions of Computation and Monads

by Carlos Tomé Cortiñas

Abstract

Monads are pervasive nowadays in programming languages. Pure functional languages, such as Haskell, go even further and use monads like IO as the centerpiece to structure programs that produce side-effects (e.g. printing to the screen). The concept of monad was developed in the framework of Category Theory during the 50s and 60s but it wasn't until much later, in the 90's, that found its way into Computer Science thanks to Eugenio Moggi. Indeed his very celebrated insight was that monads serve as a unifying concept to give semantics to effectful computations. In this talk, I will try to explain and motivate Moggi's idea. To that matter, and following his lead, I will look at (a fragment of) the computational lambda-calculus λ_c [Führmann, Appendix A], an impure programming language, and discuss how monads can be used to construct models.

References to Moggi's papers:

• 1991: Notions of Computation and Monads (main reference)
• 1989: Computational Lambda-Calculus and Monads (paper, does not include the sections 2.2 Embedding of a computational model in a topos, 5 Untyped λ_c-models, and 6 Reduction)
• 1988: Computational Lambda-Calculus and Monads (technical report)

References to work by others:

• 1994: Representing Monads Andrzej Filinski
• 1990: Direct Models for the Computational Lambda-Calculus Carsten Führmann

Computational effects and algebra:

• 2018: What is algebraic about algebraic effects and handlers? Andrej Bauer

Monads and Kleisli triples:

• 1976: Algebraic Theories Ernest Manes
• 1978: Categories for the Working Mathematician Saunders Mac Lane

Related talks:

• 2019: Moggi's Computational Lambda-Calculus and Monads Sandro Stucki

Examples

• the Kleisli category of the maybe monad X↦X+1 is (isomorphic to) the category of sets and partial functions
• the Kleisli category of the powerset monad X↦℘(X) is (isomorphic to) the category of sets and relations