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