Monad transformer

Template:One source In functional programming, a monad transformer is a type constructor which takes a monad as an argument and returns a monad as a result.

Monad transformers can be used to compose features encapsulated by monads – such as state, exception handling, and I/O – in a modular way. Typically, a monad transformer is created by generalising an existing monad; applying the resulting monad transformer to the identity monad yields a monad which is equivalent to the original monad (ignoring any necessary boxing and unboxing).

Definition

A monad transformer consists of:

1. A type constructor t of kind (* -> *) -> * -> *
2. Monad operations return and bind (or an equivalent formulation) for all t m where m is a monad, satisfying the monad laws
3. An additional operation, lift :: m a -> t m a, satisfying the following laws: (the notation `bind` below indicates infix application):
   1. lift . return = return
   2. lift (m `bind` k) = (lift m) `bind` (lift . k)

Examples

The option monad transformer

Given any monad $\mathrm{M}A$, the option monad transformer $\mathrm{M}\left(A^{?}\right)$ (where $A^{?}$ denotes the option type) is defined by:

$\begin{array}{cc}\mathrm{r}\mathrm{e}\mathrm{t}\mathrm{u}\mathrm{r}\mathrm{n}:& A\to \mathrm{M}\left(A^{?}\right)\\ & a\mapsto \mathrm{r}\mathrm{e}\mathrm{t}\mathrm{u}\mathrm{r}\mathrm{n}(\mathrm{J}\mathrm{u}\mathrm{s}\mathrm{t}a)\\ \mathrm{b}\mathrm{i}\mathrm{n}\mathrm{d}:& \mathrm{M}\left(A^{?}\right)\to (A\to \mathrm{M}\left(B^{?}\right))\to \mathrm{M}\left(B^{?}\right)\\ & m\mapsto f\mapsto \mathrm{b}\mathrm{i}\mathrm{n}\mathrm{d}m(a\mapsto \{\begin{array}{cc}\text{return Nothing}& \text{if }a=\mathrm{N}\mathrm{o}\mathrm{t}\mathrm{h}\mathrm{i}\mathrm{n}\mathrm{g}\\ f{a}^{\prime }& \text{if }a=\mathrm{J}\mathrm{u}\mathrm{s}\mathrm{t}{a}^{\prime }\end{array})\\ \mathrm{l}\mathrm{i}\mathrm{f}\mathrm{t}:& \mathrm{M}(A)\to \mathrm{M}\left(A^{?}\right)\\ & m\mapsto \mathrm{b}\mathrm{i}\mathrm{n}\mathrm{d}m(a\mapsto \mathrm{r}\mathrm{e}\mathrm{t}\mathrm{u}\mathrm{r}\mathrm{n}(\mathrm{J}\mathrm{u}\mathrm{s}\mathrm{t}a))\end{array}$

The exception monad transformer

Given any monad $\mathrm{M}A$, the exception monad transformer $\mathrm{M}(A+E)$ (where Template:Mvar is the type of exceptions) is defined by:

$\begin{array}{cc}\mathrm{r}\mathrm{e}\mathrm{t}\mathrm{u}\mathrm{r}\mathrm{n}:& A\to \mathrm{M}(A+E)\\ & a\mapsto \mathrm{r}\mathrm{e}\mathrm{t}\mathrm{u}\mathrm{r}\mathrm{n}(\mathrm{v}\mathrm{a}\mathrm{l}\mathrm{u}\mathrm{e}a)\\ \mathrm{b}\mathrm{i}\mathrm{n}\mathrm{d}:& \mathrm{M}(A+E)\to (A\to \mathrm{M}(B+E))\to \mathrm{M}(B+E)\\ & m\mapsto f\mapsto \mathrm{b}\mathrm{i}\mathrm{n}\mathrm{d}m(a\mapsto \{\begin{array}{cc}\text{return err }e& \text{if }a=\mathrm{e}\mathrm{r}\mathrm{r}e\\ f{a}^{\prime }& \text{if }a=\mathrm{v}\mathrm{a}\mathrm{l}\mathrm{u}\mathrm{e}{a}^{\prime }\end{array})\\ \mathrm{l}\mathrm{i}\mathrm{f}\mathrm{t}:& \mathrm{M}A\to \mathrm{M}(A+E)\\ & m\mapsto \mathrm{b}\mathrm{i}\mathrm{n}\mathrm{d}m(a\mapsto \mathrm{r}\mathrm{e}\mathrm{t}\mathrm{u}\mathrm{r}\mathrm{n}(\mathrm{v}\mathrm{a}\mathrm{l}\mathrm{u}\mathrm{e}a))\end{array}$

The reader monad transformer

Given any monad $\mathrm{M}A$, the reader monad transformer $E\to \mathrm{M}A$ (where Template:Mvar is the environment type) is defined by:

$\begin{array}{cc}\mathrm{r}\mathrm{e}\mathrm{t}\mathrm{u}\mathrm{r}\mathrm{n}:& A\to E\to \mathrm{M}A\\ & a\mapsto e\mapsto \mathrm{r}\mathrm{e}\mathrm{t}\mathrm{u}\mathrm{r}\mathrm{n}a\\ \mathrm{b}\mathrm{i}\mathrm{n}\mathrm{d}:& (E\to \mathrm{M}A)\to (A\to E\to \mathrm{M}B)\to E\to \mathrm{M}B\\ & m\mapsto k\mapsto e\mapsto \mathrm{b}\mathrm{i}\mathrm{n}\mathrm{d}(me)(a\mapsto kae)\\ \mathrm{l}\mathrm{i}\mathrm{f}\mathrm{t}:& \mathrm{M}A\to E\to \mathrm{M}A\\ & a\mapsto e\mapsto a\end{array}$

The state monad transformer

Given any monad $\mathrm{M}A$, the state monad transformer $S\to \mathrm{M}(A\times S)$ (where Template:Mvar is the state type) is defined by:

$\begin{array}{cc}\mathrm{r}\mathrm{e}\mathrm{t}\mathrm{u}\mathrm{r}\mathrm{n}:& A\to S\to \mathrm{M}(A\times S)\\ & a\mapsto s\mapsto \mathrm{r}\mathrm{e}\mathrm{t}\mathrm{u}\mathrm{r}\mathrm{n}(a,s)\\ \mathrm{b}\mathrm{i}\mathrm{n}\mathrm{d}:& (S\to \mathrm{M}(A\times S))\to (A\to S\to \mathrm{M}(B\times S))\to S\to \mathrm{M}(B\times S)\\ & m\mapsto k\mapsto s\mapsto \mathrm{b}\mathrm{i}\mathrm{n}\mathrm{d}(ms)((a,s^{\prime })\mapsto ka{s}^{\prime })\\ \mathrm{l}\mathrm{i}\mathrm{f}\mathrm{t}:& \mathrm{M}A\to S\to \mathrm{M}(A\times S)\\ & m\mapsto s\mapsto \mathrm{b}\mathrm{i}\mathrm{n}\mathrm{d}m(a\mapsto \mathrm{r}\mathrm{e}\mathrm{t}\mathrm{u}\mathrm{r}\mathrm{n}(a,s))\end{array}$

The writer monad transformer

Given any monad $\mathrm{M}A$, the writer monad transformer $\mathrm{M}(W\times A)$ (where Template:Mvar is endowed with a monoid operation Template:Math with identity element $\epsilon$) is defined by:

$\begin{array}{cc}\mathrm{r}\mathrm{e}\mathrm{t}\mathrm{u}\mathrm{r}\mathrm{n}:& A\to \mathrm{M}(W\times A)\\ & a\mapsto \mathrm{r}\mathrm{e}\mathrm{t}\mathrm{u}\mathrm{r}\mathrm{n}(\epsilon ,a)\\ \mathrm{b}\mathrm{i}\mathrm{n}\mathrm{d}:& \mathrm{M}(W\times A)\to (A\to \mathrm{M}(W\times B))\to \mathrm{M}(W\times B)\\ & m\mapsto f\mapsto \mathrm{b}\mathrm{i}\mathrm{n}\mathrm{d}m((w,a)\mapsto \mathrm{b}\mathrm{i}\mathrm{n}\mathrm{d}(fa)((w^{\prime },b)\mapsto \mathrm{r}\mathrm{e}\mathrm{t}\mathrm{u}\mathrm{r}\mathrm{n}(w\ast w^{\prime },b)))\\ \mathrm{l}\mathrm{i}\mathrm{f}\mathrm{t}:& \mathrm{M}A\to \mathrm{M}(W\times A)\\ & m\mapsto \mathrm{b}\mathrm{i}\mathrm{n}\mathrm{d}m(a\mapsto \mathrm{r}\mathrm{e}\mathrm{t}\mathrm{u}\mathrm{r}\mathrm{n}(\epsilon ,a))\end{array}$

The continuation monad transformer

Given any monad $\mathrm{M}A$, the continuation monad transformer maps an arbitrary type Template:Mvar into functions of type $(A\to \mathrm{M}R)\to \mathrm{M}R$, where Template:Mvar is the result type of the continuation. It is defined by:

$\begin{array}{cc}\mathrm{r}\mathrm{e}\mathrm{t}\mathrm{u}\mathrm{r}\mathrm{n}:& A\to (A\to \mathrm{M}R)\to \mathrm{M}R\\ & a\mapsto k\mapsto ka\\ \mathrm{b}\mathrm{i}\mathrm{n}\mathrm{d}:& ((A\to \mathrm{M}R)\to \mathrm{M}R)\to (A\to (B\to \mathrm{M}R)\to \mathrm{M}R)\to (B\to \mathrm{M}R)\to \mathrm{M}R\\ & c\mapsto f\mapsto k\mapsto c(a\mapsto fak)\\ \mathrm{l}\mathrm{i}\mathrm{f}\mathrm{t}:& \mathrm{M}A\to (A\to \mathrm{M}R)\to \mathrm{M}R\\ & \mathrm{b}\mathrm{i}\mathrm{n}\mathrm{d}\end{array}$

Note that monad transformations are usually not commutative: for instance, applying the state transformer to the option monad yields a type $S\to {(A\times S)}^{?}$ (a computation which may fail and yield no final state), whereas the converse transformation has type $S\to (A^{?}\times S)$ (a computation which yields a final state and an optional return value).

See also

• Monads in functional programming

External links

• A blog post briefly reviewing some of the literature on monad transformers and related concepts, with a focus on categorical-theoretic treatment