A Theory of Effects for Programming Languages

This grant was to work on the mathematical theory of effects. This is a continuation of Moggi's very influential work on modelling effects (e.g. side-effects, or nondeterminism or exceptions) by the mathematical notion of monad. The algebraic theory gives a much more fine-grained approach in which the operations and equations giving rise to the monads are emphasised. We discuss three example papers arising from this project. Plotkin, Power, and Hyland produced a paper showing how the algebraic approach accounted for all known combinations of effects in a systematic and elegant manner. Plotkin and Keimel produced a paper on the combination of particular effects: nondeterminism and positive real-valued distributions, of key interest for the semantics of parallel processes with probabilistic features. More subtly, Power produced a monograph on three-dimensional monad theory, where the algebra is used to shift the ground on which certain classes of formal approaches stand.