0
$\begingroup$

Monad laws in Haskell

Left identity:  return a >>= f ≡ f a
Right identity: m >>= return ≡ m
Associativity: (m >>= f) >>= g ≡ m >>= (\x -> f x >>= g)

is widely known, and I think the "Left identity" rule does not make sense.

In category theory, it is true that Monads corresponds to Monoid, but this "Left identity" is twisting things around.

the binary operator >>= is a notation, so is f a or f(x) etc..

  • f(x)
  • f a
  • m >>= f
  • monad.bind(f)

In program semantics, all are the same, especially, when we define f always returns a monad value.

It's like "1" and "One" means the same entity in mathematics.

1 ≡ "One"  // Some Identity! 
// this rule must be satisfied in terms of category theory!??

So-called "Left identity" in Haskell Monad law: return a >>= f ≡ f a is nothing to do with category theory but simply notation.

On the other hand "Right identity": m >>= return ≡ m makes sense because according to the notation replacement, it can be rewritten to return m ≡ m, and surely this defines one of monad feature or a rule of identity.

(edit)

  • TTX = TX
  • unit(unit(a)) = unit(a)
  • return m ≡ m

whatever, the semantics is the same.

In the later part of [Monad laws in Haskell][1], it makes an excuse saying

Not in this form, no. To see precisely why they're called "identity laws" and an "associative law", you have to change your notation slightly.

then, it introduces "Kleisli composition operator" : >=>.

What?? The different operator is introduced, then they concluds:

This is a very important way to express the three monad laws, because they are precisely the laws that are required for monads to form a mathematical category.

The widely known "Haskell monad laws" are based on the bind binary operator: >>=, but in fact, the "left identity" rule is nothing to do with catrgory theory but merely programming notation replacement, then later, by replacing the bind operator to "Kleisli composition operator" : >=>, it claims the notation replacement is based on category theory.

I think this fools the readers and is the source of confusion of Monad concept to beginers or all of us.

Probably, I also need to mention that this Monad laws are firstly fomalized in Monads for functional programming by Philip Wadler

EDIT:

Well, I do not deny return a >>= f ≡ f a is a binary operator definition. It's a replacement of notation, and here is the thing.

notation replacement is nothing to do with category theory or "Left identity" `

$\endgroup$
  • 7
    $\begingroup$ A little less attitude would go a long way. For reference, the monad laws were not invented by Phil Wadler (and of course he never said they were). As far as I know they were first used in the form we know them today by Roger Godement in the 1950's. $\endgroup$ – Andrej Bauer Oct 20 '18 at 21:30
  • 1
    $\begingroup$ I don't see any answerable question, here. If you have a question (and not just "Am I right?", pelase), please edit your post to include it. I'd also recommend trimming down the text somewhat. It usually doesn't need two screenfuls of browser text to ask a clear question. $\endgroup$ – David Richerby Oct 22 '18 at 15:29
  • $\begingroup$ @DavidRicherby: the question was first asked on StackOverflow, which resulted in a rather "heated discussion" chat.stackoverflow.com/rooms/182205/… $\endgroup$ – Willem Van Onsem Oct 23 '18 at 11:55
  • $\begingroup$ @AndrejBauer Thanks. What I meant is the monad laws in Haskell (Kleisli triple), and I believe it's formalized by Phil Wadler . $\endgroup$ – bayesian-study Oct 24 '18 at 14:46
  • 2
    $\begingroup$ It was Eugenio Moggi who first discovered the relevance of monads in (functional) programming. Phil Wadler's work has been immensly influential and he contributed a great deal of original ideas, but it just wasn't him who discovered what you are talking about. He popularized monads for functional programming very successfully, but that's a different thing. $\endgroup$ – Andrej Bauer Oct 24 '18 at 15:06
14
$\begingroup$

You should be more precise. When you say that f(x), f a and m >>= f are "the same", that does not make sense as written. f(x) and f a cannot be the same, they do not even use the same variables. Did you mean to compare f(u), f u and u >>= f? It is true that f(u) and f u are the same thing, but u >>= f is not. If f has type a -> m b (where m is the monad) then

  • in f u the type of u must be a, but
  • in u >>= f the type of u must be m a

So the types don't even match. Furthermore, if you look at concrete examples, you will see that >>= is not "just notation". It actually does things.

If we now look at the left identity law

return u >>= f  ≣  f u

we see that we cannot just rewrite the left-hand side to f u, or even f (return u). We must take into account what return and >>= do in a specific case. For instance, in the list monad we define

return x = [x]

and

(xs >>= f) = concat (map f xs)

The left identity law holds because of how concat and map work:

return x >>= f      ≣
[x] >>= f           ≣
concat (map f [x])  ≣
concat [f x]        ≣
f x

The above calculation was not just "notation"!

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.