[Haskell-beginners] Relation between monads and computations

[Dmitriy Matrosov]

Hi, everyone!

Not so long ago i started to learn haskell, and now i have a question
about relation between monads and computations. In fact, i think, that
i understand it and write some explanation for myself, but i'm not
sure whether my explanation is correct or not, and will be very
thankful if someone check it :) Here it is (i don't know category
theory and my math knowledge is poor, so if i accidently use some
terms from them incorrectly - it was just my understanding).


Monads and computations.

Generally computation consists of initial value, computation itself and the
result. So it can be illustrated as:

    type    a         (M b)            b
    data    I ------>   C   <--------- E
                 f            ConstrM

    I :: a
    f :: a -> M b
    data M a = ContrM a | ...
    E :: b

Let's see what happens: i take initial value I of type a and map it to some
computation C (of type (M b)) using function f. Then, exist such value E of
type b, that C = (ConstrM E). This value E will be the result of computation.

Now consider two functions: unitM, which maps value into trivial computation
(trivial computation is a computation, which result is equal to initial
value):

    type    a         (M a)            a
    data    I ------>   C   <--------- I
               unitM          ConstrM

    I :: a
    unitM :: a -> M a
    data M a = ContrM a | ...

and bindM, which yields result from one computation, then applies some
function f to the result, and makes another computation at the end (E is the
result of this last computation).

    type    (M a)            a          (M b)            b
    data      C   ---------> I ------->   C' <---------- E
                   pattern        f            ConstrM
                    match
    data      C   -------------------->   C' <---------- E
                      C `bindM` f              ConstrM

    C :: M a
    I :: a
    f :: a -> M b
    C' :: M b
    data M a = ContrM a | ...
    E :: b
    bindM :: M a -> (a -> M b) -> M b

Now, using fucntions unitM and bindM there is possibly to convert arbitrary
function (k :: a -> b), which makes from initial value of type a value of type
b, into terms of general computation (represented by type M).

    type    a         (M a)            a         b          (M b)           b
    data    I ------>   C   ---------> I ------> E ------->   C'  <-------- E
               unitM         pattern        k       unitM          ConstrM
                              match
    data    I ------>   C   ---------> I ----------------->   C'  <-------- E
               unitM         pattern       f = (unitM . k)         ConstrM
                              match
    data    I ------>   C   ------------------------------>   C'  <-------- E
               unitM                     `bindM` f                 ConstrM
    data    I -------------------------------------------->   C'  <-------- E
                           g = (`bindM` f) . unitM                 ConstrM

    I :: a
    unitM :: a -> M a
    C :: M a
    k :: a -> b
    C' :: M b
    data M a = ConstrM a | ...
    E :: b
    f :: a -> M b
    bindM :: M a -> (a -> M b) -> M b
    g :: a -> M b

On the first picture i take initial value I of type a, and map it to trivial
computation C of type (M a) using unitM. Then i yield result of this trivial
computation C (which is I, of course), apply function k to this result (value
I) and get value E of type b as result. Then i wrap this value E into trivial
computation C' using unitM. Result of computation C' is, of course, E.  On the
intermediate pictures i show reduction steps of the first picture. And finally
i get: i take initial value I of type a, and map it using function g into
computation C'. The result of computation C' is value E of type b.

So, from arbitrary function (k :: a -> b) i can create function g, which maps
initial value I of type a into some computation of type (M b). Actual
computation (calculation) will still be performed by k, but the result will
have type of general computation (M b) instead of b.


Monad is a way to implement such general computation, a way to write a program
based on general computations, which later may be redefined, instead of
particular ones, which redefinition leads to rewrite of large of amount of
code. Monad is a triple of type constructor M and functions unitM and bindM
(and errorM, probably?). Type constructor represents computation itself,
functions unitM and bindM used to wrap your own specific computation (k :: a
-> b) on types a and b into monadic notation (general computation notation).

First two of monad laws demand, that unitM maps into trivial computation.
..may be continued..

--
    Dmitriy Matrosov