nLab monad transformer

Contents

Context

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 functional programming using monads for computational effects, monad transformers [Espinosa 1994 §4, 1995 §2.6] are type constructors which take one monad to another in a compatible way.

In practice this is typically motivated by and used for combining a monadic effect new\mathcal{E}_{new} into any given one \mathcal{E} by new\mathcal{E} \mapsto \mathcal{E}_{new} \circ \mathcal{E} via a universal distributive law.

Formally, a monad transformer on a given category C\mathbf{C} (of data types) is a pointed endofunctor on the category of monads Mnd(C)Mnd(\mathbf{C}) (this is made explicit in Winitzki 2022, p. 474), namely:

  1. an endofunctor \mathcal{E} \mapsto \mathcal{E}' taking monads to monads

  2. for each \mathcal{E} a morphism of monads trans :trans_{\mathcal{E}} \,\colon\, \mathcal{E} \longrightarrow \mathcal{E}' (a monad transformation)

  3. such that these are natural with respect to morphism of monads.

This construction is sometimes viewed (see HP07, and at Eff) as a complication resulting from passing to monads from the setting of Lawvere theories, where any two theories may be naturally combined.

Details

The following Def. is essentially the notion in Liang, Hudak & Jones 1995, left column of p. 339, as now commonly used in Haskell (see the Haskell Transformer class).

Remark

These authors, and the functional programming/Haskell-community following them, insist that “trans (-)trans_{(\text{-})}(1) — which they denote “lift-lift \text{-}” — is not just a transformation between a single pair of monads, but a component a pointed endofunctor on the whole category of monads. This further condition may be considered (or not) in addition to the following discussion.

Definition

Given monads \mathcal{E}, \mathcal{E}' on the same category C\mathbf{C}, a monad transformer between them is:

  • a system of morphisms

    (1)D:Typetrans D:(D)(D) D \,\colon\, Type \;\;\;\;\;\; \vdash \;\;\;\;\;\; trans_D \,\colon\, \mathcal{E}(D) \to \mathcal{E}'(D)

which

  1. preserves the return-operations, in that

    (2)transret =ret , trans \circ ret^{\mathcal{E}} \;=\; ret^{\mathcal{E}'} \,,
  2. preserves the bind-operations, in that for 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)

    we have

    (3)trans D 3((bind prog 23)prog 12)=bind ((trans D 3prog 23))(trans D 2prog 12). trans_{D_3} \circ \Big( \big( bind^{\mathcal{E}} prog_{23} \big) \circ prog_{12} \Big) \;\;=\;\; bind^{\mathcal{E}'} \Big( \big( trans_{D_3} \circ prog_{23} \big) \Big) \circ \big( trans_{D_2} \circ prog_{12} \big) \mathrlap{\,.}

In Schrijvers, Piróg, Wu & Jaskelioff 2019 p. 99 the analogous condition is stated in terms of the join-operation. We may check that these are equivalent:

Proposition

A system of transformations trans D:(D)(D)trans_D \,\colon\, \mathcal{E}(D) \to \mathcal{E}'(D) is a monad transformer in the sense of Def. (cf. Rem. ) iff it is a homomorphism of monads (in the original sense of Maranda 1966), i.e.:

  1. a natural transformation trans:\trans \,\colon\, \mathcal{E} \to \mathcal{E}' of the underlying functors,

  2. respecting the unit/return-operation, in that the following diagrams commute:

    (4)D ret D (D) id trans D D ret D (D) \array{ D &\overset{ret^{\mathcal{E}}_D}{\longrightarrow}& \mathcal{E}(D) \\ \mathllap{{}^{id}}\Big\downarrow && \Big\downarrow\mathrlap{{}^{trans_D}} \\ D &\underset{ret^{\mathcal{E}'}_D}{\longrightarrow}& \mathcal{E}'(D) }
  3. respecting the join-operation (the “monad multiplication”), in that it makes the following diagram commute:

Proof

Recall that the relation between the bind- and join-operations is:

(5)bind (f:D 1(D 2))join D 2 (f) bind^{\mathcal{E}} \big( f \,\colon\, D_1 \to \mathcal{E}(D_2) \big) \;\equiv\; join^{\mathcal{E}}_{D_2} \circ \mathcal{E}(f)

and

(6)(f:D 1D 2)bind (D 1fD 2ret D 2 (D 2)) \mathcal{E}(f \,\colon\, D_1 \to D_2) \;\equiv\; bind^{\mathcal{E}} \big( D_1 \xrightarrow{\; f \;} D_2 \xrightarrow{\; ret^{\mathcal{E}}_{D_2} \;} \mathcal{E}(D_2) \big)
(7)join D bind (id (D)). join^{\mathcal{E}}_{D} \;\equiv\; bind^{\mathcal{E}}\big( id_{\mathcal{E}(D)} \big) \,.

Now in one direction: Given a morphism of monads trans:trans \,\colon\, \mathcal{E} \to \mathcal{E}', then consider the pasting diagram of the above square with the naturality square of transtrans as follows:

Going diagonally through this commuting diagram and using (5): The total left and bottom composite is the left hand side of (3) and the total top and right composite is the right hand side of (3), thus proving their equality.

In the other direction, if (3) holds then its restriction to the case prog 12idprog 23prog_{12} \,\equiv\, id \,\equiv\, prog_{23} immediately yields, by (7), the above commtuting diagram expressing respect for the join.

It just remains to see that the system of transformations trans (-)trans_{(\text{-})} (1) is necessarily natural. This is shown by the following sequence of equalities, for prog:D 1D 2prog \,\colon\, D_1 \to D_2:

trans D 2(prog) =trans D 2bind (D 1progD 2ret D (D 2)) =bind (D 1progD 2ret D (D 2)trans D 2(D 2))trans D 1 =bind (D 1progD 2ret D (D 2))trans D 1 =(prog)trans D 1, \begin{array}{ll} trans_{D_2} \circ \mathcal{E}(prog) \\ \;=\; trans_{D_2} \circ bind^{\mathcal{E}}\big( D_1 \xrightarrow{ prog } D_2 \xrightarrow{ ret^{\mathcal{E}}_D } \mathcal{E}(D_2) \big) \\ \;=\; bind^{\mathcal{E}'}\big( D_1 \xrightarrow{ prog } D_2 \xrightarrow{ ret^{\mathcal{E}}_D } \mathcal{E}(D_2) \xrightarrow{ trans_{D_2} } \mathcal{E}'(D_2) \big) \circ trans_{D_1} \\ \;=\; bind^{\mathcal{E}'}\big( D_1 \xrightarrow{ prog } D_2 \xrightarrow{ ret^{\mathcal{E}'}_D } \mathcal{E}'(D_2) \big) \circ trans_{D_1} \\ \;=\; \mathcal{E}'(prog) \circ trans_{D_1} \mathrlap{\,,} \end{array}

where we used, in order of appearance: (6), (3), (4) and finally (6) again.

Remark

(monad transformations act covariantly on Kleisli categories)
The conditions (2) and (3) equivalently say that the monad transformation transtrans (1) induces a functor between the respective Kleisli categories

As shown, this respects the free-module functors

because the following pasting diagram commutes (the left square by (2), the right square by naturality, see above):

Since it is evident that composite monad transformations give composite such functors, this means that assigning Kleisli categories to monads on C\mathbf{C} extends to a functor of the form:

This is probably the functor alluded to in Linton 1969, Lem. 10.2.

References

Original discussion:

  • David A. Espinosa, §3.2 in: Building Interpreters by Transforming Stratified Monads (1994) [pdf, pdf]

  • David A. Espinosa, §2.6 in: Semantic Lego, PhD thesis, Columbia University (1995) [pdf, pdf, slides:pdf, pdf]

  • Sheng Liang, Paul Hudak, Mark Jones, Monad transformers and modular interpreters, POPL ‘95 (1995) 333–343 [doi:10.1145/199448.199528]

  • Tom Schrijvers, Maciej Piróg, Nicolas Wu, Mauro Jaskelioff: Monad transformers and modular algebraic effects: what binds them together, in: Haskell 2019: Proceedings of the 12th ACM SIGPLAN International Symposium on Haskell (2019) 98–113 [doi:10.1145/3331545.3342595]

Textbook account:

See also:

Last revised on July 18, 2024 at 16:19:09. See the history of this page for a list of all contributions to it.