• Images
• Videos
• Documents
• Books
• Articles

Definition

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

Examples

The option monad transformer

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

r e t u r n : A → M ( A ? ) a ↦ r e t u r n ( J u s t a ) b i n d : M ( A ? ) → ( A → M ( B ? ) ) → M ( B ? ) m ↦ f ↦ b i n d m ( a ↦ { return Nothing if  a = N o t h i n g f a ′ if  a = J u s t a ′ ) l i f t : M ( A ) → M ( A ? ) m ↦ b i n d m ( a ↦ r e t u r n ( J u s t a ) ) {\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}}}

The exception monad transformer

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

r e t u r n : A → M ( A + E ) a ↦ r e t u r n ( v a l u e a ) b i n d : M ( A + E ) → ( A → M ( B + E ) ) → M ( B + E ) m ↦ f ↦ b i n d m ( a ↦ { return err  e if  a = e r r e f a ′ if  a = v a l u e a ′ ) l i f t : M A → M ( A + E ) m ↦ b i n d m ( a ↦ r e t u r n ( v a l u e a ) ) {\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}}}

The reader monad transformer

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

r e t u r n : A → E → M A a ↦ e ↦ r e t u r n a b i n d : ( E → M A ) → ( A → E → M B ) → E → M B m ↦ k ↦ e ↦ b i n d ( m e ) ( a ↦ k a e ) l i f t : M A → E → M A a ↦ e ↦ a {\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}}}

The state monad transformer

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

r e t u r n : A → S → M ( A × S ) a ↦ s ↦ r e t u r n ( a , s ) b i n d : ( S → M ( A × S ) ) → ( A → S → M ( B × S ) ) → S → M ( B × S ) m ↦ k ↦ s ↦ b i n d ( m s ) ( ( a , s ′ ) ↦ k a s ′ ) l i f t : M A → S → M ( A × S ) m ↦ s ↦ b i n d m ( a ↦ r e t u r n ( a , s ) ) {\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}}}

The writer monad transformer

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

r e t u r n : A → M ( W × A ) a ↦ r e t u r n ( ε , a ) b i n d : M ( W × A ) → ( A → M ( W × B ) ) → M ( W × B ) m ↦ f ↦ b i n d m ( ( w , a ) ↦ b i n d ( f a ) ( ( w ′ , b ) ↦ r e t u r n ( w ∗ w ′ , b ) ) ) l i f t : M A → M ( W × A ) m ↦ b i n d m ( a ↦ r e t u r n ( ε , a ) ) {\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}}}

The continuation monad transformer

Given any monad M A {\displaystyle \mathrm {M} \,A} , the continuation monad transformer maps an arbitrary type R into functions of type ( A → M R ) → 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:

r e t u r n : A → ( A → M R ) → M R a ↦ k ↦ k a b i n d : ( ( A → M R ) → M R ) → ( A → ( B → M R ) → M R ) → ( B → M R ) → M R c ↦ f ↦ k ↦ c ( a ↦ f a k ) l i f t : M A → ( A → M R ) → M R b i n d {\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 S → ( A × S ) ? {\displaystyle S\rightarrow \left(A\times S\right)^{?}} (a computation which may fail and yield no final state), whereas the converse transformation has type S → ( A ? × S ) {\displaystyle S\rightarrow \left(A^{?}\times S\right)} (a computation which yields a final state and an optional return value).

See also

• Monads in functional programming

External links

The Wikibook Haskell has a page on the topic of: Monad transformers

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

References

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. http://portal.acm.org/citation.cfm?id=199528 ↩