[Haskell-beginners] Relation between monads and computations

[Brent Yorgey]

Hi Dmitriy,

On Thu, Feb 09, 2012 at 02:02:59PM +0300, Dmitriy Matrosov wrote:
> 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).

You say you have a question, but from reading the below I am not sure
what your question is...

Let me say first that while "monad" has a precise technical
definition, "computation" does not.  So "the relation between monads
and computations" is not well-defined unless it is specified what you
mean by "computation".  There are many ways to model different ideas
of "computation"; one of them is monads, but that is not the only way.

> 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.

That last part ("there exists a value E of type b ...") doesn't seem
right to me.  There is no guarantee or requirement that a monad M be
defined so there is a constructor wrapping the "result".  For example,
consider the list type:

  data [a] = [] | (a : [a])

In this case a function of type  a -> [b]  might produce a list
containing multiple values of type b.  There is no single value of
type b which is the "result", and there is no constructor which wraps
a single value of type b into a list.

> 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

You have written this as if `bindM` works by extracting a single value
of type 'a' from C and running f on it, resulting in C'.  But this is
not how it works.  As I have shown above, there may not be a "single
value" that can be extracted from C.  `bindM` works in a way that is
specific to M, and may involve running f multiple times, or not at
all.

> 
> 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).

Yes, (k :: a -> b) can be converted into a function of type  (a -> M
b), but I think you have made it more complicated than necessary.  All
you need to do is  (unitM . k).

> 
>     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

(`bindM` f) . unitM  is equivalent to just   (unitM . k)  by the monad laws.

> 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).

I think you have some of the right ideas, but some of the details seem
confused.  (And no, the abstract idea of a monad does not include
errorM; the inclusion of 'fail' in the Monad class is just a hack
based on hsitorical accident.)

-Brent