nLab
monad (in computer science)

Idea

In computer science, a monad describes a “notion of computation”. Formally, it is a map that

• sends every type $X$ of some given programming language to a new type $T(X)$ (called the “type of $T$-computations with values in $X$”);

• equipped with a rule for composing two functions of the form $f:X\to T(Y)$ (called Kleisli functions) and $g:Y\to T(Z)$ to a function $g\circ f:X\to T(Z)$ (their Kleisli composition);

• in a way that is associative in the evident sense and unital with respect to a given unit function called ${\mathrm{pure}}_X:X\to T(X)$, to be thought of as taking a value to the pure computation that simply returns that value.

This is essentially the same structure as a monad in category theory, but presented differently; see below for the precise relationship.

For imperative programs in functional programming

Monads provide one way to “embed imperative programming? in functional programming”, and are used that way notably in the programming language Haskell. (But monads, as well as comonads and related structures, exist much more generally in programming languages; an exposition is in (Harper)).

For instance when the monad $T(-)$ forms product types $T(X)≔X\times Q$ with some fixed type $Q$ that carries the structure of a monoid, then a Kleisli function $f:X\to Y\times Q$ may be thought of as a function $X\to Y$ that produces a “side effect” output of type $Q$. The Kleisli composition of two functions $f:X\to Y\times Q$ and $g:Y\to Z\times Q$ then not only evaluates the two programs in sequence but also combines their $Q$-output using the monoid operation of $Q$; so if $fx=(y,q)$ and $gy=(z,q\prime )$ then the final result of $(g\circ f)(x)$ will be $(z,qq\prime )$. For example, $Q$ might be the set of strings of characters, and the monoid operation that of concatenation of strings (i.e. $Q$ is the free monoid on the type of characters). If the software is designed such that values of type $Q$ computed in this way appear on the user’s scteen or are written to memory, then this is a way to encode input/output in functional programming (see the IO monad? below).

But monads have plenty of further uses. They are as ubiquituous (sometimes in disguise) in computer science as monads in the sense of category theory are (sometimes in disguise) in category theory. This is no coincidence, see Relation to monads in category theory below.

Relation to monads in category theory

In computer science, a programming language may be formalised or studied by means of a category, called the syntactic category $𝒞$, whose

• objects $X\in 𝒞$ are the types of the language,

• morphisms $X\to Y$ are the terms or programs (or an equivalence class of such) that takes a value of type $X$ as input and returns a value of type $Y$.

This point of view (see computational trinitarianism) is particularly useful when studying purely functional programming languages.

Under this relation between type theory and category theory monads on the type system in the sense of computer science are monads in the sense of category theory, being certain endofunctors

$$T:𝒞\to 𝒞$$T : \mathcal{C} \to \mathcal{C}

on the syntactic category. This functor

1. sends each type, hence object $X\in 𝒞$ to another object $T(X)$;

2. the unit natural transformation $ϵ:{\mathrm{Id}}_{𝒞}\Rightarrow T$ of the monad $T$ provides for each type $X$ a component morphism ${\mathrm{pure}}_X:X\to T(X)$;

3. the multiplication natural transformation $\mu :T\circ T\Rightarrow T$ of the monad provides for each object $X$ a morphism ${\mu }_X:T(T(X))\Rightarrow X$ which induces the Kleisli composition by the formula

$$\begin{array}{rl}(g\circ f)& ≔(Y\stackrel{g}{\to }T(Y)){\circ }_{\mathrm{Kleisli}}(X\stackrel{f}{\to }T(Y))\\ & ≔X\stackrel{f}{\to }T(Y)\stackrel{T(g)}{\to }T(T(Z))\stackrel{\mu (Z)}{\to }TZ\end{array},$$\begin{aligned} (g \circ f) &\coloneqq (Y \stackrel{g}{\to} T(Y)) \circ_{Kleisli} (X \stackrel{f}{\to} T(Y)) \\ & \coloneqq X \stackrel{f}{\to} T(Y) \stackrel{T(g)}{\to} T(T(Z)) \stackrel{\mu(Z)}{\to} T Z \end{aligned} \,,

Here the morphism $T(g)$ in the middle of the last line makes use of the fact that $T(-)$ is indeed a functor and hence may also be applied to morphisms / functions between types. The last morphism $\mu (Z)$ is the one that implements the ”$T$-computation”.

The monads arising this way in computer science are usually required also to interact nicely with the structure of the programming language, as encoded in the structure of its syntactic category; in most cases, terms of the language will be allowed to take more than one input, so the category $𝒞$ will be at least monoidal, and the corresponding kind of ‘nice’ interaction corresponds to the monad’s being a strong monad.

Examples

• A number of monads are definable in terms of standard type-forming operations, such as the maybe monad?, the reader monad?, the writer monad?, and the state monad?.

• Other monads may be supplied “axiomatically” by the programming language, such as the IO monad? in Haskell.

• Equipping homotopy type theory (say implemented as a programming language concretely in Coq or Agda) with two axiomatic idempotent monads, denoted $♯$ and $\Pi$, with some additional data and relations, turns it into cohesive homotopy type theory. See also modal type theory.

Related concepts

Examples of (co)monads in type theory appear in

• modal type theory.

References

The original reference for monads as ‘notions of computation’ is

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

Expositions are in

• Robert Harper, Of course ML Has Monads! (2011) (web)

The specification of monads in Haskell is at

• The Haskell programming language, Monad laws

Discussion of aspects of quantum computing in terms of monads in functional programming are in

• Thorsten Altenkirch, Alexander Green, The quantum IO monad, in Semantic Techniques in Quantum Computation, January 2009, appeared in 2010 (pdf, talk slides)