# nLab monad (in computer science)

Contents

### Context

#### Computation

intuitionistic mathematics

### Computability

#### Categorical algebra

internalization and categorical algebra

universal algebra

categorical semantics

# Contents

## Idea

In computer science, a (co-)monad (or (co-)Kleisli triple, or (co-)extension system) is a kind of data type-structure which describes “notions of computations” [Moggi (1991)] that may “have external effects or be subject to external contexts/causes” — such as involving random access memory, input/output, exception handling, writing to or reading from global variables, etc. — as familiar from imperative programming but cast as “pure functions” with deterministic and verifiable behaviour, in the style of functional programming.

In short, a (“extension system-style” [Manes (1976), Ex. 3.12] or “Kleisli triple-style” [Moggi (1991), Def. 1.2]) monad in a given programming language consists of assignments (but see below):

1. to any data type $D$ of a new data type $\mathcal{E}(D)$ of “$D$-data with $\mathcal{E}$-effects”,

2. to any pair of $\mathcal{E}$-effectful functions (programs) of the form $prog_{12} \,\colon\, D_1 \to \mathcal{E}(D_2)$ and $prog_{23} \,\colon\, D_2 \to \mathcal{E}(D_3)$ of an effective-composite function $bind^{\mathcal{E}} prog_{23} \;\circ\; prog_{12}(-) \,\colon\, D_1 \to \mathcal{E}(D_3)$ (their binding or Kleisli composition),

3. to any data type $D$ of a function $ret^{\mathcal{E}}_D \;\colon\; D \to \mathcal{E}(D)$ assigning “trivial $\mathcal{E}$-effects”,

such that the binding is associative and also unital with respect to the return operation, hence such that data types with $\mathcal{E}$-effectful programs between them constitute a category (the Kleisli category of the given effect/monad $\mathcal{E}$).

We now explain in more detail what this means and what it is good for.

In programming it frequently happens that a program with “nominal” output data type $D$ de facto outputs data of some modified type $T(D)$ which accounts for “external effects” caused by the program, where

(1)$D \;\mapsto\; \mathcal{E}(D)$

is some general operation sending data types $D$ to new data types $\mathcal{E}(D)$.

For example, if alongside the computation of its nominal output data $d \colon D$ a program also writes a log message $msg \,\colon\,$ String, then its actual output data is the pair $(d, msg)$ of product type $Write(D) \,\coloneqq\, D \times String$.

Or, dually, if the program may fail and instead “throw an exception message” $msg \,\colon\,$ String, then its actual output data is either $d \colon D$ or $msg \colon String$, hence is of coproduct type $Excep(D) \,\coloneqq\, D \sqcup String$.

Given such an $\mathcal{E}$-effectful program $prog_{12} \;\colon\; D_1 \to \mathcal{E}(D_2)$ and given a subsequent program $prog_{23} \,\colon\, D_2 \to \mathcal{E}(D_3)$ accepting nominal input data of type $D_2$ and itself possibly involved in further effects of type $\mathcal{E}(-)$, then the naïve composition of the two programs makes no sense (unless $\mathcal{E}(D) = D$ is actually the trivial sort of effect), but their evident intended composition is, clearly, obtained by:

1. first adjusting $prog_{23}$ via a given prescription

(2)$\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\! prog \;\mapsto\; bind^{\mathcal{E}} prog \,,$

such that $bind^{\mathcal{E}} prog_{23} \,\colon\, \mathcal{E}(D_2) \to \mathcal{E}(D_3)$:

1. does accept data of type $\mathcal{E}(D_2)$ and

2. “acts as $prog_{23}$ while carrying any previous $\mathcal{E}$-effects along” (this intuition becomes a formal fact below in (9));

2. then forming the naive composition $bind^{\mathcal{E}} prog_{23} \;\circ\; prog_{12}$

as follows:

(Beware that we are denoting by “$bind^{\mathcal{E}} prog (-)$” what in programming languages like Haskell is denoted by(-) >>= prog” aka “fish notation”, eg. Milewski (2019), and which some authors denote by “$prog^\ast\,$”, e.g. Moggi (1991); Uustalu (2021), lecture 1, p. 12.)

Depending on the intended behaviour of these programs, it remains to specify how exactly $bind^{\mathcal{E}} prog_{23}$ “carries $\mathcal{E}(-)$-effects along”, hence what the “bind” operation (2) does concretely.

For instance, in the above example of a logging-effect, where $Write(D_2) \,\coloneqq\, D_2 \times String$, the evident way is to use the concatenation $String \times String \xrightarrow{\; concat \;} String$ and set:

$bind^{Write} prog_{23}\;\coloneqq\; D_2 \times String \xrightarrow{ prog_{23} \times Id_{String} } D_3 \times String \times String \xrightarrow{ Id_{D_3} \times concat } D_3 \times String \,.$

In the other example above, where the effect is the possible throwing of an exception message, the evident way to carry this kind of effect along is to use the codiagonal $\nabla \,\colon\, String \sqcup String \to String$, which amounts to keep forwarding the exception that has already been thrown, if any:

$bind^{Excep} prog_{23} \;\coloneqq\; D_2 \sqcup String \xrightarrow{ prog_{23} \sqcup Id_{String} } D_3 \sqcup String \sqcup String \xrightarrow{ id_{D_3} \sqcup \nabla } D_3 \sqcup String \,.$

Whatever design choice one makes for how to “carry along effects”, it must be consistent in that applying the method to a triple of $\mathcal{E}$-effectful programs which are nominally composable, then their effectful composition should be unambiguously defined in that it is associative, satisfying the following equation – here called the the first “monad law”:

(3)$bind^{\mathcal{E}} prog_{34} \;\circ\; \Big( bind^{\mathcal{E}} prog_{23} \;\circ\; prog_{12} \Big) \;\;\;=\;\;\; bind^{\mathcal{E}} \Big( bind^{\mathcal{E}} prog_{34} \;\circ\; prog_{23} \Big) \;\circ\; prog_{12} \,.$

Finally, for such a notion of effectful programs to be usefully connected to “pure” programs without effects, it ought to be the case that for any program $prog_{01} \,\colon\, D_0 \xrightarrow{\;} D_1$ that happens to have no $\mathcal{E}$-effects, we have a prescription for how to regard it as an $\mathcal{E}$-effectful program in a trivial way. For that purpose there should be defined an operation

(4)$ret_{D} \;\colon\; D \xrightarrow{\;} \mathcal{E}(D)$

which does nothing but “return” data of type $D$, but re-regarded as effectful $\mathcal{E}(D)$-data in a trivial way; so that we may construct the trivially effectful program $ret^{\mathcal{D}}_{D_1} prog_{01} \;\colon\; D_0 \xrightarrow{\;} \mathcal{E}(D_1)$.

For instance, in the above example of log-message effects this would be the operation $D \to D \times String$ which assigns the empty string $ret^{Write} \;\colon\; d \mapsto (d, \varnothing)$.

In the other example above, of exception handling, the trivial effect $D \to D \sqcup String$ is just not to throw an exception, which is just $ret^{Excep} \;\colon\; d \mapsto d$ (the right coprojection into the coproduct).

The final consistency condition (i.e. the remaining “monad law”) then is that “carrying along trivial effects is indeed the trivial operation”, i.e. that

(5)$bind^{\mathcal{E}} prog_{01} \;\circ\; ret_{D_0}(-) \;=\; prog_{01} \;\;\;\;\;\;\;\;\; \text{and} \;\;\;\;\;\;\;\;\; bind^{\mathcal{E}} ret_{D_1} \;\circ\; prog_{01}(-) \;=\; prog_{01} \,.$

Notice that the associativity condition (3) and the unitality condition (5) are jointly equivalent to saying that data types with hom-sets of $\mathcal{E}$-effectful programs between them, in the above sense, form a category. In category theory this is known as the Kleisli category $Kl(\mathcal{E})$ of a monad $\mathcal{E}$ on the category $Type$ of data types with programs between them:

(6)$\begin{array}{rcl} Obj\Big( Kl(\mathcal{E}) \Big) &\;\;=\;\;& Obj\Big( Type \Big) \\ Hom\Big( Kl(\mathcal{E}) \Big)\big(D_1,\, D_2\big) &\;\;=\;\;& Hom\Big( Type \Big) \big( D_1, \, \mathcal{E}(D_2) \big) \\ (-) \circ_{\mathrm{Kl}(\mathcal{E})} (-) &\;\;=\;\;& (-) \circ_{Type} bind^{\mathcal{E}}(-) \,. \end{array}$

Traditionally in category theory, the axioms on monads are presented in a somewhat different way, invoking a monad “product” natural transformation $\mathcal{E} \circ \mathcal{E} \xrightarrow{ \mu } \mathcal{E}$ instead of the “binding” operation. One readily checks that these two axiomatic presentations of monads are in fact equal – see (7) below –, but the above “Kleisli triple/extension system”-presentation is typically more relevant in the practice of functional programming.

In summary, a choice of assignments (but see below) to data types $D_i$ of

1. $\mathcal{E}(D) \;\colon\; Type$,

namely of types of $\mathcal{E}$-effectful data of nominal type $D$ (1);

2. $bind^{\mathcal{E}}_{D_1, D_2} \;\colon\; Hom\big(D_1,\, \mathcal{E}(D_2)\big) \longrightarrow Hom\big(\mathcal{E}(D_1),\,\mathcal{E}(D_2)\big)$,

namely of how to execute a prog while carrying along any previous effects (2);

3. $ret^{\mathcal{E}}_D \;\colon\; D \to \mathcal{E}(D)$,

namely of how to regard plain $D$-data as trivially effectful (4)

subject to:

1. the associativity condition (3)

2. the unitality condition (5)

is called a monad in computer science (also: “Kleisli triple” in functional programming) and serves to encode the notion that all programs may be subject to certain external effects of a kind $\mathcal{E}$ that is specified by the above choices of monad operations.

Here, for the time being (but see below), we write $Hom(D_1, D_2)$ for the set of programs/functions taking data of type $D_1$ to data of $D_2$ (the hom set in the plain category of types).

The first running example above is known as the writer monad, since it encodes the situation where programs may have the additional effect of writing a message string into a given buffer.

The other running example above is naturally called the exception monad.

Relation to other familiar axioms for monads. The above Kleisli/extension-structure, making a Kleisli-style monad in computer science, may and often is encoded in different equivalent ways:

Alternatively postulating operations

1. $D \mapsto \mathcal{E}(D)$ (as before)

2. $fmap^{\mathcal{E}}_{D_1, D_2} \;\colon\; Hom\big(D_1 \to D_2\big) \longrightarrow Hom\big(\mathcal{E}(D_1), \mathcal{E}(D_2)\big)$

3. $ret^{\mathcal{E}}_D \;\colon\; D \to \mathcal{E}(D)$

4. $join^{\mathcal{E}}_D \;\colon\; \mathcal{E}\big( \mathcal{E}(D) \big) \to \mathcal{E}(D)$

such that

1. $fmap^{\mathcal{E}}$ is functorial on data types,

2. $join^{\mathcal{E}}$ is associative and unital (with respect to $ret$) as a natural transformation,

yields the definition of monad more traditionally used in category theory (namely as a monoid object in endofunctors, here on the plain category of data types).

Direct inspection shows that one may bijectively transmute such $bind$- and $join$-operators into each other by expressing them as the following composites (using category theory-notation, for instance “ev” denotes the evaluation map):

(7)$\begin{array}{ll} & fmap^{\mathcal{E}}_{D_1, D_2} \;\colon\; Hom\big(D_1, D_2\big) \xrightarrow{ ret \circ (-) } Hom\big(D_1,\, \mathcal{E}(D_2) \big) \xrightarrow{ bind } Hom\big( \mathcal{E}(D_1),\, \mathcal{E}(D_2) \big) \\ & join^{\mathcal{E}}_D \;\colon\; \mathcal{E}\big( \mathcal{E}(D) \big) \xrightarrow{ \big( id_{ \mathcal{E} \mathcal{E}(D) }, name(id_{ \mathcal{E} D }) \big) } \mathcal{E} \mathcal{E} D \times Hom\big( \mathcal{E}(D),\, \mathcal{E}(D) \big) \xrightarrow{ bind } \mathcal{E}(D) \\ \text{and conversely:} \\ & bind^{\mathcal{E}}_{D, D'} \;\colon\; \mathcal{E}(D) \times Hom\big( \mathcal{E}(D),\, \mathcal{E}(D') \big) \xrightarrow{ \big( id_{\mathcal{E} D}, fmap_{D, \mathcal{E} D'} \big) } \mathcal{E} (D) \times Hom\big( \mathcal{E}(D) , \mathcal{E}\mathcal{E}(D') \big) \xrightarrow{\; ev \;} \mathcal{E} \mathcal{E}(D') \xrightarrow{\; join \;} D' \,. \end{array}$

But in fact, in functional programming-languages one typically considers an enhanced version of the above situation:

In these higher-order languages one has, besides the (hom-)set of programs/functions $Hom\big(D_1, \, D_2\big)$ also the actual data type of functions, namely the function type $D_1 \to D_2$, which in terms of categorical semantics is the internal hom-object $Map(D_1, \, D_2)$ in the cartesian closed category of data types. Therefore, in such languages (like Haskell) the type of the binding operation for given data types $D_1$, $D_2$ is actually taken to be the function type/internal hom

$\begin{array}{ll} bind^{\mathcal{E}}_{D_1, D_2} \;\colon\; && \big( D_1 \to \mathcal{E}(D_2) \big) \to \big( \mathcal{E}(D_1) \to \mathcal{E}(D_2) \big) \\ &\simeq & \mathcal{E}(D_1) \times \big( D_1 \to \mathcal{E}(D_2) \big) \to \mathcal{E}(D_2) \\ & \simeq & \mathcal{E}(D_1) \to \Big( \big( D_1 \to \mathcal{E}(D_2) \big) \to \mathcal{E}(D_2) \Big) \end{array}$

(where we used the hom-isomorphism of the product$\dashv$internal hom-adjunction to re-identify the types on the right)

which (beware) is traditionally written without many of the parenthesis, as follows:

$bind^{\mathcal{E}}_{D_1, D_2} \;\colon\; \mathcal{E} D_1 \to \big( D_1 \to \mathcal{E} D_2 \big) \to \mathcal{E} D_2 \,.$

In general (except in the base topos of Sets), such an iterated function type/internal hom is richer than (certainly different from) the corresponding plain hom set, and accordingly a “Kleisli triple” defined as above but with the binding operation typed in this internal way is more information than a plain monad on the underlying category of types: namely what is called a strong monad (eg. McDermott & Uustalu (2022)).

On such a strong monad, the bind operation is defined as the following composite:

$\mathcal{E}(D_1) \times \mathcal{E} Map(D_1,\,D_2) \xrightarrow{\; strength_{\mathcal{E}} \;} \mathcal{E}\big(D_1 \times Map(D_1, \, \mathcal{E} D_2) \big) \xrightarrow{ \mathcal{E} eval_{D_1, \mathcal{E} D_2} } \mathcal{E} \mathcal{E} D_2 \xrightarrow{\; \mu_{D_2} \;} \mathcal{E} D_2 \,.$

This makes the monads be enriched monads in the self-enrichment of the category of types given by the function type/internal hom.

Yet more structure on effect-monads is available in dependent type theories with type universes, where one may demand that the monad operation $D \mapsto T(D)$ is not just an endofunction on the set of types, but an endomorphism of the type universe. At least for idempotent monads this case is further discussed at reflective subuniverse and modal type theory and maybe elsewhere.

Further in the practice of programming: if programs may cause external effects, as above, then one will often want to have some of them handle these effects.

This is particularly evident in the above running examples of exceptions whose whole design purpose typically is to be handled when they arise.

Since a “handling” of $\mathcal{E}$-effects should mean that these be done with and turned into pure data of some actual type $D$, an $\mathcal{E}$-effect handler on(to) a data type $D$ should primarily consist of a program of the form

$\mathcal{E}(D) \to D \,.$

that handles effects produced by $\mathcal{E}$-effectful programs $D' \to \mathcal{E}(D)$, turning them into pure computations $D' \to D$.

But in addition, such a handler needs to handle effects that have been “carried along” (2) from previous computations, even along otherwise in-effectful computations $prog_{0,1} \;\colon\; D_{0} \to D_{1}$; therefore all these need to be assigned handlers:

$hndl^{\mathcal{E}}_{D_2} prog_{1,2} \;\colon\; \mathcal{E}(D_1) \to D_2 \,.$

Of such choice of effect handling, consistency demands that:

1. first handling all previous effects carried along (2) and then the newly produced effects by a given $prog \,\colon\, D \to \mathcal{E}(D')$ has the same result as letting $prog$ take care of carrying along previous effects by passing to $prog[-]$ and then handling the resulting accumulation at once:

2. handling the trivial effect ought to be no extra operation:

(8) 

A data structure consisting of such assignments $hndl^{\mathcal{E}}$ subject to these “laws” is known as an Kleisli triple algebra (e.g. Uustalu (2021), Lec. 2) or algebra over an extension system (see here) for $\mathcal{E}$ and is bijectively the same as what in traditional category theory is known as an algebra over $\mathcal{E}$ or $\mathcal{E}$-algebra or, maybe best: an $\mathcal{E}$-module or $\mathcal{E}$-modal type.

Given a pair of such $\mathcal{E}$-modal types $\big(D_1, hndl^{\mathcal{E}}_{D_1} \big)$, $\big(D_2, hndl^{\mathcal{E}}_{D_2} \big)$, a function $\phi \,\colon\, D_1 \to D_2$ is a homomorphism between them if the result of handling $\mathcal{E}$-effects before or after applying $\phi$ is the same, hence if for all functions $f \,\colon\, D_0 \to D_1$ the following diagram commutes:

Free $\mathcal{E}$-effect handlers. Notice that above we motivated already the binding operation (2) as a kind of $\mathcal{E}$-effect handling: namely as the “carrying along” of previous $\mathcal{E}$-effects. This intuition now becomes a precise statement:

For any $D_2 \;\colon\; Type$ we may tautologically handle (8) $\mathcal{E}$-effects by absorbing them into the data type $\mathcal{E}(D_2)$, with the effect-handler simply being the effect-binding operation (2):

(9)$hndl^{\mathcal{E}}_{\mathcal{E}(D_2)} \Big( D_1 \xrightarrow{ prog } \mathcal{E}(D_2) \Big) \;\coloneqq\; bind^{\mathcal{E}} prog \;\colon\; \mathcal{E}(D_1) \to \mathcal{E}(D_2) \,.$

The $\mathcal{E}$-effect-handlers (8) arising this way are called free.

The full subcategory of free $\mathcal{E}$-effect handlers among all $\mathcal{E}$-modal types is known as the Kleisli category. By the Kleisli equivalence, this is equivalent to the (plain) category (6) of $\mathcal{E}$-effectful programs that we started with. Here this means that:

• Plain data types with $\mathcal{E}$-effectful programs betweem them are equivalently data types freely equipped with the structure of $\mathcal{E}$-effect handlers.

which makes a lot of sense.

(…) e.g. Uustalu & Vene (2008), POM13, GKOBU16, KRU20 (…):

• On the one hand:

• A Kleisli map for a monad $\mathcal{E}$ is a program

$prog \;\colon\; D \to \mathcal{E}(D')$

causing an external $\mathcal{E}$-effect.

• A Kleisli-module for a monad $\mathcal{E}T$ is a prescription

$hdl^{\mathcal{E}}_D id_D \;\colon\; \mathcal{E}(D) \to D$

for handling such $\mathcal{E}$-effects.

• Dually:

• A co-Kleisli map for a comonad $\mathcal{C}$ is a program

$prog \;\colon\; \mathcal{C}(D) \to D'$

subject to an external $\mathcal{C}$-“context” (Uustalu & Vene (2008), POM13)

(a $\mathcal{C}$-cause).

• A co-Kleisli co-module for a comonad $\mathcal{C}$ is a program

$prvd^{\mathcal{C}}_D id_D \;\colon\; D \to \mathcal{C}(D)$

producing or providing such $\mathcal{C}$-contexts.

(cf. [Uustalu (2021), Lect. 3, slide 9])

(…)

## Examples

Various monads are definable in terms of standard type-forming operations (such as product types, function types, etc.). These include the following.

#### State monad and Random access memory

A functional program with input of type $X$, output of type $Y$ and mutable state $S$ is a function (morphism) of type $X \times S \longrightarrow Y \times S$. Under the (Cartesian product $\dashv$ internal hom)-adjunction this is equivalently given by its adjunct, which is a function of type $X \longrightarrow [S, S \times Y ]$. Here the operation $[S, S\times (-)]$ is the monad induced by the above adjunction and this latter function is naturally regarded as a morphism in the Kleisli category of this monad. This monad $[S, S\times (-)]$ is called the state monad for mutable states of type S.

#### Maybe monad and Controlled failure

The maybe monad is the operation $X \mapsto X \coprod \ast$. The idea here is that a function $X \longrightarrow Y$ in its Kleisli category is in the original category a function of the form $X \longrightarrow Y \coprod \ast$ so either returns indeed a value in $Y$ or else returns the unique element of the unit type/terminal object $\ast$. This is then naturally interpreted as “no value returned”, hence as indicating a “failure in computation”.

#### Exception monad and Exception handling

The continuation monad on a given type $S$ acts by $X \mapsto [[X,S],S]$.

(…)

Other monads may be supplied “axiomatically” by the programming language, meaning that they are data structures typed as monads, but whose actual type formation, binding- and return-operations are special purpose operations provided by the programming environment.

This includes:

In this vein:

## References

### General

The extension system-style presentation of monads as used in computer science is briefly mentioned in:

and expanded on in

but not related there to computation.

The original observation of monads as “notions of computation” is:

On the impact of Moggi (1991):

• Martin Hyland, John Power, The Category Theoretic Understanding of Universal Algebra: Lawvere Theories and Monads, Electronic Notes in Theoretical Computer Science (ENTCS) archive Volume 172, April, 2007 Pages 437-458 (pdf)

In the generality of relative monads:

The dual notion of comonads in computer science as modelling contexts:

Textbook accounts of monads as used in actual programming languages such as Haskell:

Further discussion/exposition of the notion and application of (co)monads in computer science:

and an exposition of category theory and monads in terms of Haskell is in

A comparison of monads with applicative functors (also known as idioms) and with arrows (in computer science) is in

• Exequiel Rivas, Relating Idioms, Arrows and Monads from Monoidal Adjunctions, (arXiv:1807.04084)

Discussion of comonads in this context includes