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