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 \mathcal C consists of the following:

  • a class \mathrm{Ob}(\mathcal C) of objects
  • for any objects A and B, a class \mathrm{hom}_{\mathcal C}(A, B) of morphisms f : A \to B
  • for any object A, an identity morphism \mathrm{id}_A
  • for any objects A, B, and C, a composition operation that maps morphisms f : A \to B and g : B \to C to morphisms gf : A \to C

Composition is associative and identities are neutral elements of composition.

An example of a category is \mathbf{Set}, the category of sets and functions, which is defined as follows:

  • \mathrm{Ob}(\mathbf{Set}) is the class of all sets.
  • \mathrm{hom}_{\mathbf{Set}}(A, B) is B^A, the set of all functions from A to B.
  • \mathrm{id}_A is the identity function on A.
  • Morphism composition is function composition.

The category \mathbf{Hask} is similar to \mathbf{Set}. It is defined as follows:

  • \mathrm{Ob}(\mathbf{Hask}) is the set of all monomorphic Haskell types.
  • \mathrm{hom}_{\mathbf{Hask}}(\tau_1, \tau_2) is the set of all inhabitants of the type \tau_1 -> \tau_2.
  • \mathrm{id}_\tau is the identity function on \tau.
  • 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 F : \mathcal C \to \mathcal D is a structure-preserving map from the category \mathcal C to the category \mathcal D. It maps every object A of \mathcal C to an object FA of  \mathcal D and every morphism f : A \to B of \mathcal C to a morphism Ff : FA \to FB such that

\forall A \in \mathrm{Ob}(\mathcal C) \mathrel. F\mathrm{id}_A = \mathrm{id}_{FA}

and

\forall A, B, C \in \mathrm{Ob}(\mathcal C) \mathrel. \forall f : A \to B \mathrel. \forall g : B \to C \mathrel. F(gf) = (Fg)(Ff) .

For every category \mathcal C, there exists the identity functor \mathrm{Id}_{\mathcal C} : \mathcal C \to \mathcal C with

\forall A \in \mathrm{Ob}(\mathcal C) \mathrel. \mathrm{Id}_{\mathcal C}A = A

and

\forall A, B \in \mathrm{Ob}(\mathcal C) \mathrel. \forall f : A \to B \mathrel. \mathrm{Id}_{\mathcal C}f = f .

For functors F : \mathcal C \to \mathcal D and G : \mathcal D \to \mathcal E, we can form the composition GF : \mathcal C \to \mathcal E with

\forall A \in \mathrm{Ob}(\mathcal C) \mathrel. (GF)A = G(FA)

and

\forall A, B \in \mathrm{Ob}(\mathcal C) \mathrel. \forall f : A \to B \mathrel. (GF)f = G(Ff) .

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 \mathbf{Hask} to \mathbf{Hask}. Thereby, f maps objects (which are types), and fmap maps morphisms (which are functions).

Natural transformations

Let \mathcal C and \mathcal D be categories, and let F and G be functors from \mathcal C to \mathcal D. A natural transformation \tau from F to G is a family \left\{\tau_A : FA \to GA\right\}_{A \in \mathrm{Ob}(\mathcal C)} for which

\forall A, B \in \mathrm{Ob}(\mathcal C) \mathrel. \forall f : A \to B \mathrel. \tau_B(Ff) = (Gf)\tau_A

holds.

From \tau and a functor V : \mathcal D \to \mathcal Q, we can derive the natural transformation V\tau : VF \to VG with

\forall A \in \mathrm{Ob}(\mathcal C) \mathrel. \left(V\tau\right)_A = V\left(\tau_A\right) .

This is similar to applying a functor to a morphism. However if we have a functor W : \mathcal Q \to \mathcal C, we can also derive the natural transformation \tau W : FW \to GW with

\forall X \in \mathrm{Ob}(\mathcal Q) \mathrel. \left(\tau W\right)_X = \tau_{WX} .

Let f and g be instances of Haskell’s Functor class, and let F, G : \mathbf{Hask} \to \mathbf{Hask} be the functors they denote. A natural transformation from F to G 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 \mathcal C and \mathcal D, the functor category \mathcal D^{\mathcal C} is defined as follows:

  • \mathrm{Ob}\left(\mathcal D^{\mathcal C}\right) is the class of all functors from \mathcal C to \mathcal D.
  • \mathrm{hom}_{\mathbf{\mathcal D^{\mathcal C}}}(F, G) is the class of all natural transformations from F to G.
  • \mathrm{id}_F is \left\{\mathrm{id}_{FA}\right\}_{A \in \mathrm{Ob}(\mathcal C)}.
  • Morphism composition is pointwise composition of natural transformations.

Monads

A monad on a category \mathcal C is a triple (T, \eta, \mu) where

\begin{array}{rcl}T & : & \mathcal C \to \mathcal C \\ \eta & : & \mathrm{Id}_{\mathcal C} \to T \\ \mu & : & TT \to T\end{array}

and the equations

\mu(\eta T) = \mu(T\eta) = \mathrm{id}_T : T \to T

and

\mu(\mu T) = \mu(T\mu) : TTT \to T

hold.

Given this definition, the straightforward way to implement monads on \mathbf{Hask} 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 \eta, and join corresponds to \mu. 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

3 thoughts on “A short recap of monads

  1. Pingback: An introduction to ideal monads | Theory Lunch

  2. Pingback: An introduction to ideal monads | Theory Lunch

  3. Pingback: Three talks about ideal monads « Wolfgang Jeltsch

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s