I used the first theory lunch meeting at the Institute of Cybernetics to recap some basics about monads. I discussed how monads are defined in category theory, and how they are implemented in Haskell.
Categories
A category consists of the following:
- a class of objects
- for any objects and , a class of morphisms
- for any object , an identity morphism
- for any objects , , and , a composition operation that maps morphisms and to morphisms
Composition is associative and identities are neutral elements of composition.
An example of a category is , the category of sets and functions, which is defined as follows:
- is the class of all sets.
- is , the set of all functions from to .
- is the identity function on .
- Morphism composition is function composition.
The category is similar to . It is defined as follows:
- is the set of all monomorphic Haskell types.
- is the set of all inhabitants of the type
->
. - is the identity function on .
- Morphism composition is function composition.
Categories with additional structure can also serve as models of logic. Here, objects model propositions, and morphisms model proofs.
Functors
A functor is a structure-preserving map from the category to the category . It maps every object of to an object of and every morphism of to a morphism such that
and
.
For every category , there exists the identity functor with
and
.
For functors and , we can form the composition with
and
.
In Haskell, there is the Functor
class, which is defined as follows:
class Functor f where fmap :: (a -> b) -> (f a -> f b)
Every instance of Functor
corresponds to a functor from to . Thereby, f
maps objects (which are types), and fmap
maps morphisms (which are functions).
Natural transformations
Let and be categories, and let and be functors from to . A natural transformation from to is a family for which
holds.
From and a functor , we can derive the natural transformation with
.
This is similar to applying a functor to a morphism. However if we have a functor , we can also derive the natural transformation with
.
Let f
and g
be instances of Haskell’s Functor
class, and let be the functors they denote. A natural transformation from to is a function t
of the polymorphic type forall a . f a -> g a
. The above axiom for natural transformations holds automatically, since t
has to treat values of type a
as black boxes. This is closely related to the concept of free theorems.
Functor categories
For any categories and , the functor category is defined as follows:
- is the class of all functors from to .
- is the class of all natural transformations from to .
- is .
- Morphism composition is pointwise composition of natural transformations.
Monads
A monad on a category is a triple where
and the equations
and
hold.
Given this definition, the straightforward way to implement monads on in Haskell is as follows:
class Functor m => Monad m where return :: a -> m a join :: m (m a) -> m a
Thereby, return
corresponds to , and join
corresponds to . The definition of the Monad
class in the Prelude is different though:
class Monad m where return :: a -> m a (>>=) :: m a -> (a -> m b) -> m b
That said, both definitions are equivalent, as (>>=)
can be defined in terms of fmap
and join
, and fmap
and join
can be defined in terms of return
and (>>=)
. The latter is done in Control.Monad
, where the fmap
derived from return
and (>>=)
is called liftM
.
Monads are used in Haskell to implement effectful computations. Thereby, the choice of a monad determines the kind of effect. Following is an overview of some monads:
Type | Effect |
---|---|
data Maybe a = Nothing | Just a |
failure |
data Either e a = Left e | Right a |
exception |
data [a] = [] | a : [a] |
nondeterminism |
newtype Reader r a = Reader (r -> a) |
read-only access to state |
newtype State s a = State (s -> (a,s)) |
read-write access to state |
Pingback: An introduction to ideal monads | Theory Lunch
Pingback: An introduction to ideal monads | Theory Lunch
Pingback: Three talks about ideal monads « Wolfgang Jeltsch