A short recap of monads

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

About these ads