nLab monad (in computer science)

Contents

Context

Computation

Categorical algebra

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

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
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
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction setinternal homfunction type
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian productdependent productdependent product type
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijectionisomorphism/adjoint equivalenceequivalence of types
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
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

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 DD of a new data type (D)\mathcal{E}(D) of “DD-data with \mathcal{E}-effects”,

  2. to any pair of \mathcal{E}-effectful functions (programs) of the form prog 12:D 1(D 2)prog_{12} \,\colon\, D_1 \to \mathcal{E}(D_2) and prog 23:D 2(D 3)prog_{23} \,\colon\, D_2 \to \mathcal{E}(D_3) of an effective-composite function bind prog 23prog 12():D 1(D 3)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 DD of a function ret D :D(D)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.

Basic idea: Monadic effects

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

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

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

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

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

Given such an \mathcal{E}-effectful program prog 12:D 1(D 2)prog_{12} \;\colon\; D_1 \to \mathcal{E}(D_2) and given a subsequent program prog 23:D 2(D 3)prog_{23} \,\colon\, D_2 \to \mathcal{E}(D_3) accepting nominal input data of type D 2D_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 (D)=D\mathcal{E}(D) = D is actually the trivial sort of effect), but their evident intended composition is, clearly, obtained by:

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

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

    such that bind prog 23:(D 2)(D 3)bind^{\mathcal{E}} prog_{23} \,\colon\, \mathcal{E}(D_2) \to \mathcal{E}(D_3):

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

    2. “acts as prog 23prog_{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 prog 23prog 12bind^{\mathcal{E}} prog_{23} \;\circ\; prog_{12}

as follows:

(Beware that we are denoting by “bind prog()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 *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 prog 23bind^{\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)D 2×StringWrite(D_2) \,\coloneqq\, D_2 \times String, the evident way is to use the concatenation String×StringconcatStringString \times String \xrightarrow{\; concat \;} String and set:

bind Writeprog 23D 2×Stringprog 23×Id StringD 3×String×StringId D 3×concatD 3×String. 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 :StringStringString\nabla \,\colon\, String \sqcup String \to String, which amounts to keep forwarding the exception that has already been thrown, if any:

bind Excepprog 23D 2Stringprog 23Id StringD 3StringStringid D 3D 3String.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 prog 34(bind prog 23prog 12)=bind (bind prog 34prog 23)prog 12. 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:D 0D 1prog_{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:D(D) ret_{D} \;\colon\; D \xrightarrow{\;} \mathcal{E}(D)

which does nothing but “return” data of type DD, but re-regarded as effectful (D)\mathcal{E}(D)-data in a trivial way; so that we may construct the trivially effectful program ret D 1 𝒟prog 01:D 0(D 1)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 DD×StringD \to D \times String which assigns the empty string ret Write:d(d,)ret^{Write} \;\colon\; d \mapsto (d, \varnothing).

In the other example above, of exception handling, the trivial effect DDStringD \to D \sqcup String is just not to throw an exception, which is just ret Excep:ddret^{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 prog 01ret D 0()=prog 01andbind ret D 1prog 01()=prog 01. 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()Kl(\mathcal{E}) of a monad \mathcal{E} on the category TypeType of data types with programs between them:

(6)Obj(Kl()) = Obj(Type) Hom(Kl())(D 1,D 2) = Hom(Type)(D 1,(D 2)) () Kl()() = () Typebind (). \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 iD_i of

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

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

  2. bind D 1,D 2 :Hom(D 1,(D 2))Hom((D 1),(D 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 D :D(D)ret^{\mathcal{E}}_D \;\colon\; D \to \mathcal{E}(D),

    namely of how to regard plain DD-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)Hom(D_1, D_2) for the set of programs/functions taking data of type D 1D_1 to data of D 2D_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(D)D \mapsto \mathcal{E}(D) (as before)

  2. fmap D 1,D 2 :Hom(D 1D 2)Hom((D 1),(D 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 D :D(D)ret^{\mathcal{E}}_D \;\colon\; D \to \mathcal{E}(D)

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

such that

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

  2. join join^{\mathcal{E}} is associative and unital (with respect to retret) 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 bindbind- and joinjoin-operators into each other by expressing them as the following composites (using category theory-notation, for instance “ev” denotes the evaluation map):

(7) fmap D 1,D 2 :Hom(D 1,D 2)ret()Hom(D 1,(D 2))bindHom((D 1),(D 2)) join D :((D))(id (D),name(id D))D×Hom((D),(D))bind(D) and conversely: bind D,D :(D)×Hom((D),(D))(id D,fmap D,D)(D)×Hom((D),(D))ev(D)joinD. \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}

Refined idea: Internal monads

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(D 1,D 2)Hom\big(D_1, \, D_2\big) also the actual data type of functions, namely the function type D 1D 2D_1 \to D_2, which in terms of categorical semantics is the internal hom-object Map(D 1,D 2)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 1D_1, D 2D_2 is actually taken to be the function type/internal hom

bind D 1,D 2 : (D 1(D 2))((D 1)(D 2)) (D 1)×(D 1(D 2))(D 2) (D 1)((D 1(D 2))(D 2)) \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\dashvinternal hom-adjunction to re-identify the types on the right)

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

bind D 1,D 2 :D 1(D 1D 2)D 2. 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:

(D 1)×Map(D 1,D 2)strength (D 1×Map(D 1,D 2))eval D 1,D 2D 2μ D 2D 2. \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.

In particular, monads as used in Haskell are really strong/enriched monads, in this way.


Yet more structure on effect-monads is available in dependent type theories with type universes, where one may demand that the monad operation DT(D)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 idea: Monad modules

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 DD, an \mathcal{E}-effect handler on(to) a data type DD should primarily consist of a program of the form

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

that handles effects produced by \mathcal{E}-effectful programs D(D)D' \to \mathcal{E}(D), turning them into pure computations DDD' \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:D 0D 1prog_{0,1} \;\colon\; D_{0} \to D_{1}; therefore all these need to be assigned handlers:

hndl D 2 prog 1,2:(D 1)D 2. 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:D(D)prog \,\colon\, D \to \mathcal{E}(D') has the same result as letting progprog take care of carrying along previous effects by passing to prog[]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 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 (D 1,hndl D 1 )\big(D_1, hndl^{\mathcal{E}}_{D_1} \big), (D 2,hndl D 2 )\big(D_2, hndl^{\mathcal{E}}_{D_2} \big), a function ϕ:D 1D 2\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:D 0D 1f \,\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:TypeD_2 \;\colon\; Type we may tautologically handle (8) \mathcal{E}-effects by absorbing them into the data type (D 2)\mathcal{E}(D_2), with the effect-handler simply being the effect-binding operation (2):

(9)hndl (D 2) (D 1prog(D 2))bind prog:(D 1)(D 2). 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.


Dual idea: Comonadic contexts

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

By formal duality:

  • On the one hand:

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

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

      causing an external \mathcal{E}-effect.

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

      hdl D id D:(D)D 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:𝒞(D)D 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 D 𝒞id D:D𝒞(D) 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

Definable monads

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 XX, output of type YY and mutable state SS is a function (morphism) of type X×SY×SX \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[S,S×Y]X \longrightarrow [S, S \times Y ]. Here the operation [S,S×()][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×()][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 XX*X \mapsto X \coprod \ast. The idea here is that a function XYX \longrightarrow Y in its Kleisli category is in the original category a function of the form XY*X \longrightarrow Y \coprod \ast so either returns indeed a value in YY 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

(…) exception monad (…)

Continuation monad and Continuation-passing

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

(…)

Axiomatic monads

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:

and emphasis on the combination of monads, comonads and graded modalities:

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:

See also:

The specification of monads in Haskell is at:

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

On the issue of the CS-style monads really being strong monads:

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

  • David Overton, Comonads in Haskell, 2014 (web)

In quantum computation

Discussion of aspects of quantum computing in terms of monads:

The quantum IO monad:

Exposition:

Implementation in Haskell:

Last revised on November 15, 2022 at 09:49:09. See the history of this page for a list of all contributions to it.