-- definition
 
class Monad m where
   return :: a -> m a
   (>>=)  :: m a -> (a -> m b) -> m b
 
-- utility functions
 
   (>=>)  :: (a -> m b) -> (b -> m c) -> (a -> m c)
   (f >=> g) a = f a >>= g
 
   fmap   :: (a -> b) -> m a -> m b
   fmap f ma =  ma >>= (return . f)
 
   join   ::  m (m a) ->  m a
   join mma = mma >>= id
 
   (>>)   :: m a -> m b -> m b
   ma >> mb = ma >>= (const mb)

The laws can be viewed as right unit, left unit and associativity.

The operation »= is also called 'bind'. Its type is somewhat ugly, especially because of a→m b. But instantiating a monad by implementing 'bind' is more concise than defining 'fmap' and 'join', which is what mathematicians usually do.

A term 'f x y' can be viewed as an x-indexed family of functions 'f x', evaluated at y. For fixed x, we're going to use 'f x' as second argument for the bind operation 'my »=', where 'my' might also depend on x, and then lambda abstract the x outside. The resulting function can be used argument for a second bind 'mx »='. The resulting body

 mx >>= \x-> (my >>= \y -> f x y) 

can be viewed as a function 'f :: a → b → m c', which has been passed two monadic values 'mx :: m a', 'mx :: m a'. Haskell has the following syntactic sugar for this expression

 do {x <- mx; y <- my; f x y} 

and one easily extends this to any number of arguments 'do {x ← mx; y ← my; z ←mz …'.

A 'do' block is of course still a single expression. One might say that the procedural aspect of it is that eta/beta-reduction of the inner expression possibly include reductions of the outer ones - there is a smart and a stupid way to compute 'do { x ← return (2^2-4); y ← return (x*(x+1)^7); return (x+y) }'.

For the time being, this example is instructive

 [1,2] >>= (\ x -> [2,3] >>= (\y -> return (x/=y) >>= (\r -> (case r of True -> return (x,y); _ -> [])))) 

is

 do x <- [1,2]; y <- [2,3]; r <- return (x/=y); (case r of True -> return (x,y); _ -> []) 

is

 [(x,y) | x <- [1,2], y <- [2,3], x/=y] 

Here is what makes the use of predicates possible: Note that 'join [ [1,2],[],[3],[] ]' is '[1,2,3]' and this is part of the working of the list monads »=. Since for x=2, y=2, the Bool 'x/=y' isn't 'True', the value '[]' is returned and consequently dropped from the resulting list.

The list-functors $\text{fmap}$ maps functions $f :: a \to b$ to functions $T(f)$ defined by concatenation with Haskells $\text{map}$ function, i.e. $\text{fmap}\ f\ xs\ =\ [\ f\ a\ |\ a \leftarrow xs\ ]$, e.g. $\text{map}\ (x\mapsto x^2)\ [2,3,4]$ evaluates to $[4,9,16]$. $\text{return}$ then maps terms $x$ of type $a$ to terms $[x]$ (list with one member) of type $[a]$. $\text{join}$ is flatten, e.g. $\text{join}$ applied to the list of lists $[[7,9,3],[2],[5,10]]$ evaluates to $[7,9,3,2,5,10]$.

Now what the functor construction does for you is generating infinite depth (lists of lists of lists of…) and once you’ve proven your system monadic, you know that your arrows are structural throughout the system: E.g. let $f :: \text{Int}\to\text{Char}$, then

• $\text{map}\ f\ (\text{return}\ 3)$ is $\text{map}\ f\ [3]$ is $[f\ 3]$.
• $\text{return}\ (f\ 3)$ is $[f\ 3]$ as well.

Similarly,

• $\text{map}\ f\ (\text{join}\ [[7,3],[2]])$ is $\text{map}\ f\ [7,3,2]$ is $[f\ 7,f\ 3,f\ 2]$.
• $\text{join}\ (\text{map}\ (\text{map}\ f)\ [[7,3],[2]])$ is $\text{join}\ [(\text{map}\ f)\ [7,3],(\text{map}\ f)\ [2]]$ is $\text{join}\ [[f\ 7,f\ 3],[f\ 2]]$ is $[f\ 7,f\ 3,f\ 2]$ as well.

Types $a$ get mapped to $\text{Maybe}\ a$. For each type $a$, the type $\text{Maybe}\ a$ contains a copy of all of $a$'s terms $x,y,\dots$, there written $\text{Just}\ x,\text{Just}\ y,\dots$, plus an additional term called $\text{Nothing}$. I.e. the maybe functor effectively adds an „exception“ term to all types of $\text{Hask}$. If $f:: a\to b$ and $x::a$, then the arrow image of the functor on $f$ is just the function which maps $\text{Just}\ x$ to $\text{Just}\ f(x)$ and

Return maps $x$ in $a$ to $\text{Just}\ x$ in $\text{Maybe}\ a$ and join maps $\text{Just}\ (\text{Just}\ x)$ to $\text{Just}\ x$ and in particular, $\text{Just}\ \text{Nothing}$ to $\text{Nothing}$.

Note that for any 'g::a→b', the function 'return.g' is of type a→m b and therefore the pattern 'mx »= \x→return (g x)' is generally common. (However not all terms of a→m b are of the form return.g.) This is used to “lift” non-monadic functions 'f :: a → b → m c':

 liftM2 f mx my = do {x <- mx; y <- my; return (f x y)} 

Since 'id f x = f x', id on functions is curried eval and so id for function spaces takes two arguments. Since id comes for every type/object, every monad gives rise to an Applicative instance via

(<*>) :: m (a -> b) -> m a -> m b
(<*>) mg ma = liftM2 id mg my
-- or = join $ fmap (\g -> fmap g mx) mg

Note that conversely, '<*>' doesn't suffice to define a '»='.

I'm going to explain what this (<*>) does in mathematical terminology: The Yoneda lemma implies that there is an isomorphism from $FA$ to $\mathrm{nat}(\mathrm{Hom}(A,B),FB)$. Consider a category with exponential objects and arrows corresponding to components of the natural transformations (such as is the case for Hask, where the above map is $at\mapsto g\mapsto T(g)(ta):FA\to B^A\to FB$), then we can apply the functors arrow map to the latter and obtain a map $FA\to F\,B^A\to FFB)$ to. One could say that this is provides a way to “apply” $tg:F\,B^A$ to $ta:FA$. Note, however, that $T\,B^A$ isn't necessarily a honest function space anymore, so that's abuse of terminology. (For example, 'Noting :: Maybe (Int→Int)' isn't a function. Things still work out, however, because if you pass 'Noting', the outer arrow mapping in the described function takes care of it. In that case the 'tg' value doesn't even matter so this is hardly an “evaluation” of 'Nothing'.). Lastly, if the functor comes with a monadic 'join', then we can get rid of the second $F$ in $FFB$ in the type of the function, and then it's called '<*>'.

One could define a monad via 'join' and 'fmap' (mathematicians definition) and then set

f >=> g =  join . (fmap g) . f
ma >>= f = (join . (fmap f)) ma

One could also define '>⇒' and set

ma >>= f = (id >=>  f)  ma
fmap f =  id >=> (return . f)
join =  id >=> id

Monad (category theory), Monade (Informatik)

Applicative