Explanation of Monad laws

问题:

From a gentle introduction to Haskell, there are the following monad laws. Can anyone intuitively explain what they mean?

return a >>= k             = k a
m >>= return               = m
xs >>= return . f          = fmap f xs
m >>= (\x -> k x >>= h)    = (m >>= k) >>= h

Here is my attempted explanation:

1. We expect the return function to wrap a so that its monadic nature is trivial. When we bind it to a function, there are no monadic effects, it should just pass a to the function.

2. The unwrapped output of m is passed to return that rewraps it. The monadic nature remains the same. So it is the same as the original monad.

3. The unwrapped value is passed to f then rewrapped. The monadic nature remains the same. This is the behavior expected when we transform a normal function into a monadic function.

4. I don't have an explanation for this law. This does say that the monad must be "almost associative" though.

回答1:

Your descriptions seem pretty good. Generally people speak of three monad laws, which you have as 1, 2, and 4. Your third law is slightly different, and I'll get to that later.

For the three monad laws, I find it much easier to get an intuitive understanding of what they mean when they're re-written using Kleisli composition:

-- defined in Control.Monad
(>=>) :: Monad m => (a -> m b) -> (b -> m c) -> a -> m c
mf >=> n = \x -> mf x >>= n

Now the laws can be written as:

1) return >=> mf = mf                  -- left identity
2) mf >=> return = mf                  -- right identity
4) (f >=> g) >=> h = f >=> (g >=> h)   -- associativity

1) Left Identity Law - returning a value doesn't change the value and doesn't do anything in the monad.

2) Right Identity Law - returning a value doesn't change the value and doesn't do anything in the monad.

4) Associativity - monadic composition is associative (I like KennyTM's answer for this)

The two identity laws basically say the same thing, but they're both necessary because return should have identity behavior on both sides of the bind operator.

Now for the third law. This law essentially says that both the Functor instance and your Monad instance behave the same way when lifting a function into the monad, and that neither does anything monadic. If I'm not mistaken, it's the case that when a monad obeys the other three laws and the Functor instance obeys the functor laws, then this statement will always be true.

A lot of this comes from the Haskell Wiki. The Typeclassopedia is a good reference too.

回答2:

No disagreements with the other answers, but it might help to think of the monad laws as actually describing two sets of properties. As John says, the third law you mention is slightly different, but here's how the others can be split apart:

Functions that you bind to a monad compose just like regular functions.

As in John's answer, what's called a Kleisli arrow for a monad is a function with type a -> m b. Think of return as id and (<=<) as (.), and the monad laws are the translations of these:

1. id . f is equivalent to f
2. f . id is equivalent to f
3. (f . g) . h is equivalent to f . (g . h)

Sequences of monadic effects append like lists.

For the most part, you can think of the extra monadic structure as a sequence of extra behaviors associated with a monadic value; e.g. Maybe being "give up" for Nothing and "keep going" for Just. Combining two monadic actions then essentially concatenates the sequences of behaviors they held.

In this sense, return is again an identity--the null action, akin to an empty list of behaviors--and (>=>) is concatenation. So, the monad laws are translations of these:

1. [] ++ xs is equivalent to xs
2. xs ++ [] is equivalent to xs
3. (xs ++ ys) ++ zs is equivalent to xs ++ (ys ++ zs)

---

These three laws describe a ridiculously common pattern, which Haskell unfortunately can't quite express in full generality. If you're interested, Control.Category gives a generalization of "things that look like function composition", while Data.Monoid generalizes the latter case where no type parameters are involved.

回答3:

In terms of do notation, rule 4 means we can add an extra do block to group a sequence of monadic operations.

    do                          do
                                  y <- do
      x <- m                             x <- m
      y <- k x          <=>              k x
      h y                         h y

This allows functions that return a monadic value to work properly.

回答4:

The first three laws say that "return" only wraps a value and does nothing else. So you can eliminate "return" calls without changing the semantics.

The last law is associativity for bind. It means that you take something like:

do
   x <- foo
   bar x
   z <- baz

and turn it into

do
   do
      x <- foo
      bar x
   z <- baz

without changing the meaning. Of course you wouldn't do exactly this, but you might want to put the inner "do" clause in an "if" statement and want it to mean the same when the "if" is true.

Sometimes monads don't exactly follow these laws, particularly when some kind of bottom value occurs. That's OK as long as its documented and is "morally correct" (i.e. the laws are followed for non-bottom values, or the results are considered equivalent in some other way).

回答5:

A monad essentially is used to allow access at global value and in the same time to hide the global value from the parameter list of the function.

The idea is, the a function call, in order to simulate a global, receives its actual arguments and also the global and returns the value and the new global. The monad is used to do this in an elegant way by hiding the global value.

For a monad of type Mx, each monadic operation is a closure that encloses a value of type x. The monadic operation says "pass me the global value and I provide you the result consisting of the new value of the global and in the same time the value you need to compute" -- this statement is the same for any monad, including the continuation monad.

There are 2 operators that are enough to make any computation as a monad and both of them follow the logic of this statement.

The return operator simply packs the value to be computed in the environment of a closure that does no computation. This closure waits for the global value and provides the answer

The bind operator also is waiting for a global value but it makes some computation before to provide the answer. It unpacks the value enclosed in the monad (it unpacks the value enclosed by the closure representing the monad), makes some computation in 2 continuations that are passed once the global value and other one that is passed the value computed by the first continuation and returns a new closure enclosing the computed value as a monadic value.

Now , to answer your question, from the viewpoint just described, the unit-law composition says that the return operator is never allowed to change the value of the global variable that it receives, otherwise, even if the code is semantically correct, it is no more a monad pattern due to type checking.

The associative law means that the order of monadic compositions is not important. This is in agreement with the lazy evaluation and mathematical model of composing the same operator in associative way.