Group: comp.lang.haskell · Group Profile
Author: Vesa KarvonenVesa Karvonen Date: Apr 1, 2008 05:29
> On 1 Apr, 11:03, Gareth McCaughan pobox.com> wrote:>> "andrea" wrote:
>>
>> [me:]
>>
>>>> If instead you take x == 10 then you should get the right types.
>>>> (In the Maybe monad, return == Just.)
>>
>> [Andrea:]
>>
>>> return x == Just x
>>> of course works, but it's not the monad law I think...
>>
>> Why do you think that, and what do you think *is* the
>> monad law?
> Ok this
> *Transform List> (return 10 >>= Just) == Just 10
> True
> Looks more like the "proof" of the law, doesn't it?
No, your example is not a proof of the left identity law
return x >>= f = f x
for arbitrary x and f, which is what I assume you are trying to prove.
One problem with your example is that you use a specific f. Your example
would pass if one would define
return x = Just x
Nothing >>= _ = Nothing
Just x >>= _ = Just x
but the above definitions do not satisfy the left identity law, so your
example is not a sufficient condition to prove the left identity law for
the maybe monad.
The maybe monad is defined as:
return x = Just x
Nothing >>= _ = Nothing
Just x >>= f = f x
To prove the left identity law for the maybe monad, one simply needs to
observe that
return x >>= f (by definition of return)
= Just x >>= f (by definition of >>=)
= f x
which proves it.
-Vesa Karvonen
| 
