Understanding Monads (Re: Probable C# 6.0 features)

[Timon Gehr]

On 12/11/2013 03:32 PM, Robert Clipsham wrote:
> They way I like to think of monads is simply a box that performs
> computations.  ...

The term has a more general meaning in category theory. :)

What you are describing is a monad in the category of types and (pure!) 
functions. Since there has been some interest on this topic recently, 
I'll elaborate a little on that in a type theoretic setting. It would be 
easy to generalize the notions I'll describe to an arbitrary category.

I think it is actually easier to picture the concept using the 
definition that does not squash map and join into a single bind 
implementation and then derives them from there.

Then a monad consists of an endofunctor, and two natural transformations 
'return' (or 'η') and 'join' (or 'μ'). (I'll explain what each term 
means, and there will be examples, so bear with me :o). Feel free to ask 
questions if I lose you at some point.)

An endofunctor consists of:

m:   Type -> Type
map: Π(a:Type)(b:Type). (a -> b) -> (m a -> m b)

I.e. a mapping on types and a mapping on functions. The type of 'map' 
could be read as: for all types 'a' and 'b', map creates a function from 
'm a' to 'm b' given a function from 'a' to 'b'. The closest concept in 
D is a template parameter (but what we have here is cleaner.)

An example of an endofunctor is the following:

m: Type -> Type
m = list

map: Π(a:Type)(b:Type). (a -> b) -> (list a -> list b)
map a b f = list_rec [] ((::).f)

The details are not that important. This is just the map function on 
lists, so for example:

map nat nat [1,2,3] (λx. x + 1) = [2,3,4]

(In case you are lost, a somewhat analogous statement in D would be 
assert([1,2,3].map!(int,int)(x=>x+1) == [2,3,4]).)

The map function for any functor must satisfy some intuitive laws:

ftr-id: Π(a:Type). map a a (id a) = id (m a)

I.e. if we map an identity function, we should get back an identity 
function.

ftr-compose: Π(a:Type)(b:Type)(c:Type)(f:b->c)(g:a->b).
                map b c f . map a b g = map a c (f . g)


I.e. if we map twice in a row, we can just map the composition of both 
functions once. Eg. instead of

map nat nat (λx. x + 1) (map nat nat (λx. x + 2) [1,2,3])

we can write

map nat nat (λx. x + 3) [1,2,3]

without changing the result.

Many polymorphic containers form endofunctors in the obvious way. You 
could e.g. imagine mapping a tree (this corresponds to a functor (tree, 
maptree)

    1                                           2
   / \                                         / \
  2   3    - maptree nat nat (λx. x + 1) ->   3   4
     / \                                         / \
    4   5                                       5   6

A natural transformation between two functors (f, mapf) (g, mapg) is a 
mapping of the form:

η: Π(a:Type). f a -> g a

There are additional restrictions (though it is redundant to state them 
in a type theory where types arguments are parametric). Intuitively, if 
your functors are containers, a natural transformation is only allowed 
to reshape your data.

For example, a natural transformation from (tree, maptree) to (list, 
map) might reshape a tree into a list as follows:

     1
    / \
   2   3      - inorder nat -> [2,1,4,3,5]
      / \
     4   5

This example just performs an in-order traversal, but an arbitrary 
reshaping would be a natural transformation. Note that it is valid to 
lose or duplicate data, though usually one uses natural transformations 
that just preserve your data.)

Formally, the restriction is

naturality: Π(a:Type)(b:Type)(h:a->b). η b. mapf h = mapg h . η h

I.e.: if we map h over an 'f' and then reshape it we should get the same 
as if we had reshaped it first and then mapped on the reshaped 
structure. For example, if we reshape a tree into a list using a natural 
transformation, then it does not matter whether we increase all its 
elements by one before reshaping, or if we increase all elements of the 
resulting list by one.

We are now ready to state what a monad is (still in the restricted sense 
where we just consider the category of types and functions):

A monad consists of:
an endofunctor (m, map)

together with two natural transformations:

return: Π(a:Type). a -> m a
join: Π(a:Type). m (m a) -> m a

Note that return is a natural transformation from the identity functor 
(id Type, λa b. id (a->b)) to our endofunctor (m, map). And join is a 
natural transformation from (m . m, map . map) to (m, map). It is easy 
to see that those are indeed functors. The first one is an example of a 
functor that is not a kind of container (mapping is just function 
application on a single value.)

For implementing 'return', we should reshape a single value into an 'm'. 
E.g. if 'm' is 'list', the most canonical implementation of return is:

return: Π(a:Type). a -> list a
return a x = [x]

I.e. we create a singleton list. This is clearly a natural 
transformation. For the tree, we'd just create a single node.

For join, the most canonical implementation just preserves the order of 
the elements, but forgets some of the structure, eg:

[[1,2],[3,4],[5]] - join nat -> [1,2,3,4,5]

This is also what the eponymous function in std.array does for D arrays.

It is a little hard to draw in ASCII, but it is also easy to see how one 
could implement join for the tree example: Just join the root of every 
tree in your tree to the outer tree.

       1
      / \                                  1
    ---  \                                / \
    |2|   \        - jointree nat ->     2   3
    ---    \                                / \
        ---------                          4   5
        |   3   |
        |  / \  |
        | 4   5 |
        ---------

Of course there are now some intuitive restrictions on what 'return' and 
'join' operations constitute a valid monad, namely:

neutral_left: Π(a:Type). join a . map a (m a) (return a) = id
neutral_right: Π(a:Type). join a . return a = id

This is quite intuitive. I.e. if we reshape each element into the monad 
structure using return and then merge the inner structure into the outer 
one, we don't do anything. Analogously if we reshape the entire 
structure into a new monad structure and then join. Examples for the 
list case:

join nat (map nat (list nat) return [1,2,3]) =
   join nat [[1],[2],[3]] = [1,2,3]

join nat (return nat [1,2,3]) =
   join nat [[1,2,3]] = [1,2,3]


Furthermore we need:

associativity: Π(a:Type). join a . map (join a) = join a . join (m a)

I.e. it does not matter in which order we join.

These restrictions are also called the 'monad laws'.


Example for the list case:

join nat (map (join nat) [[[1,2],[3]],[[4],[5,6]]]) =
   join nat [[1,2,3],[4,5,6]] = [1,2,3,4,5,6]

join nat (join (list nat) [[[1,2],[3]],[[4],[5,6]]]) =
   join nat [[1,2],[3],[4],[5,6]] = [1,2,3,4,5,6]

At this point, this second restriction should feel quite intuitive as well.

Now what about bind? Bind is simply:

bind: Π(a:Type)(b:Type). m a -> (a -> m b) -> m b
bind a b x f = join b (map a (m b) f x)

i.e. bind is 'flatMap'.

Example with a list:

bind nat nat [1,2,3] (λx. [3*x-2,3*x-1,3*x]) =
   join nat (map a (m b) (λx. [3*x-2,3*x-1,3*x] [1,2,3]) =
     join nat [[1,2,3],[4,5,6],[7,8,9]] =
       [1,2,3,4,5,6,7,8,9]

Now on to something completely different: The state monad.

First we'll describe the endofunctor:

Let 'state' be the type of some state we want the monad to thread through.

m: Type -> Type
m a = state -> (a, state)

I.e. the structure we are looking at is a function that computes a 
result and a new state from some starting state. This is how we can 
capture side-effects to the state with a pure function. 'm a' is hence 
the type of a computation of a value of type 'a' that modifies a store 
of type 'state'.

Note that now our structure may be huge: It 'stores' an 'a' for every 
possible starting state. In order to map, we need to destructure down to 
the point where we can reach a single value:

map: Π(a:Type)(b:Type). (a -> b) -> (m a -> m b)
map a b f x = λ(s:state). case x s of { (a,s') => (f a, s') }

Note how this is quite straightforward. We need to return a function, so 
we just create a lambda and get a state. After we run x on the state we 
get a tuple whose first component we can map.

'return' is even easier: Embedding a value into the state monad creates 
a 'computation' with a constant result.

return: Π(a:Type). a -> m a
return a x = λ(s:state). (x,s)

Before we implement join, lets look at m (m nat):

state->(state->(a,state), state)

I.e. if we apply such a thing to a state, we get a function taking a 
state and returning an (a,state) as well as a state. Since we are 
looking to get an (a,state), the implementation writes itself:

join: Π(a:Type). m (m a) -> m a
join a x = λ(s:state). case x s of { (x',s') => x' s' }

Intuitively, to run a computation within the monad, just apply it to the 
current state and update the state accordingly.

Why does this satisfy the monad laws?

neutral_left: Π(a:Type). join a . map a (m a) (return a) = id

This states that turning a value into a constant computation with that 
result and then running that computation is a no-op. Check.

neutral_right: Π(a:Type). join a . return a = id

This states that if we wrap a computation in another one and then run 
the computation inside, this is the same computation as the one we 
started with. Check.

associativity: Π(a:Type). join a . map (join a) = join a . join (m a)

This states that composition of computations is associative. Check.

In case this last point is not so obvious, it says that if we have eg:

a=2;
b=a+3;
c=a+b;

Then it does not matter if we first execute a and then (b and then c) or 
if we first execute (a and then b) and then c. This is obvious.

In order to fully grok monads, it is also useful to look at how they can 
influence control flow. The monad with the most general effects on 
control flow is the continuation monad. But it's getting late, so if 
someone is interested I could explain this another time, or you might 
google it.