nLab monad transformer

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 $\mathcal{E}_{new}$ into any given one $\mathcal{E}$ by $\mathcal{E} \mapsto \mathcal{E}_{new} \circ \mathcal{E}$ via a universal distributive law.

Formally, a monad transformer on a given category $\mathbf{C}$ (of data types) is a pointed endofunctor on the category of monads $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_{\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_{(\text{-})}$” (1) — which they denote “$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 $\mathbf{C}$, a monad transformer between them is:

• a system of morphisms

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

which

1. preserves the return-operations, in that

   (2)$$trans \circ ret^{\mathcal{E}} \;=\; ret^{\mathcal{E}'} \,,$$

2. preserves the bind-operations, in that for $prog_{12}\,\colon\, D_1 \to \mathcal{E}(D_2)$ and $prog_{23}\,\colon\, D_2 \to \mathcal{E}(D_3)$

   we have

   (3)$$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 \,\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 \,\colon\, \mathcal{E} \to \mathcal{E}'$ of the underlying functors,

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

   (4)$$\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^{\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)$$\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^{\mathcal{E}}_{D} \;\equiv\; bind^{\mathcal{E}}\big( id_{\mathcal{E}(D)} \big) \,.$$

Now in one direction: Given a morphism of monads $trans \,\colon\, \mathcal{E} \to \mathcal{E}'$, then consider the pasting diagram of the above square with the naturality square of $trans$ 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_{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_{(\text{-})}$ (1) is necessarily natural. This is shown by the following sequence of equalities, for $prog \,\colon\, D_1 \to D_2$:

$$\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 $trans$ (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 $\mathbf{C}$ extends to a functor of the form:

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

Related concepts

• monad transformation

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:

• Sergei Winitzki, Section 14 of: The Science of Functional Programming – A tutorial, with examples in Scala (2022) [leanpub:sofp, github:sofp]

See also:

• Wikipedia, Monad transformer

• Haskell, Monad transformers

• hackage.haskell.org/package/transformers-0.5.6.2/docs/Control-Monad-Trans-Class.html

• Bryan O’Sullivan, Don Stewart, and John Goerzen, Monad transformers, Chapter 18 of Real World Haskell

• Mauro Jaskelioff, Eugenio Moggi, Monad Transformers as Monoid Transformers, Theoretical Computer Science 411 51–52 (2010) 4441-4466 [doi:10.1016/j.tcs.2010.09.011, pdf]

• Martin Hyland, John Power, The Category Theoretic Understanding of Universal Algebra: Lawvere Theories and Monads, Electronic Notes in Theoretical Computer Science (ENTCS) 172 (2007) 437-458 [pdf]

• Mauro Jaskelioff, Monatron: An Extensible Monad Transformer Library, in: Implementation and Application of Functional Languages. IFL 2008, Lecture Notes in Computer Science 5836 (2011) 233–248 [doi:10.1007/978-3-642-24452-0_13]

• Oleksandr Manzyuk, Calculating monad transformers with category theory (2012) [pdf]

• Maciej Piróg, Eilenberg–Moore Monoids and Backtracking Monad Transformers, EPTCS 207 (2016) 23-56 [ar, doi:10.4204/EPTCS.207.2&rbrack

• Chung-Chieh Shan, Monad transformers (2020) [blog post]