Monad transformer: Difference between revisions

Revision as of 17:25, 15 January 2013

Latest revision as of 11:37, 16 March 2025

(13 intermediate revisions by 10 users not shown)

Line 1:

{{One source|date=November 2023}}

{{Wikibooks|Haskell|Monad transformers}}

In [[functional programming]], a '''monad transformer''' is a type constructor which takes a [[monads in functional programming|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 <code>t</code> of [[kind (type theory)|kind]] <code>(* -> *) -> * -> *</code>

# Monad operations <code>return</code> and <code>bind</code> (or an equivalent formulation) for all <code>t m</code> where <code>m</code> is a monad, satisfying the [[Monad_(functional_programming)#Monad_laws|monad laws]]

# An additional operation, <code>lift :: m a -> t m a</code>, satisfying the following laws:<ref name="modular-interpreters">

{{cite conference

| first = Sheng

| last = Liang |author2=Hudak, Paul |author3=Jones, Mark

| coauthors = Hudak, Paul; Jones, Mark

| title = Monad transformers and modular interpreters

| booktitlebook-title = Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

| pages = 333&ndash;343333–343

| publisher = ACM

| year = 1995

Line 23 ⟶ 21:

| format = PDF

| doi = 10.1145/199448.199528

| doi-access = free

}}

</ref> (the notation <code>`bind`</code> below indicates infix application):

## <code>lift . return = return</code>

## <code>lift (m `bind` k) = (lift m) `bind` (lift . k)</code>

== Examples ==

=== The option monad transformer ===

Given any monad <math>\mathrm{M} \, A</math>, the option monad transformer <math>\mathrm{M} \left( A^{?} \right)</math> (where <math>A^{?}</math> denotes the [[option type]]) is defined by:

:<math>\begin{array}{ll}

*<math>\mathrm{return}: A \rarr \mathrm{M} \left( A^{?} \right) = a \mapsto \mathrm{return} (\mathrm{Just}\,a)</math>

*<math>\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)</math> \\

*<math>\mathrm{lift}: & \mathrm{M} (A) \rarr \mathrm{M} \left( A^{?} \right) =\\
& m \mapsto \mathrm{bind} \, m \, (a \mapsto \mathrm{return} (\mathrm{Just} \, a)) \end{array}</math>

=== The readerexception monad transformer ===

Given any monad <math>\mathrm{M} \, A</math>, the stateexception monad transformer <math>S \rarr \mathrm{M} (A \times+ SE)</math> (where <math>S</math>{{mvar|E}} is the state type of exceptions) is defined by:

:<math>\begin{array}{ll}

*<math>\mathrm{return}: & A \rarr \mathrm{M} (A + E) = a \mapsto \mathrm{return} (\mathrm{value}\,a)</math>

& a \mapsto \mathrm{return} (\mathrm{value}\,a) \\

*<math>\mathrm{liftbind}: & \mathrm{M} \, (A + E) \rarr (A \rarr \mathrm{M} \,(B R+ E)) \rarr \mathrm{M} \,(B R =+ E)\\mathrm{bind}</math>

& 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) \\

*<math>\mathrm{lift}: & \mathrm{M} \, A \rarr E \rarr \mathrm{M} \, (A = a+ E)\mapsto e \mapsto a</math>

*<math>\mathrm{return}:& Am \rarrmapsto \mathrm{Mbind} \left(, A^{?}m \right) =, (a \mapsto \mathrm{return} (\mathrm{Justvalue} \, a)</math>) \\

\end{array}</math>

=== The statereader monad transformer ===

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

:<math>\begin{array}{ll}

*<math>\mathrm{return}: & A \rarr E \rarr \mathrm{M} \, A = a \mapsto e \mapsto \mathrm{return} \, a</math>

& a \mapsto e \mapsto \mathrm{return} \, a \\

*<math>\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)</math>

& 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 \\

\end{array}</math>

=== The writerstate monad transformer ===

Given any monad <math>\mathrm{M} \, A</math>, the writerstate monad transformer <math>S \rarr \mathrm{M}(WA \times AS)</math> (where <math>W</math>{{mvar|S}} is endowedthe withstate a [[monoid]] operation <math>*</math> with identity element <math>\varepsilon</math>type) is defined by:

:<math>\begin{array}{ll}

*<math>\mathrm{return}: & A \rarr S \rarr \mathrm{M} (A \times S) = a \mapsto s \mapsto \mathrm{return} \, (a, s)</math>

& a \mapsto s \mapsto \mathrm{return} \, (a, s) \\

*<math>\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')</math>

& m \mapsto k \mapsto s \mapsto \mathrm{bind} \, (m \, s) \,((a, s') \mapsto k \, a \, s') \\

*<math>\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))</math>

*<math>& m \mathrm{return}:mapsto As \rarrmapsto \mathrm{Mbind} (W \times, A)m =\, (a \mapsto \mathrm{return} \, (\varepsilona, as)) \end{array}</math>

=== The continuationwriter monad transformer ===

Given any monad <math>\mathrm{M} \, A</math>, the writer monad transformer <math>\mathrm{M}(W \times A)</math> (where {{mvar|W}} is endowed with a [[monoid]] operation {{math|&lowast;}} with identity element <math>\varepsilon</math>) is defined by:

:<math>\begin{array}{ll}

\mathrm{return}: & A \rarr \mathrm{M} (W \times A)\\

& a \mapsto \mathrm{return} \, (\varepsilon, a) \\

*<math>\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)))</math>

*<math>\mathrm{lift}:& \mathrm{M}m \,mapsto Af \rarrmapsto \mathrm{Mbind}(W \times, A)m =\,((w, ma) \mapsto \mathrm{bind} \, m(f \, (a) \, ((w', b) \mapsto \mathrm{return} \, (\varepsilonw * w', ab))</math>) \\

\mathrm{lift}: & \mathrm{M} \, A \rarr \mathrm{M}(W \times A)\\

*<math>\mathrm{lift}: \mathrm{M} \, A \rarr \mathrm{M} (A + E) =& m \mapsto \mathrm{bind} \, m \, (a \mapsto \mathrm{return} (\mathrm{value}, (\varepsilon, a))</math> \\

\end{array}</math>

=== The exceptioncontinuation monad transformer ===

Given any monad <math>\mathrm{M} \, A</math>, the exceptioncontinuation monad transformer maps an arbitrary type {{mvar|R}} into functions of type <math>(A \rarr \mathrm{M} (A\, + ER) \rarr \mathrm{M} \, R</math>, (where <math>E</math>{{mvar|R}} is the result type of exceptions)the continuation. It is defined by:

:<math>\begin{array}{ll}

*<math>\mathrm{return}: A \rarr \mathrm{M} (A + E) = a \mapsto \mathrm{return} (\mathrm{value}\,a)</math>

*<math>\mathrm{bindreturn}: \mathrm{M}colon (A& + E) \rarr (A \rarr \mathrm{M} left(B + E))A \rarr \mathrm{M} (B + E) = m \mapsto f \mapsto \mathrm{bind} \, mR \,\left( aright) \mapsto \begin{cases} \mbox{return err } e & \mbox{if } a =rarr \mathrm{errM} \, eR\\ f \, a' & \mbox{if } a = \mathrm{value} \, a' \end{cases} \right)</math>

& a \mapsto k \mapsto k \, a \\

*<math>\mathrm{lift}: \mathrm{M} \, A \rarr \mathrm{M} (A + E) = m \mapsto \mathrm{bind} \, m \, (a \mapsto \mathrm{return} (\mathrm{value} \, a))</math>

*<math>\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</math><math>= c \mapsto f \mapsto k \mapsto c \, \left( a \mapsto f \, a \, k \right)</math>

& c \mapsto f \mapsto k \mapsto c \, \left( a \mapsto f \, a \, k \right) \\

*<math>\mathrm{returnlift} \colon & \mathrm{M} \, A \rarr \left( A \rarr \mathrm{M} \, R \right) \rarr \mathrm{M} \, R = a \mapsto k \mapsto k \, a</math>

& \mathrm{bind}

\end{array}</math>

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

== See also ==

=== The reader monad transformer ===

* [[Monads in functional programming]]

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

*<math>\mathrm{return}: A \rarr E \rarr \mathrm{M} \, A = a \mapsto e \mapsto \mathrm{return} \, a</math>

*<math>\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)</math>

*<math>\mathrm{lift}: \mathrm{M} \, A \rarr E \rarr \mathrm{M} \, A = a \mapsto e \mapsto a</math>

== References ==

=== The state monad transformer ===

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

*<math>\mathrm{return}: A \rarr S \rarr \mathrm{M} (A \times S) = a \mapsto s \mapsto \mathrm{return} \, (a, s)</math>

*<math>\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')</math>

*<math>\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))</math>

=== The writer monad transformer ===

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

*<math>\mathrm{return}: A \rarr \mathrm{M} (W \times A) = a \mapsto \mathrm{return} \, (\varepsilon, a)</math>

*<math>\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)))</math>

*<math>\mathrm{lift}: \mathrm{M} \, A \rarr \mathrm{M}(W \times A) = m \mapsto \mathrm{bind} \, m \, (a \mapsto \mathrm{return} \, (\varepsilon, a))</math>

=== The continuation monad transformer ===

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

*<math>\mathrm{return} \colon A \rarr \left( A \rarr \mathrm{M} \, R \right) \rarr \mathrm{M} \, R = a \mapsto k \mapsto k \, a</math>

*<math>\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</math><math>= c \mapsto f \mapsto k \mapsto c \, \left( a \mapsto f \, a \, k \right)</math>

*<math>\mathrm{lift}: \mathrm{M} \, A \rarr (A \rarr \mathrm{M} \, R) \rarr \mathrm{M} \, R = \mathrm{bind}</math>

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

== See also ==

* [[Monads in functional programming]]

* [[Natural transformation]] - a related concept in [[category theory]]

== References ==

{{Reflist}}

== External links ==

{{Wikibooks|Haskell|Monad transformers}}

* [http://conway.rutgers.edu/~ccshan/wiki/blog/posts/Monad_transformers/] - aA 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}}