“Left identity” of Monad laws in Haskell is wrong

Question

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" `

Answer 1

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"!