nLab enriched monad




The notion of enriched monads is that of monads in the context of enriched category theory: For VV a base of enrichment, a VV-enriched monad is a monad internal to the 2-category VCat of VV-enriched categories.

Generally (except in the base case V=V = Set) the structure of a VV-enriched monad on a VV-enriched category C\mathbf{C} is stronger than that of the underlying monad on the underlying Set-category CC, whence one also speaks of strong monads (a priori a different notion, which however coincides with that of enriched monads under mild conditions, such as when VV is closed, see there).

The concept of enriched monads is key for the application of monads in computer science, since a monad coded verbatim in a functional programming language — where function types XYX \to Y are to be interpreted not as external hom-sets but as internal homs in the ambient closed monoidal category VV of data types — is really a VV-enriched monad (hence typicall a strong monad).




A VV-enriched monad on C\mathbf{C} is, in Kleisli triple-presentation (eg. McDermott & Uustalu 2022, Def. 5.8):

  • for every object XCX \,\in\, \mathbf{C}, an object T(X)CT(X) \,\in\,\mathbf{C};

  • for every object XCX \,\in\,\mathbf{C}, a morphism in VV of the form

    ret X:IC(X,T(X)) ret_X \;\colon\; I \to \mathbf{C}\big(X,T(X)\big)

    (the monad unit)

  • for all pairs of objects X,YX,Y of mathbfCmathbf{C}, a morphism in VV of the form

    bind X,Y:C(X,T(Y))C(T(X),T(Y)) bind_{X,Y} \;\colon\; \mathbf{C}\big(X,T(Y)\big) \to \mathbf{C}\big(T(X),T(Y)\big)

    (the Kleisli extension or bind-operation)

such that the structural equations on a Kleisli triple

  1. bind(f)ret X=fbind(f) \circ ret_X = f,

  2. bind(ret X)=idbind(ret_X\big) = id

  3. bind(g)bind(f)=bind(bind(g)f)bind(g) \circ bind(f) = bind\big(bind(g) \circ f\big)

hold for generalized elements ff, gg of the hom-objects C(X,T(Y))\mathbf{C}\big(X,\,T(Y)\big), C(Y,T(Z))\mathbf{C}\big(Y,\,T(Z)\big), which means that the following diagrams commute in VV for all objects X,Y,ZX, Y, Z of C\mathbf{C}:


Relation to strong and monoidal monads


(equivalence between VV-strength and VV-enrichment) For

then there is a bijection between the structures of

on the underlying functors,

and for any pair FF, GG of such a bijection between

It follows in particular that there is a bijection between

on such C\mathbf{C}.

(Ratkovic 2012, §3.2; McDermott & Uustalu 2022, Prop. 5.4, 5.8)


For VV a closed monoidal category the further assumptions in Prop. apply to C=DV\mathbf{C} = \mathbf{D} \coloneqq \mathbf{V} being the canonical self-enrichment of VV.


(Kock 1972, Thm. 3.2, review in GLLN08, §7.3, §A.4, Ratkovic 2012, Prop. 3.3.9)

Hence from combining Prop. with Prop. we get:


For VV a symmetric closed monoidal category with V\mathbf{V} denoting its self-enriched category, every symmetric monoidal monad on VV gives the structure of a VV-enriched monad on V\mathbf{V}.



In the case in of enrichment by truth values, a monad is a closure operator on a poset.


In the application of monads in computer science, C=V\mathbf{C} = \mathbf{V} is typically the base of enrichment itself, canonically enriched over itself. For classical computing this is typically a cartesian closed category.

Since declaring a monad in a functional programming language means to define it in the internal language of VV, such monads in computer science are actually enriched, see the discussion there.

For example, if VV is the syntactic category of a programming language, then all the definable monads in the language are VV-enriched.


See also:

Last revised on August 23, 2023 at 11:09:32. See the history of this page for a list of all contributions to it.