nLab
monad (in computer science)

Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type
falseinitial objectempty type
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
logical conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type/path type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Constructivism, Realizability, Computability

Contents

Idea

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

This is essentially the same structure as a monad in the sense of 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 an account of the use of monads in industry see Benton15, pp. 11-12.

For instance when the monad T()T(-) forms product types T(X)X×QT(X) \coloneqq X \times Q with some fixed type QQ that carries the structure of a monoid, then a Kleisli function f:XY×Qf : X \to Y \times Q may be thought of as a function XYX \to Y that produces a side effect output of type QQ. The Kleisli composition of two functions f:XY×Qf \colon X \to Y \times Q and g:YZ×Qg \colon Y \to Z \times Q then not only evaluates the two programs in sequence but also combines their QQ-output using the monoid operation of QQ; so if fx=(y,q)f x = (y,q) and gy=(z,q)g y = (z,q') then the final result of (gf)(x)(g \circ f)(x) will be (z,qq)(z, q q'). For example, QQ might be the set of strings of characters, and the monoid operation that of concatenation of strings (i.e. QQ is the free monoid on the type of characters). If the software is designed such that values of type QQ computed in this way appear on the user’s screen 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 𝒞\mathcal{C}, whose

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:𝒞𝒞 T \colon \mathcal{C} \longrightarrow \mathcal{C}

on the syntactic category. This functor

  1. sends each type, hence object X𝒞X \in \mathcal{C} to another object T(X)T(X);

  2. the unit natural transformation ϵ:Id 𝒞T\epsilon \colon Id_{\mathcal{C}} \Rightarrow T of the monad TT provides for each type XX a component morphism pure X:XT(X)pure_X : X \to T(X);

  3. the multiplication natural transformation μ:TTT\mu \colon T \circ T \Rightarrow T of the monad provides for each object XX a morphism μ X:T(T(X))T(X)\mu_X : T(T(X)) \to T(X) which induces the Kleisli composition by the formula

(gf) (YgT(Z)) Kleisli(XfT(Y)) XfT(Y)T(g)T(T(Z))μ(Z)TZ, \begin{aligned} (g \circ f) &\coloneqq (Y \stackrel{g}{\to} T(Z)) \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)T(g) in the middle of the last line makes use of the fact that T()T(-) is indeed a functor and hence may also be applied to morphisms / functions between types. The last morphism μ(Z)\mu(Z) is the one that implements the “TT-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 𝒞\mathcal{C} will be at least monoidal, and the corresponding kind of ‘nice’ interaction corresponds to the monad’s being a strong monad.

The ‘bind’ operation is a means of describing multiplication on such a strong monad MM. It is a term of the form MA(MB) AMBM A \to (M B)^A \to M B, which is equivalent to a map of the form MA×MB AMBM A \times M B^A \to M B. It is the composite

MA×MB AstrengthM(A×MB A)Meval A,MBMMBmBMB M A \times M B^A \stackrel{strength}{\to} M(A \times M B^A) \stackrel{M eval_{A, M B}}{\to} M M B \stackrel{m B}{\to} M B

where m:MMMm \colon M M \to M is the monad multiplication.

When monads are defined in Haskell, the Kleisli composition, ‘bind’, is defined in Haskell. So monads in Haskell are always enriched monads, according to the self-enrichment defined by the function type in Haskell.

Examples

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

Other monads may be supplied “axiomatically” by the programming language,

This includes

See also:

Examples of (co)monads in (homotopy) type theory involve in particular modal operators as they appear in

See also

For an approach to composing monads, see

Another approach to modelling side effects in functional programming languages are

Free monads in computer science appear in the concepts of

Other generalizations are

There is also

References

General

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

The impact of Moggi’s work is assessed and a case for Lawvere theories is made in

Effects treated this way are known as algebraic effects.

Expositions of monads in computer science include

See also:

The specification of monads in Haskell is at

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

Generalization from monads to relative monads is discussed in

Discussion of comonads in this context includes

In quantum computation

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