Abstract
So far, we've mapped logic to functional languages. However, many programs are imperative and not purely functional, as their execution has effects on the external world : they consume inputs, produce outputs, modify files, etc.
Monads are a concept derived from category theory and applied to denotational semantics by Moggi in 1989. They provide an elegant framework for describing many kinds of effects, from assignment to probabilistic programming. The monadic transformation, which generalizes the CPS transformation of the4th lecture, makes it possible to translate any program with monadic effects into a pure functional program.
Some monads have a clear logical meaning. For example, the monadic transformation of continuations is a doubly negative translation that injects classical logic into intuitionistic logic, as seen in the4th lecture ; similarly, the monadic transformation of exceptions injects intuitionistic logic into minimal logic, with no ex falso quod libet law. On monads in general, the logical content reduces to correspondences with certain modal logics, in particular Mendler's lax modality, and a combination of the classical □ and ◇ modalities observed by Pfenning and Davies.
In combination with dependent types, monads can also be used to reason about programs. The state monad can be enriched to capture invariants on the state as well as monotonic state evolution properties. More generally, Hoare monads and Dijkstra monads allow functions to be associated with any preconditions and postconditions, as in program logic. The F* language puts this monadic approach to program proof into practice.
Just as monads describe the propagation of effects, the algebraic effects theory of Plotkin, Power, Pretnar et al. seeks to describe the generation and processing of effects. It leads to a new construct for programming languages,effect handlers, which generalize exception handlers.
