Nottingham FP Lab Blog

Monad Transformers

by Mauro Jaskelioff on February 4, 2008.
Tagged as: Lunches.

Monad transformers were introduced as a programming technique many years ago, but we are still not sure what mathematical structure they are. For example, we still don’t know if every monad has an associated monad transformer, or even if every monad should have just one associated monad transformer.

John Power argues that monad transformers should come before monads since every M-monad transformer gives raise to a monad M by applying it to the identity monad. One structure that comes before monads is adjunctions: every adjunction $\langle F,G,\eta,\varepsilon\rangle\colon\mathbb{C}\rightharpoonup\mathbb{D}$ gives rise to a monad $\langle FG, \eta, G\varepsilon F\rangle$ . Also, every monad can be split into an adjunction. There are usually many adjunctions a monad can be split into, but there are two canonical ones: the Kleisli and the Eilenberg-Moore (which are the initial and the final splittings in some sense).

Now, given an adjunction $\langle F,G,\eta,\varepsilon\rangle\colon\mathbb{C}\rightharpoonup\mathbb{D}$ and a monad $\langle M, \eta^{M}, \mu^{M}\rangle$ on $\mathbb{D}$ , we can choose any adjunction giving rise to it and use adjoint composition to obtain a monad $\langle GMF,G\eta^{M}F\cdot\eta,G\mu^{M}F\cdot GM\varepsilon MF\rangle$ on $\mathbb{C}$ .

So, a monad transformer for a monad $T$ might be explained by a choice of an adjunction $\langle F,G,\eta,\varepsilon\rangle\colon\mathbb{C}\rightharpoonup\mathbb{D}$ splitting $T$ and a lifting of monads in $\mathbb{C}$ to monads in $\mathbb{D}$ .

If the choice of the adjunction is the Eilenberg-Moore one, then the lifting of $M$ is given by a distributive law of monads
$\lambda\colon TM\rightarrow MT$ , and the obtained monad is $\langle MT,\eta^{M}\cdot\eta^{T},\mu^{T}\cdot \mu^{M}\cdot M\lambda_{T}\rangle$ . For example, this explains the standard Haskell monad transformers for Maybe and Writer.

If the choice of the adjunction is the Kleisli one, then the lifting of $M$ is given by a distributive law of monads
$\lambda\colon MT\rightarrow TM$ , and the obtained monad is $\langle TM,\eta^{T}\cdot\eta^{M},\mu^{M}\cdot \mu^{T}\cdot T\lambda_{M}\rangle$ . For example, this explains the standard Haskell monad transformers for Reader and Cont.

The State monad transformer is not explained by any of the canonical adjunctions splitting the monad, but by the currying/uncurrying adjunction characterizing exponentials:

$\langle S\times -,S\Rightarrow -,\eta^{S},\varepsilon^{S}\rangle\colon\mathbb{C}\rightharpoonup\mathbb{C}$

Note that here the lifting is trivial, as the category on the left and the right of the adjunction is the same.