Semantics Club 16 11 2001

Computational effects and enriched Lawvere theories

John Power


In the late 1980's, Eugenio Moggi proposed using monads to give a unified way to model computational effects such as state, exceptions, nondeterminism and input/output. Here, we propose a different but, in a precise sense, almost equivalent approach, using the concept of Lawvere theory, suitably enriched. This keeps the mathematics closer to the computational phenomena, supports a theory of modularity that has hitherto been missing, and fits naturally with well structured general development of structural operational semantics for at least some such effects. Parts of the technical content of this work have been done jointly with Martin Hyland, Gordon Plotkin, and others.