Deokhwan Kim wrote:
What is the practical meaning of monad laws?
(M, return, >>=) is not qualified as a category-theoretical monad, if the following laws are not satisfied:
1. (return x) >>= f == f x 2. m >>= return == m 3. (m >>= f) >>= g == m >> (\x -> f x >>= g)
The 3. law contains a typo and must be 3. (m >>= f) >>= g == m >>= (\x -> f x >>= g)
But what practical problems can unsatisfying them cause? In other words, I wonder if declaring a instance of the Monad class but not checking it for monad laws may cause any problems, except for not being qualified as a theoretical monad?
This question is likely to be a result of an unlucky introduction to monads where they are introduced top down: "Hear ye, a monad, this is some mystic thing obeying the spiritual laws 1.,2. and 3.", isn't it? It is this way that monads get the attribute "theoretical". Asking what the practical meaning of the monad laws might be is like asking what the practical meaning of the laws for natural number addition could be: what does i) a + (b+c) == (a+b) + c mean? How can i understand ii) a + 0 == a ? What does iii) a + b == b + a signify? These question are unlikely to arise because you have an intuition of what a natural number is: a number of bullets in sack, coins in your pocket, people in the mailing-list etc. With this knowledge, you will most likely not have any problems explaining the laws i),ii),iii) to somebody else and most likely you will have not doubt about *why* they must be true. For monads, my intuition is as following: a value of type (M a) is an action, something producing a value of type a and (or by) executing a side-effect like drawing on the screen or screwing up the hard drive. With the operator >>=, I can execute such actions in a specific sequence. For the sequence, it is of course unimportant how i group my actions: i can group actions act1 and act2 first and then postpend act3, or i can group act2 and act3 first and then prepend it with act1. To simplify writing down a formular corresponding to this fact, we introduce the operator >> defined by act1 >> act2 = act1 >>= \x -> act2 which sequences actions but for simplicity discards the computed value x of type a. It is only the side-effect of act1 we are interested in. Now, the thought about grouping written does as formular is just (act1 >> act2) >> act3 == act1 >> (act2 >> act3) and this is the simplified version of law 3. Of course, we know that this is coined "associativity". The actual law 3 is just a formulation for >>= that takes proper care of the intermediate calculation result x. With return x , we can create an action which computes the value x but has absolutely no side-effects. This can also be stated in formulas, as Mr "return" explains: 1. "if i am prepended to guys doing side-effects, i give them the value x but do not take any responsibility for side-effects happening" (return x) >>= (\y -> f y) == f x 2. "if i am postponed to an action which computes a value x, i don't do any additional side-effects but just return the value i have been given" m >>= (\x -> return x) == m which is of course equivalent to m >>= return == m So to answer your question:
In other words, I wonder if declaring a instance of the Monad class but not checking it for monad laws may cause any problems, except for not being qualified as a theoretical monad? A thing you declare to be an instance of the Monad class, but one that does not fulfill the three laws above, simply does not match the intuition behind a monad. I.e. your definitions of (>>=) and (return) are most likely to be void of the intended meaning.
Regards, apfelmus