Relation between monads and computations
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
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
Hi Brent, thanks for the answer!
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...
The original question was: "Am i right?". I just try to understand what monad is, and, because it is referred as computations, i try to understand why. E.g. from [2], end of section 2.1: "Just as the type Value represents a value, the type M Value can be thought of as representing a computation. The purpose of unitM is to coerce a value into computation; the purpose of bindM is to evaluate a computation, yielding a value." Similarly, it often referred as computation in [1]. (Though, i don't finish reading both of these papers).
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.
May i ask you then, what is the precise definition of monad? The only other definition besides "the computation", which i know, is "a triple of (M, unitM, bindM)" (from [2]), but it does not explain to me what this may have common with computations. Definition of computation, which i assume, is something (may be better to say triple), which have initial value, some transformation (function? or action?) and the result. Is this definition correct?
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.
Well, you're right, this should be rewritten. Here i just try to recognise in monad all three parts of my computation definition. Then: "the result of computation is values E1,.. En of type b from which using constructors ConstrM1,.. ContrMk may be made computation C of type M b". Is the idea right?
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).
Hmm, so i was wrong here. Initially, i suppose, that the purpose of bindM is to convert function of type (a -> b) into function of type (a -> M b), but now i see it is wrong. Mentioned above quote from [2] says, that "the purpose of bindM is to evaluate a computation, yielding a value.", which sounds a little unfinished to me. Then may be: the purpose of bindM is to make composition of functions of type (a -> M b) and (b -> M c) possible. Is this right? References: [1] Hal Daume III, "Yet another haskell tutorial" [2] Philip Wadler, "The essence of functional programming" -- Dmitriy Matrosov
On Wed, Feb 15, 2012 at 10:31:03PM +0300, Dmitriy Matrosov wrote:
Hi Brent, thanks for the answer!
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...
The original question was: "Am i right?". I just try to understand what monad is, and, because it is referred as computations, i try to understand why. E.g. from [2], end of section 2.1: "Just as the type Value represents a value, the type M Value can be thought of as representing a computation. The purpose of unitM is to coerce a value into computation; the purpose of bindM is to evaluate a computation, yielding a value."
"The purpose of bindM is to evaluate a computation, yielding a value" -- I have the greatest respect for Phil Wadler, but this is simply wrong. From this description one would expect bindM to have the type bindM :: M a -> a but it does not.
Similarly, it often referred as computation in [1]. (Though, i don't finish reading both of these papers).
Referring to values of type M a as "computations" is just supposed to give some intuition, it is not a precise statement or a definition in any sense. Monads are one possible formal framework for *defining* what we mean by "computation". So trying to understand how monads are computations will not get you anywhere. Instead, you should just try to understand various examples of monads, and eventually you may get some insight into how they can be thought of as "computations".
May i ask you then, what is the precise definition of monad? The only other definition besides "the computation", which i know, is "a triple of (M, unitM, bindM)" (from [2]),
Yes. A monad is a triple (M, unitM, bindM) satisfying a certain set of equational laws.
but it does not explain to me what this may have common with computations.
Of course it doesn't. The definition of the Peano naturals does not explain what they have to do with counting. The definition of a group does not explain what it has to do with symmetry. Etc.
Definition of computation, which i assume, is something (may be better to say triple), which have initial value, some transformation (function? or action?) and the result. Is this definition correct?
No. If you want to *define* computation, then in this context one should say "the definition of computation is a value of type M a, where M is a monad"! The word "computation" has been chosen because this turns out to correspond to certain intuitive ideas people have about that word but to really understand which intuitive ideas are meant you will have to study the definition and examples of monads.
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.
Well, you're right, this should be rewritten. Here i just try to recognise in monad all three parts of my computation definition. Then: "the result of computation is values E1,.. En of type b from which using constructors ConstrM1,.. ContrMk may be made computation C of type M b". Is the idea right?
Not really. I advise you to forget the idea of defining what the "result" of a computation is. As I said above, the quote from Phil Wadler about running a computation and extracting its result is wrong (or at the very least, extremely unhelpful).
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).
Hmm, so i was wrong here. Initially, i suppose, that the purpose of bindM is to convert function of type (a -> b) into function of type (a -> M b), but now i see it is wrong. Mentioned above quote from [2] says, that "the purpose of bindM is to evaluate a computation, yielding a value.", which sounds a little unfinished to me. Then may be: the purpose of bindM is to make composition of functions of type (a -> M b) and (b -> M c) possible. Is this right?
Yes! In fact, there is a standard operator (>=>) :: Monad m => (a -> m b) -> (b -> m c) -> (a -> m c) which is defined in terms of bind. Implementing it is a good exercise. By the way, you may be interested in reading the Typeclassopedia: http://www.haskell.org/haskellwiki/Typeclassopedia -Brent
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).
Hmm, so i was wrong here. Initially, i suppose, that the purpose of bindM is to convert function of type (a -> b) into function of type (a -> M b), but now i see it is wrong. Mentioned above quote from [2] says, that "the purpose of bindM is to evaluate a computation, yielding a value.", which sounds a little unfinished to me. Then may be: the purpose of bindM is to make composition of functions of type (a -> M b) and (b -> M c) possible. Is this right?
Yes! In fact, there is a standard operator
(>=>) :: Monad m => (a -> m b) -> (b -> m c) -> (a -> m c)
which is defined in terms of bind. Implementing it is a good exercise.
By the way, you may be interested in reading the Typeclassopedia:
Thank you very much, Brent! I'll try what you advise and read this link. And then may be ask again.. :) -- Dmitriy Matrosov
participants (2)
-
Brent Yorgey -
Dmitriy Matrosov