nLab extension system

Redirected from "monad in extension form".
Extension systems

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

Extension systems

Idea

The notion of “extension system” (Marmolejo & Wood (2010)), originally called “algebraic theory in extension form” (Manes (1976), p. 32) and previously also referred to as “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 JJ-relative monads to the case where JJ 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 CC consists of

  • For every object ACA\in C, an object TACT A\in C and a morphism η A:ATA\eta_A \colon A\to T A, and

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

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

    • For every f:BTAf \colon B\to T A, we have f Tη B=ff^T \circ \eta_B = f, and

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

Given these data, we make TT a functor by Tf=(η Af) TT f = (\eta_A \circ f)^T, we define multiplication maps μ A:TTATA\mu_A:T T A \to T A as (1 TA) T(1_{T A})^T, and we verify that the result is a monad. Conversely, given a monad (T,η,μ)(T,\eta,\mu), we define f T=μ ATff^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 TC_T (whence the aternative terminology “Kleisli triple”):

its objects are those of CC, its morphisms BAB\to A are the morphisms BTAB\to T A in CC, and the composite of f:BTAf:B\to T A with g:CTBg:C \to T B is f Tgf^T \circ g.

The category of algebras

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

  • An object BB, and

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

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

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

Strong monads

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

References

The notion appears explicitly in:

and is expanded on considerably in

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

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

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

Generalization to pseudomonads:

Last revised on April 6, 2024 at 10:19:34. See the history of this page for a list of all contributions to it.