Segal condition meets computational effects

摘要

Every finitary monad T on the category of sets is described by an algebraic theory whose n-ary operations are the elements of the free algebra Tn generated by n letters. This canonical presentation of the monad (called its Lawvere theory) offers a precious guideline in the search for an intuitive presentation of the monad by generators and relations. Hence, much work has been devoted to extend this correspondence between monads and theories to situations of semantic interest, like enriched categories and countable monads. In this paper, we clarify the conceptual nature of these extended Lawvere theories by investigating the change-of-base mechanisms which underlie them. Our starting point is the Segal condition recently established by Weber for a general notion of monad with arities. Our first step is to establish the Segal condition a second time, by reducing it to the Linton condition which characterizes the algebras of a monad as particular presheaves over the category of free algebras. This reduction is achieved by a relevant change-of-base from the category of interest to its subcategory of arities. This conceptual approach leads us to an abstract notion of Lawvere theory with arities, which extends to every class of arity the traditional correspondence in Set between Lawvere theories and finitary monads. Finally, we illustrate the benefits of Lawvere's ideas by describing how the concrete presentation of the state monad recently formulated by Plotkin and Power is ultimately validated by a rewriting property on sequences of updates and lookups.