Monad transformer: Difference between revisions

Content deleted Content added
No edit summary
Line 51:
*<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) = am \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>
 
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]]