The Universal Algebra of Computational Effects: Lawvere Theories and Monads

Lawvere theories were defined in 1963 as a category theoretic axiomatisation of the notion of a clone of an equational theory. A connection was soon established with the notion of monad, which had been extant in algebraic topology for the previous decade. Monads, although mathematically the less direct and less malleable formulation, rapidly gained precedence. In 1987, they were proposed as a unified model of computational effects, but without reference to universal algebra. But universal algebra is central to the idea of computational effect, as it provides a theoretical foundation for the computational operations that give rise to the effect. Recognition of that fact has led to renewed prominence of the notion of Lawvere theory. We study the history of the development, in particular asking why Lawvere theories were eclipsed by monads, and how the renewed interest in them in the setting of computational effects might develop.