Abstracts.2019.Monads

Moggi's Computational Lambda-Calculus and Monads

by Sandro Stucki

If you've ever used a functional programming language such as Haskell, chances are you have encountered Monads. In Haskell, Monads are used to model and reason about computational effects (like exceptions, side effects/global state, input–output, nondeterminism, probabilistic nondeterminism, local state, partiality, and continuations). In this talk I will explore the category-theoretical origins of Monads and present Moggi's computational lambda-calculus, which inspired their use in functional programming. If there's time I might also say a word about graded monads and connections to modal logic.

Here are links to the papers by Eugenio Moggi:

• 1988: Computational Lambda-Calculus and Monads (technical report)
• 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)

and to Andrzej Filinski's paper on monadic reflection (there are others):

• 1994: Representing Monads

Bibliography

1. Martin Hyland and John Power. 2007. "The Category Theoretic Understanding of Universal Algebra: Lawvere Theories and Monads".
2. Emily Riehl. 2017, 2019. "A Categorical View of Computational Effects". Compose Conference slides and video, Lambda World slides and video.