nLab extension system

This page is about an alternative presentation of monads as popular for monads in computer science. For a different notion of an “extension system” (that is to a bicategory what a closed category is to a monoidal category) see instead closed category.

Idea

The notion of an “extension system” (Marmolejo & Wood (2010)), originally called “algebraic theory in extension form” (Manes (1976), p. 32) and previously also referred to as a “Kleisli triple” (Moggi (1991), Def. 1.2) is an equivalent way of presenting the structure of a monad (on a category) that does not explicitly refer to composition (“iteration”) of its underlying endofunctor. This is simpler for certain purposes, and in any case more natural for others, notably in the use of monads in computer science. Abstractly, the notion may be understood as specialising the definition of $J$-relative monads to the case where $J$ is the identity functor.

Specifically, noticing that the endofunctor underlying a monad may be understood as constructing its free algebras, which (lacking relations) tend to be “large” (say as concerns the cardinality of their underlying sets), the iterated application of this endofunctor produces ever larger objects, and some authors have pointed to avoiding this phenomenon as motivation for considering extension systems:

[Marmolejo-Wood 10]: there is an important overarching reason to consider monads in this way. Extension systems allow us to completely dispense with the iterates $[$…$]$ of the underlying arrow. No iteration is necessary. A moment’s reflection on the various terms of terms and terms of terms of terms that occur in practical applications suggest that this alone justifies the alternate approach. $[$…$]$ we note that extension systems in higher dimensional category theory provide an even more important simplication of monads. For even in dimension 2, some of the tamest examples are built on pseudofunctors that are difficult to iterate.

Major alternative motivation for extension systems comes from their understanding as monads in computer science (Kleisli triples); see there for more.

Definition

An extension system (Marmolejo-Wood 2010) on a category $C$ consists of

• For every object $A\in C$, an object $T A\in C$ and a morphism $\eta_A \colon A\to T A$, and

• For every morphism $f\colon B\to T A$ in $C$, a morphism $f^T \colon T B \to T A$ (the Kleisli extension of $f$), satisfying the following axioms:

  • For every $A$ we have $(\eta_A)^T = 1_{T A}$,

  • For every $f \colon B\to T A$, we have $f^T \circ \eta_B = f$, and

  • For every $f \colon B\to T A$ and $g:C \to T B$, we have $f^T \circ g^T = (f^T \circ g)^T$.

Given these data, we make $T$ a functor by $T f = (\eta_A \circ f)^T$, we define multiplication maps $\mu_A:T T A \to T A$ as $(1_{T A})^T$, and we verify that the result is a monad. Conversely, given a monad $(T,\eta,\mu)$, we define $f^T = \mu_A \circ T f$ and check the above axioms. Thus, extension systems are equivalent to monads.

The Kleisli category

This presentation of a monad is especially convenient for defining the Kleisli category $C_T$ (whence the aternative terminology “Kleisli triple”):

its objects are those of $C$, its morphisms $B\to A$ are the morphisms $B\to T A$ in $C$, and the composite of $f:B\to T A$ with $g:C \to T B$ is $f^T \circ g$.

The category of algebras

It is also possible to define algebras over a monad using this presentation. A $T$-algebra consists of

• An object $B$, and

• For every morphism $h:X\to B$, a morphism $h^B : T X \to B$, such that

• For every $h:X\to B$ we have $h^B \circ \eta_X = h$, and

• For every $h:X\to B$ and $y:Y\to T X$ we have $h^B \circ y^T = (h^B \circ y)^B$.

As endofunctors with a particular isomorphism

The data of a monad on a category $C$ can be equivalently presented by specifying:

• An endofunctor $T : C \to C$, and

• A natural isomorphism $\phi : \Hom_C(-,T-) \cong \Hom_C(T-,T-)$. That is, for all objects $X$ and $Y$ of $C$, a bijection $\phi_{X,Y} : \Hom_C(X,TY) \cong \Hom_C(TX, TY)$ which is natural in $X$ and $Y$.

The monad structure can be obtained as follows. For each object $X$ of $C$, we have a function $\phi_{TX,X} : \Hom_C(TX,TX) \to \Hom_C(TTX, TX)$ and a function $\phi_{X,X}^{-1} : \Hom_C(TX, TX) \to \Hom_C(X,TX)$. Let $\mu_X$ and $\eta_X$ be the image of $\mathrm{Id}_{TX}$ under $\phi_{TX,X}$ and $\phi_{X,X}^{-1}$ respectively. In words, $\eta_X$ is the restriction of $\mathrm{Id}_{TX}:TX \to TX$ to $X$, and $\mu_X$ is its extension to $TTX$. The resulting natural transformations $\eta$ and $\mu$ make $(T,\eta,\mu)$ a monad.

Conversely, given a monad $(T,\eta,\mu)$, define the map $\phi$ as follows. For all objects $X$ and $Y$ of $C$, define $\phi_{X,Y} : \Hom_C(X,TY) \to \Hom_C(TX,TY)$ by setting $\phi_{X,Y}(f) = \mu_Y \circ Tf$ for all $f : X \to TY$, and define $\phi_{X,Y}^{-1}$ by setting $\phi_{X,Y}^{-1}(g) = g \circ \eta_X$ for all $g: TX \to TY$. The axioms of a monad make $\phi$ a natural isomorphism with inverse $\phi^{-1}$.

Strong monads

When $C$ is a cartesian closed category, to make $T$ a strong monad we simply have to enhance the extension operation $(-)^T$ to an internal morphism $(T A)^B \to (T A)^{T B}$, or equivalently $T B \times (T A)^B \to T A$. This morphism is known as “bind” in use of monads in computer science.

Related concepts

• monad in computer science

• relative monad

• polymonad

References

The notion appears explicitly in:

• Ernest G. Manes, Sec 3, Ex. 12 (p. 32) of: Algebraic Theories, Springer (1976) [doi:10.1007/978-1-4612-9860-1]

and is expanded on considerably in

• Francisco Marmolejo, Richard J. Wood, Monads as extension systems – no iteration is necessary TAC 24 4 (2010) 84-113 [tac:24-04]

An earlier appearance in a different guise (“devices”):

• R. F. C. Walters, Chapter I of: A categorical approach to universal algebra, Ph.D. Thesis (1970) [anu:1885/133321]

The use of extension systems (there called Kleisli triples) as monads in computer science capturing computation with side effects is due to:

• Eugenio Moggi, Notions of computation and monads, Information and Computation, 93 1 (1991) [doi:10.1016/0890-5401(91)90052-4, pdf]

This way of presenting a monad is also closely related to continuation-passing style, as described in

• Andrzej Filinski, Representing Monads, POPL 1994. (pdf)

Generalization to pseudomonads:

• Francisco Marmolejo, Richard J. Wood, Kan extensions and lax idempotent pseudomonads, TAC 26 1 (2012) 1-29 [26-01]

• Francisco Marmolejo, Richard J. Wood, No-iteration pseudomonads, TAC 28 14 (2013) 371-402 [tac:28-14]