nLab
extension system

Note: This page is about an alternative presentation of monads. There is a different notion of “extension system” that is to a bicategory what a closed category is to a monoidal category; for this, see closed category.

Extension systems

Idea

An extension system is a way of presenting a monad that doesn’t involve iteration of the underlying endofunctor. This is simpler for certain purposes, and the operations involved are more basic to some applications such as monads in computer science.

From (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 justies 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.

Definition

An extension system (Marmolejo-Wood 10) 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, 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: 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 above definitions are from

  • F. Marmolejo and R. J. Wood, Monads as extension systems – no iteration is necessary, TAC 2010.

but the definition of monad as extension system appeared in

  • E. G. Manes. Algebraic Theories. Springer-Verlag, 1976.

and this definition and also the definition of algebras by an extension operation appeared in

  • R.F.C. Walters, A categorical approach to universal algebra, Ph.D. Thesis, 1970.

See also

  • F. Marmolejo and R. J. Wood, Kan extensions and lax idempotent pseudomonads, TAC 2012

  • F. Marmolejo and R. J. Wood, No-iteration pseudomonads, TAC 2013

The definition of monad as an extension system was used by Eugenio Moggi (and referred to as a “Kleisli triple”) in his original paper introducing the application of monads in computer science for modeling different notions of computation:

  • Eugenio Moggi, Notions of computation and monads, Information And Computation, 93(1), 1991. (pdf)

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

Last revised on May 28, 2018 at 04:11:35. See the history of this page for a list of all contributions to it.