Monad transformer

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:

• $\mathrm {return} :A\rightarrow \mathrm {M} \left(A^{?}\right)=a\mapsto \mathrm {return} (\mathrm {Just} \,a)$
• $\mathrm {bind} :\mathrm {M} \left(A^{?}\right)\rightarrow \left(A\rightarrow \mathrm {M} \left(B^{?}\right)\right)\rightarrow \mathrm {M} \left(B^{?}\right)=a\mapsto f\mapsto \mathrm {bind} \,a\,\left(a'\mapsto {\begin{cases}{\mbox{return Nothing}}&{\mbox{if }}a'=\mathrm {Nothing} \\f\,a''&{\mbox{if }}a'=\mathrm {Just} \,a''\end{cases}}\right)$
• $\mathrm {lift} :\mathrm {M} (A)\rightarrow \mathrm {M} \left(A^{?}\right)=m\mapsto \mathrm {bind} \,m\,(x\mapsto \mathrm {return} (\mathrm {Just} \,x))$

The exception monad transformer

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

• $\mathrm {return} :A\rightarrow \mathrm {M} (A+E)=a\mapsto \mathrm {return} (\mathrm {value} \,a)$
• $\mathrm {bind} :\mathrm {M} (A+E)\rightarrow (A\rightarrow \mathrm {M} (B+E))\rightarrow \mathrm {M} (B+E)=a\mapsto f\mapsto \mathrm {bind} \,a\,\left(a'\mapsto {\begin{cases}{\mbox{return err }}e&{\mbox{if }}a'=\mathrm {err} \,e\\f\,a''&{\mbox{if }}a'=\mathrm {value} \,a''\end{cases}}\right)$
• $\mathrm {lift} :\mathrm {M} \,A\rightarrow \mathrm {M} (A+E)=m\mapsto \mathrm {bind} \,m\,(x\mapsto \mathrm {return} (\mathrm {value} \,x))$

The reader monad transformer

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

• $\mathrm {return} :A\rightarrow E\rightarrow \mathrm {M} \,A=a\mapsto e\mapsto \mathrm {return} \,a$
• $\mathrm {bind} :(E\rightarrow \mathrm {M} \,A)\rightarrow (A\rightarrow E\rightarrow \mathrm {M} \,B)\rightarrow E\rightarrow \mathrm {M} \,B=m\mapsto k\mapsto e\mapsto \mathrm {bind} \,(m\,e)\,(a\mapsto k\,a\,e)$
• $\mathrm {lift} :\mathrm {M} \,A\rightarrow E\rightarrow \mathrm {M} \,A=a\mapsto e\mapsto a$

See also

• Monads in functional programming
• Natural transformation - a related concept in category theory

External links

• [1] - a highly technical blog post briefly reviewing some of the literature on monad transformers and related concepts, with a focus on categorical-theoretic treatment