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:
- A type constructor
t of kind (* -> *) -> * -> * - Monad operations
return and bind (or an equivalent formulation) for all t m where m is a monad, satisfying the monad laws - An additional operation,
lift :: m a -> t m a, satisfying the following laws: (the notation `bind` below indicates infix application):lift . return = returnlift (m `bind` k) = (lift m) `bind` (lift . k)
Given any monad M A , the option monad transformer M ( A ? ) (where 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 ) ) Given any monad M A , the exception monad transformer 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 ) ) Given any monad M A , the reader monad transformer E → 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 Given any monad M A , the state monad transformer S → M ( A × 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 ) ) Given any monad M A , the writer monad transformer M ( W × A ) (where W is endowed with a monoid operation ∗ with identity element ε ) 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 ) ) Given any monad M A , the continuation monad transformer maps an arbitrary type R into functions of type ( A → M R ) → 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 Note that monad transformations are usually not commutative: for instance, applying the state transformer to the option monad yields a type S → ( A × S ) ? (a computation which may fail and yield no final state), whereas the converse transformation has type S → ( A ? × S ) (a computation which yields a final state and an optional return value).
