Content deleted Content added
No edit summary |
m reformatted math environments to get rid of page-breaking expressions |
||
| (7 intermediate revisions by 6 users not shown) | |||
Line 1:
{{One source|date=November 2023}}
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.
Line 6 ⟶ 7:
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
Line 12 ⟶ 13:
| last = Liang |author2=Hudak, Paul |author3=Jones, Mark
| title = Monad transformers and modular interpreters
|
| pages =
| publisher = ACM
| year = 1995
Line 20 ⟶ 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>
Line 28 ⟶ 30:
===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}
& 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) & m \mapsto \mathrm{bind} \, m \, (a \mapsto \mathrm{return} (\mathrm{Just} \, a)) \end{array}</math> ===The exception monad transformer===
Given any monad <math>\mathrm{M} \, A</math>, the exception monad transformer <math>\mathrm{M} (A + E)</math> (where
\mathrm{return}: & A \rarr \mathrm{M} (A + E) & a \mapsto \mathrm{return} (\mathrm{value}\,a) & 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) & m \mapsto \mathrm{bind} \, m \, (a \mapsto \mathrm{return} (\mathrm{value} \, a)) \end{array}</math>
===The reader monad transformer===
Given any monad <math>\mathrm{M} \, A</math>, the reader monad transformer <math>E \rarr \mathrm{M}\,A</math> (where
\mathrm{return}: & A \rarr E \rarr \mathrm{M} \, A & a \mapsto e \mapsto \mathrm{return} \, a & m \mapsto k \mapsto e \mapsto \mathrm{bind} \, (m \, e) \,( a \mapsto k \, a \, e) & a \mapsto e \mapsto a \end{array}</math>
===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>\begin{array}{ll}
& 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') & m \mapsto s \mapsto \mathrm{bind} \, m \, (a \mapsto \mathrm{return} \, (a, s)) \end{array}</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>\begin{array}{ll}
& 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))) & m \mapsto \mathrm{bind} \, m \, (a \mapsto \mathrm{return} \, (\varepsilon, a)) \end{array}</math>
===The continuation monad transformer===
Given any monad <math>\mathrm{M} \, A</math>, the continuation monad transformer maps an arbitrary type
:<math>\begin{array}{ll}
& 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{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).
| |||