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:
# A type constructor t of kind (* -> *) -> * -> *
# Monad operations return and bind (or an equivalent formulation) for all t m where m is a monad, satisfying the monad laws
# An additional operation, lift :: m a -> t m a, satisfying the following laws:

(the notation `bind` below indicates infix application):
## lift . return = return
## lift (m `bind` k) = (lift m) `bind` (lift . k)

Examples

The option monad transformer

Given any monad $\mathrm \, A$, the option monad transformer $\mathrm \left( A^ \right)$ (where $A^$ denotes the option type) is defined by:
:$\begin \mathrm: & A \rarr \mathrm \left( A^ \right) = a \mapsto \mathrm (\mathrm\,a) \\ \mathrm: & \mathrm \left( A^ \right) \rarr \left( A \rarr \mathrm \left( B^ \right) \right) \rarr \mathrm \left( B^ \right) = m \mapsto f \mapsto \mathrm \, m \, \left(a \mapsto \begin \mbox & \mbox a = \mathrm\\ f \, a' & \mbox a = \mathrm \, a' \end \right) \\ \mathrm: & \mathrm (A) \rarr \mathrm \left( A^ \right) = m \mapsto \mathrm \, m \, (a \mapsto \mathrm (\mathrm \, a)) \end$

The exception monad transformer

Given any monad $\mathrm \, A$, the exception monad transformer $\mathrm (A + E)$ (where is the type of exceptions) is defined by:
:$\begin \mathrm: & A \rarr \mathrm (A + E) = a \mapsto \mathrm (\mathrm\,a) \\ \mathrm: & \mathrm (A + E) \rarr (A \rarr \mathrm (B + E)) \rarr \mathrm (B + E) = m \mapsto f \mapsto \mathrm \, m \,\left( a \mapsto \begin \mbox e & \mbox a = \mathrm \, e\\ f \, a' & \mbox a = \mathrm \, a' \end \right) \\ \mathrm: & \mathrm \, A \rarr \mathrm (A + E) = m \mapsto \mathrm \, m \, (a \mapsto \mathrm (\mathrm \, a)) \\ \end$

The reader monad transformer

Given any monad $\mathrm \, A$, the reader monad transformer $E \rarr \mathrm\,A$ (where is the environment type) is defined by:
:$\begin \mathrm: & A \rarr E \rarr \mathrm \, A = a \mapsto e \mapsto \mathrm \, a \\ \mathrm: & (E \rarr \mathrm \, A) \rarr (A \rarr E \rarr \mathrm\,B) \rarr E \rarr \mathrm\,B = m \mapsto k \mapsto e \mapsto \mathrm \, (m \, e) \,( a \mapsto k \, a \, e) \\ \mathrm: & \mathrm \, A \rarr E \rarr \mathrm \, A = a \mapsto e \mapsto a \\ \end$

The state monad transformer

Given any monad $\mathrm \, A$, the state monad transformer $S \rarr \mathrm(A \times S)$ (where is the state type) is defined by:
:$\begin \mathrm: & A \rarr S \rarr \mathrm (A \times S) = a \mapsto s \mapsto \mathrm \, (a, s) \\ \mathrm: & (S \rarr \mathrm(A \times S)) \rarr (A \rarr S \rarr \mathrm(B \times S)) \rarr S \rarr \mathrm(B \times S) = m \mapsto k \mapsto s \mapsto \mathrm \, (m \, s) \,((a, s') \mapsto k \, a \, s') \\ \mathrm: & \mathrm \, A \rarr S \rarr \mathrm(A \times S) = m \mapsto s \mapsto \mathrm \, m \, (a \mapsto \mathrm \, (a, s)) \end$

The writer monad transformer

Given any monad $\mathrm \, A$, the writer monad transformer $\mathrm(W \times A)$ (where is endowed with a monoid operation with identity element $\varepsilon$) is defined by:
:$\begin \mathrm: & A \rarr \mathrm (W \times A) = a \mapsto \mathrm \, (\varepsilon, a) \\ \mathrm: & \mathrm(W \times A) \rarr (A \rarr \mathrm(W \times B)) \rarr \mathrm(W \times B) = m \mapsto f \mapsto \mathrm \, m \,((w, a) \mapsto \mathrm \, (f \, a) \, ((w', b) \mapsto \mathrm \, (w * w', b))) \\ \mathrm: & \mathrm \, A \rarr \mathrm(W \times A) = m \mapsto \mathrm \, m \, (a \mapsto \mathrm \, (\varepsilon, a)) \\ \end$

The continuation monad transformer

Given any monad $\mathrm \, A$, the continuation monad transformer maps an arbitrary type into functions of type $(A \rarr \mathrm \, R) \rarr \mathrm \, R$, where is the result type of the continuation. It is defined by:
:$\begin \mathrm \colon & A \rarr \left( A \rarr \mathrm \, R \right) \rarr \mathrm \, R = a \mapsto k \mapsto k \, a \\ \mathrm \colon & \left( \left( A \rarr \mathrm \, R \right) \rarr \mathrm \, R \right) \rarr \left( A \rarr \left( B \rarr \mathrm \, R \right) \rarr \mathrm \, R \right) \rarr \left( B \rarr \mathrm \, R \right) \rarr \mathrm \, R = c \mapsto f \mapsto k \mapsto c \, \left( a \mapsto f \, a \, k \right) \\ \mathrm \colon & \mathrm \, A \rarr (A \rarr \mathrm \, R) \rarr \mathrm \, R = \mathrm \end$
Note that monad transformations are usually not commutative: for instance, applying the state transformer to the option monad yields a type $S \rarr \left(A \times S \right)^$ (a computation which may fail and yield no final state), whereas the converse transformation has type $S \rarr \left(A^ \times S \right)$ (a computation which yields a final state and an optional return value).

See also

*Monads in functional programming

References

External links

A highly technical blog post briefly reviewing some of the literature on monad transformers and related concepts, with a focus on categorical-theoretic treatment
{{Expand section, date=May 2008

Functional programming