Monad transformer

From Wikipedia, the free encyclopedia
Jump to: navigation, search

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)


The option monad transformer[edit]

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 \rarr \mathrm{M} \left( A^{?} \right) = a \mapsto \mathrm{return} (\mathrm{Just}\,a)
  • \mathrm{bind}: \mathrm{M} \left( A^{?} \right) \rarr \left( A \rarr \mathrm{M} \left( B^{?} \right) \right) \rarr \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) \rarr \mathrm{M} \left( A^{?} \right) = m \mapsto \mathrm{bind} \, m \, (a \mapsto \mathrm{return} (\mathrm{Just} \, a))

The exception monad transformer[edit]

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 \rarr \mathrm{M} (A + E) = a \mapsto \mathrm{return} (\mathrm{value}\,a)
  • \mathrm{bind}: \mathrm{M} (A + E) \rarr (A \rarr \mathrm{M} (B + E)) \rarr \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 \rarr \mathrm{M} (A + E) = m \mapsto \mathrm{bind} \, m \, (a \mapsto \mathrm{return} (\mathrm{value} \, a))

The reader monad transformer[edit]

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

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

The state monad transformer[edit]

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

  • \mathrm{return}: A \rarr S \rarr \mathrm{M} (A \times S) = a \mapsto s \mapsto \mathrm{return} \, (a, s)
  • \mathrm{bind}: (S \rarr \mathrm{M}(A \times S)) \rarr (A \rarr S \rarr \mathrm{M}(B \times S)) \rarr S \rarr \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 \rarr S \rarr \mathrm{M}(A \times S) = m \mapsto s \mapsto \mathrm{bind} \, m \, (a \mapsto \mathrm{return} \, (a, s))

The writer monad transformer[edit]

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

  • \mathrm{return}: A \rarr \mathrm{M} (W \times A) = a \mapsto \mathrm{return} \, (\varepsilon, a)
  • \mathrm{bind}: \mathrm{M}(W \times A) \rarr (A \rarr \mathrm{M}(W \times B)) \rarr \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 \rarr \mathrm{M}(W \times A) = m \mapsto \mathrm{bind} \, m \, (a \mapsto \mathrm{return} \, (\varepsilon, a))

The continuation monad transformer[edit]

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

  • \mathrm{return} \colon A \rarr \left( A \rarr \mathrm{M} \, R \right) \rarr \mathrm{M} \, R = a \mapsto k \mapsto k \, a
  • \mathrm{bind} \colon \left( \left( A \rarr \mathrm{M} \, R \right) \rarr \mathrm{M} \, R \right) \rarr \left( A \rarr \left( B \rarr \mathrm{M} \, R \right) \rarr \mathrm{M} \, R \right) \rarr \left( B \rarr \mathrm{M} \, R \right) \rarr \mathrm{M} \, R= c \mapsto f \mapsto k \mapsto c \, \left( a \mapsto f \, a \, k \right)
  • \mathrm{lift}: \mathrm{M} \, A \rarr (A \rarr \mathrm{M} \, R) \rarr \mathrm{M} \, R = \mathrm{bind}

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[edit]


  1. ^ Liang, Sheng; Hudak, Paul; Jones, Mark (1995). "Monad transformers and modular interpreters" (PDF). Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY: ACM. pp. 333–343. doi:10.1145/199448.199528. 

External links[edit]

  • [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