nLab monad (in computer science)

Contents

This entry is about monads as known from categorical algebra but in their application to computer science. See also at monad (disambiguation).


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
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity 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 set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
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 (1989), 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 p. 321, and which some authors denote by an upper-star, “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: Strong 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 richer or stronger structure than that of a plain monad on the underlying category of types: namely it is an enriched monad or equivalently a strong monad with respect to the self-enrichment of the symmetric monoidal closed category of types (Moggi 1991 §3, cf. Goubault-Larrecq, Lasota & Nowak 2002, McDermott & Uustalu (2022)).

On such an enriched/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 \,.

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

In this case – and in most discussions by default – the symmetric monoidal closed category of types is assumed to be cartesian closed (“classical types”) but in contexts of linear type theory (such as quantum computation) it may be non-cartesian (or both: cf. doubly closed monoidal category).


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

(from Overton 2014)

By formal duality, all of the above discussion has a dual version, where now (e.g. Uustalu & Vene (2008), POM13, GKOBU16, KRU20):

  • comonads encode computational contexts (co-effects),

  • their coproduct operation is the duplication (co-join) of contexts which serves to extend (co-bind) contexts over consecutive programs,

  • comodules over comonads are data structures that provide (co-handle) such context.

In more detail:

  • Above we had that:

    • 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.

  • Now 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])


Syntactic idea: Do-notation

Finally, to turn all this into an efficient programming language one just has to declare a convenient syntax for denoting Kleisli composition.

One such syntax is known as “do notation” (introduced with “{...}” instead of “do” by Launchbury 1993 §3.3, then promoted by Mark Jones in the 1990s [HHPW07, p. 25] and adopted by Haskell in version 1.3, for review see Benton, Hughes & Moggi 2002 p. 70, Milewski 2019 §20.3), which aims to jointly express:

  1. successive Kleisli composition in words like “do this, do that, and return the result”,

  2. any intermediate bind-operation as “extracting” a DD-datum dd out of an (D)\mathcal{E}(D)-datum EE with notation d <- E

Syntactically, do-notation is the following syntactic sugar for combined Kleisli composition and variable binding:

  1. do prog \;\;\equiv\;\; prog

  2. do prog1 prog2 \;\;\equiv\;\; prog1 bind (\_ -> prog2)

  3. do (x <- prog1) prog2 \;\;\equiv\;\; prog1 bind (\x -> prog2)

This is, first of all, a suggestive notation (in fact a “domain specific embedded programming language”, see there) for expressing effect-binding:

but thereby it furthermore provides a convenient means of expressing successive Kleisli-composition simply by successivley “calling” the separate procedures, much in the style of imperative programming (which thereby is emulated/encapsulated by pure functional programming):

but the notation becomes more suggestive with the rule that the “<-”-symbols may notationally be suppressed for functions with trivial in- or out-put (ie. of unit type *\ast) besides their \mathcal{E}-effect, as in this example:

This case brings out clearly how the ambient “doreturn”-syntax block expresses the (Kleisli-)composition of any number of \mathcal{E}-effectful procedures.

On top of that the “<-”-syntax is meant to be suggestive of reading out a value. This is accurate imagery for the state monad (and its abstraction to the IO-monad), where from the two pasic operations of reading/writng a global variable

read : WState(W) read w(w,w)write : WWState(*) write w(ww) \array{ read &\colon& W State(W) \\ read &\equiv& w \mapsto (w,w) } \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\; \array{ write &\colon& W \to W State(\ast) \\ write &\equiv& w \mapsto (w' \mapsto w) }

any WW-stateful program, such as the simple example

inc : State(*) inc nn+1 \array{ inc &\colon& \mathbb{N}State(\ast) \\ inc &\equiv& n \mapsto n+1 }

may be constucted in do-notation, such as:

For a similar effect monad such as the list monad the analogous do-code for incrementing all entries in a list of numbers looks as follows:

Here The do-notation on the right evokes the idea that in each step a number n:n \colon \mathbb{N} is “read out” from MyList and then its increment returned — but leaves linguistically implicit the idea that this operation is to be performed for all elements of the list and all results re-compiled into an output list.

Indeed, in general it is misleading to think of Kleisli composition as being about “reading out” data. What Kleisli composition is really about is acting on data that has generators and defining a program by what it does on generators, hence for a given generating datum:

Therefore the conceptually more accurate (if maybe less concise) program-linguistic reflection of the monadic effect-binding operation would be a “fordo”-block:

In terms of such for-do-notation, the generic case that we started with above has the following syntactic rendering:

This syntax may be notationally less concise but it evokes rather closely what is actually going on in programming with monadic effects.

For example, the above operation of icrementing all numbers in a given list reads in fordo-notation as follows:

neatly indicative of how the operation +1+1 is applied for every number nn found in the list.

(NB.: There is no clash with fordo-notation as used for loops in imperative programming, since functionally these are instead expressed by recursion.)

The appropriateness of rendering effect binding as a fordo-expression becomes yet more pronounced in contexts of substructural typing contexts such as in linear type theory, where the idea of “reading out” of monadic types via “<-”-notation becomes yet more dubious.

For example, consider the relative monad (this example) which sends sets to the vector spaces that are their linear spans:

Q:Set Vect W W𝟙 \array{ \mathllap{\mathrm{Q} \;\;\colon\;\;} Set &\longrightarrow& Vect \\ W &\mapsto& \underset{W}{\oplus} \mathbb{1} }

with

bind Q:(WQW) (QWQW) (w|ψ w) ( wq W|w wq w|ψ w) \array{ \mathllap{bind^{\mathrm{Q}} \;\;\colon\;\;} (W \to \mathrm{Q}W') &\longrightarrow& (\mathrm{Q}W \to \mathrm{Q}W') \\ \left( w \mapsto \left\vert \psi_w \right\rangle \right) &\mapsto& \left( \sum_w q_{{}_W} \left\vert w \right\rangle \,\mapsto\, \sum_w q_{{}_w} \left\vert \psi_w \right\rangle \right) }

In this case the traditional do-notation would suggest that given a vector one may “read out” a basis element from it – which does not make conceptual sense.

Instead, what’s really happening is that to define a linear map G:QWG \colon \mathrm{Q}W \to \mathscr{H} on a vector space equipped with a linear basis WW (literally: a set of free generators) it is sufficient to define this map for each basis-vector |w\left\vert w \right\rangle — and this is just what the fordo-notation for the Q\mathrm{Q}-monad expresses:


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 (cf. Moggi 1991, Exp. 1.1):

State monad and Random access memory

A functional program with input of type DD, output of type DD' and mutable state WW is a function (morphism) of type D×WD×WD \times W \longrightarrow D' \times W – also called a Mealy machine (see there).

Under the (Cartesian product \dashv internal hom)-adjunction (currying) this is equivalently given by its adjunct, which is a function of type D[W,W×D]D \longrightarrow [W, W \times D' ]. Here the operation [W,W×()][W, W\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 [W,W×()][W, W\times (-)] is called the state monad for mutable states of type WW:

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:

Further discussion:

On the impact of Moggi (1991):

Origin of the do-notation for Kleisli composition of effectful programs:

  • John Launchbury, §3.3 in: Lazy imperative programming, Proceedings of ACM Sigplan Workshop on State in Programming Languages, Copenhagen (1993) [pdf, pdf]

Introducing the notion of monad transformers:

More (early) literature is listed here:

In the generality of relative monads:

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

on codo-notation for comonadic contexts:

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

The identification of (co)effect handling with (co)modales over the given (co)monad:

Discussion in actual programming languages such as Haskell:

and Scala:

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

Further 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)

In quantum computation

Discussion of aspects of quantum computing in terms of monads:

The quantum IO monad:

Exposition:

Implementation in Haskell:

Much of the text and the diagrams in the entry above follow

Last revised on December 12, 2023 at 23:49:33. See the history of this page for a list of all contributions to it.