Monad transformer
Encyclopedia
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).
) is defined by:
operation with identity element ) is defined by:
Note that monad transformations are not commutative: for instance, applying the state transformer to the option monad yields a type (a computation which may fail and yield no final state), whereas the converse transformation has type (a computation which yields a final state and an optional return value).
Functional programming
In computer science, functional programming is a programming paradigm that treats computation as the evaluation of mathematical functions and avoids state and mutable data. It emphasizes the application of functions, in contrast to the imperative programming style, which emphasizes changes in state...
, a monad transformer is a type constructor which takes a monad
Monads in functional programming
In functional programming, a monad is a programming structure that represents computations. Monads are a kind of abstract data type constructor that encapsulate program logic instead of data in the domain model...
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
t
of kindKind (type theory)In the area of mathematical logic and computer science known as type theory, a kind is the type of a type constructor or, less commonly, the type of a higher-order type operator...
(* -> *) -> * -> *
- Monad operations
return
andbind
(or an equivalent formulation) for allt m
wherem
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 = return
-
lift (m `bind` k) = (lift m) `bind` (lift . k)
-
The option monad transformer
Given any monad , the option monad transformer (where denotes the option typeOption type
In programming languages and type theory, an option type or maybe type is a polymorphic type that represents encapsulation of an optional value; e.g. it is used as the return type of functions which may or may not return a meaningful value when they're applied...
) is defined by:
The exception monad transformer
Given any monad , the exception monad transformer (where is the type of exceptions) is defined by:The reader monad transformer
Given any monad , the reader monad transformer (where is the environment type) is defined by:The state monad transformer
Given any monad , the state monad transformer (where is the state type) is defined by:The writer monad transformer
Given any monad , the writer monad transformer (where is endowed with a monoidMonoid
In abstract algebra, a branch of mathematics, a monoid is an algebraic structure with a single associative binary operation and an identity element. Monoids are studied in semigroup theory as they are naturally semigroups with identity. Monoids occur in several branches of mathematics; for...
operation with identity element ) is defined by:
The continuation monad transformer
Given any monad , the continuation monad transformer maps an arbitrary type into functions of type , where is the result type of the continuation. It is defined by:Note that monad transformations are not commutative: for instance, applying the state transformer to the option monad yields a type (a computation which may fail and yield no final state), whereas the converse transformation has type (a computation which yields a final state and an optional return value).
See also
- Monads in functional programmingMonads in functional programmingIn functional programming, a monad is a programming structure that represents computations. Monads are a kind of abstract data type constructor that encapsulate program logic instead of data in the domain model...
- Natural transformationNatural transformationIn category theory, a branch of mathematics, a natural transformation provides a way of transforming one functor into another while respecting the internal structure of the categories involved. Hence, a natural transformation can be considered to be a "morphism of functors". Indeed this intuition...
- a related concept in category theoryCategory theoryCategory theory is an area of study in mathematics that examines in an abstract way the properties of particular mathematical concepts, by formalising them as collections of objects and arrows , where these collections satisfy certain basic conditions...
External links
- http://conway.rutgers.edu/~ccshan/wiki/blog/posts/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