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).

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:^[1] (the notation `bind` below indicates infix application):
   1. lift . return = return
   2. lift (m `bind` k) = (lift m) `bind` (lift . k)

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

${\displaystyle {\begin{array}{ll}\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)\\&m\mapsto f\mapsto \mathrm {bind} ,円m,円\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,円(a\mapsto \mathrm {return} (\mathrm {Just} ,円a))\end{array}}}${\displaystyle {\begin{array}{ll}\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)\\&m\mapsto f\mapsto \mathrm {bind} ,円m,円\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,円(a\mapsto \mathrm {return} (\mathrm {Just} ,円a))\end{array}}}

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

${\displaystyle {\begin{array}{ll}\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)\\&m\mapsto f\mapsto \mathrm {bind} ,円m,円\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,円(a\mapsto \mathrm {return} (\mathrm {value} ,円a))\\\end{array}}}${\displaystyle {\begin{array}{ll}\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)\\&m\mapsto f\mapsto \mathrm {bind} ,円m,円\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,円(a\mapsto \mathrm {return} (\mathrm {value} ,円a))\\\end{array}}}

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

${\displaystyle {\begin{array}{ll}\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\\\end{array}}}${\displaystyle {\begin{array}{ll}\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\\\end{array}}}

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

${\displaystyle {\begin{array}{ll}\mathrm {return} :&A\rightarrow S\rightarrow \mathrm {M} (A\times S)\\&a\mapsto s\mapsto \mathrm {return} ,円(a,s)\\\mathrm {bind} :&(S\rightarrow \mathrm {M} (A\times S))\rightarrow (A\rightarrow S\rightarrow \mathrm {M} (B\times S))\rightarrow S\rightarrow \mathrm {M} (B\times S)\\&m\mapsto k\mapsto s\mapsto \mathrm {bind} ,円(m,円s),円((a,s')\mapsto k,円a,円s')\\\mathrm {lift} :&\mathrm {M} ,円A\rightarrow S\rightarrow \mathrm {M} (A\times S)\\&m\mapsto s\mapsto \mathrm {bind} ,円m,円(a\mapsto \mathrm {return} ,円(a,s))\end{array}}}${\displaystyle {\begin{array}{ll}\mathrm {return} :&A\rightarrow S\rightarrow \mathrm {M} (A\times S)\\&a\mapsto s\mapsto \mathrm {return} ,円(a,s)\\\mathrm {bind} :&(S\rightarrow \mathrm {M} (A\times S))\rightarrow (A\rightarrow S\rightarrow \mathrm {M} (B\times S))\rightarrow S\rightarrow \mathrm {M} (B\times S)\\&m\mapsto k\mapsto s\mapsto \mathrm {bind} ,円(m,円s),円((a,s')\mapsto k,円a,円s')\\\mathrm {lift} :&\mathrm {M} ,円A\rightarrow S\rightarrow \mathrm {M} (A\times S)\\&m\mapsto s\mapsto \mathrm {bind} ,円m,円(a\mapsto \mathrm {return} ,円(a,s))\end{array}}}

Given any monad ${\displaystyle \mathrm {M} ,円A}${\displaystyle \mathrm {M} ,円A}, the writer monad transformer ${\displaystyle \mathrm {M} (W\times A)}${\displaystyle \mathrm {M} (W\times A)} (where W is endowed with a monoid operation ∗ with identity element ${\displaystyle \varepsilon }${\displaystyle \varepsilon }) is defined by:

${\displaystyle {\begin{array}{ll}\mathrm {return} :&A\rightarrow \mathrm {M} (W\times A)\\&a\mapsto \mathrm {return} ,円(\varepsilon ,a)\\\mathrm {bind} :&\mathrm {M} (W\times A)\rightarrow (A\rightarrow \mathrm {M} (W\times B))\rightarrow \mathrm {M} (W\times B)\\&m\mapsto f\mapsto \mathrm {bind} ,円m,円((w,a)\mapsto \mathrm {bind} ,円(f,円a),円((w',b)\mapsto \mathrm {return} ,円(w*w',b)))\\\mathrm {lift} :&\mathrm {M} ,円A\rightarrow \mathrm {M} (W\times A)\\&m\mapsto \mathrm {bind} ,円m,円(a\mapsto \mathrm {return} ,円(\varepsilon ,a))\\\end{array}}}${\displaystyle {\begin{array}{ll}\mathrm {return} :&A\rightarrow \mathrm {M} (W\times A)\\&a\mapsto \mathrm {return} ,円(\varepsilon ,a)\\\mathrm {bind} :&\mathrm {M} (W\times A)\rightarrow (A\rightarrow \mathrm {M} (W\times B))\rightarrow \mathrm {M} (W\times B)\\&m\mapsto f\mapsto \mathrm {bind} ,円m,円((w,a)\mapsto \mathrm {bind} ,円(f,円a),円((w',b)\mapsto \mathrm {return} ,円(w*w',b)))\\\mathrm {lift} :&\mathrm {M} ,円A\rightarrow \mathrm {M} (W\times A)\\&m\mapsto \mathrm {bind} ,円m,円(a\mapsto \mathrm {return} ,円(\varepsilon ,a))\\\end{array}}}

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

${\displaystyle {\begin{array}{ll}\mathrm {return} \colon &A\rightarrow \left(A\rightarrow \mathrm {M} ,円R\right)\rightarrow \mathrm {M} ,円R\\&a\mapsto k\mapsto k,円a\\\mathrm {bind} \colon &\left(\left(A\rightarrow \mathrm {M} ,円R\right)\rightarrow \mathrm {M} ,円R\right)\rightarrow \left(A\rightarrow \left(B\rightarrow \mathrm {M} ,円R\right)\rightarrow \mathrm {M} ,円R\right)\rightarrow \left(B\rightarrow \mathrm {M} ,円R\right)\rightarrow \mathrm {M} ,円R\\&c\mapsto f\mapsto k\mapsto c,円\left(a\mapsto f,円a,円k\right)\\\mathrm {lift} \colon &\mathrm {M} ,円A\rightarrow (A\rightarrow \mathrm {M} ,円R)\rightarrow \mathrm {M} ,円R\\&\mathrm {bind} \end{array}}}${\displaystyle {\begin{array}{ll}\mathrm {return} \colon &A\rightarrow \left(A\rightarrow \mathrm {M} ,円R\right)\rightarrow \mathrm {M} ,円R\\&a\mapsto k\mapsto k,円a\\\mathrm {bind} \colon &\left(\left(A\rightarrow \mathrm {M} ,円R\right)\rightarrow \mathrm {M} ,円R\right)\rightarrow \left(A\rightarrow \left(B\rightarrow \mathrm {M} ,円R\right)\rightarrow \mathrm {M} ,円R\right)\rightarrow \left(B\rightarrow \mathrm {M} ,円R\right)\rightarrow \mathrm {M} ,円R\\&c\mapsto f\mapsto k\mapsto c,円\left(a\mapsto f,円a,円k\right)\\\mathrm {lift} \colon &\mathrm {M} ,円A\rightarrow (A\rightarrow \mathrm {M} ,円R)\rightarrow \mathrm {M} ,円R\\&\mathrm {bind} \end{array}}}

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

• Monads in functional programming

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

• Functional programming

• Articles needing additional references from November 2023
• All articles needing additional references
• Articles to be expanded from May 2008
• All articles to be expanded