A question about "monad laws"

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
68 messages Options
1234
Reply | Threaded
Open this post in threaded view
|

Re: A question about "monad laws"

Dan Weston
Not to be picky, but where did you hear that (==) established an
equivalence relation? Not I expect from the Haskell98 Report!

The only law I can find there is that

   x /= y iff not (x == y)

So, the definition  x == y = False
                     x /= y = True

would be perfectly legitimate, making x /= x = True, which kind of ruins
the equivalence relation thing, no?

Dan

Wolfgang Jeltsch wrote:

> Am Mittwoch, 12. März 2008 00:53 schrieb askyle:
>> […]
>
>> So if floating point (==) doesn't correspond with numeric equality, it's
>> not FP's fault, but ours for expecting it to do!
>
> No, I think, it’s the Prelude’s fault to define (==) as “floating point
> equality”.  We should us a different identifier like floatingPointEq.  (==)
> is expected to be an equivalence relation.  (I think I already said this.)
>
>> […]
>
> Best wishes,
> Wolfgang
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: A question about "monad laws"

askyle
In reply to this post by Wolfgang Jeltsch-2
Wolfgang Jeltsch-2 wrote
No, I think, it’s the Prelude’s fault to define (==) as “floating point equality”.
My bad, I meant IEEE (==) when I said it was "our" fault. I concur that the
Prelude is at fault for using the (==) symbol for FP equality. Even if you don't
demand from (==) to be an equivalence, you're giving a pure functional type
to an impure operation (e.g because of SNaNs)

My point was that since Haskell has a known and established mechanism for
delimiting impurity, it seems as a shame not to use it to add some rigour to the
myth-ridden, poorly understood floating point world. We need good FP for FP =)
Reply | Threaded
Open this post in threaded view
|

Re: A question about "monad laws"

askyle
In reply to this post by ajb@spamcop.net
ajb-2 wrote
Define:
     f >=> g = \x -> f x >>= g
So you're either not taking (>=>) as primitive or you're stating the additional
property that there exists (>>=) such that f >=> g  === (>>= g) . f
(from which you can easily show that (f . g) >=> h === (f >=> h) . g ).

A presentation of the monad laws based on (>=>) (I prefer (<=<) since it meshes
better with (.) ) should (IMHO) regard (>=>) as primitive and state its needed properties
whence one can derive all other formulations (Note that he Identity law then requires the
existence of return as another primitive).

That done, you define (>>=), fmap and the rest in terms of (<=<) :

(>>=) = flip (<=< id)               -- I like to put it as (>>= g) = (g <=< id)
fmap f = (return . f) <=< id
Reply | Threaded
Open this post in threaded view
|

Re: A question about "monad laws"

ajb@spamcop.net
G'day all.

Quoting askyle <[hidden email]>:

> So you're either not taking (>=>) as primitive or you're stating the
> additional
> property that there exists (>>=) such that f >=> g  === (>>= g) . f
> (from which you can easily show that (f . g) >=> h === (f >=> h) . g ).

If you wanted to prove that bind is natural, you would need to define
bind, no?

Cheers,
Andrew Bromage
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: A question about "monad laws"

Wolfgang Jeltsch-2
In reply to this post by Dan Weston
Am Donnerstag, 13. März 2008 21:10 schrieben Sie:
> Not to be picky, but where did you hear that (==) established an
> equivalence relation?

I think that’s the way it should be according to most Haskeller’s opinion.  It
might be true that the Haskell 98 report doesn’t say so but I think that many
library types and functions (Data.Set stuff, for example) rely on this.  A
future standard should state laws an instance has to obey for every class it
introduces.

> […]

Best wishes,
Wolfgang
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: A question about "monad laws"

askyle
In reply to this post by ajb@spamcop.net
ajb-2 wrote
If you wanted to prove that bind is natural, you would need to define bind, no?
Yup: bind f = f <=< id         -- whence you can say (>>=) = flip bind
My point is that (as far as I can see) you cannot prove the properties of bind
by only assuming identity and associativity for (<=<). You need some way to
relate (<=<) to normal composition.

To be more explicit:

Given:
1. m :: * -> *
2. return :: a -> m a
3. (<=<) :: (b -> m c) -> (a -> m b) -> (a -> m c)
such that:
1. return <=< f === f <=< return === f
2. (f <=< g) <=< h === f <=< (g <=< h)

Define:
bind f = f <=< id
(>>=) = flip bind
fmap f = bind (return . f)
join = bind id

Show the monad laws hold, either for (return,bind), (return,(>>=)) or
(fmap,return,join) (in the latter case, there's also showing that fmap is
a functor and return and join are natural transformations).

If someone can show it can be done without also assuming:
3. (f <=< g) . h === f <=< (g . h)
I'll stand corrected.
Reply | Threaded
Open this post in threaded view
|

Re: A question about "monad laws"

ajb@spamcop.net
G'day all.

Quoting askyle <[hidden email]>:

> Yup: bind f = f <=< id         -- whence you can say (>>=) = flip bind

Ah, yes.

> My point is that (as far as I can see) you cannot prove the properties of
> bind by only assuming identity and associativity for (<=<).

One thing that may help is that if you can prove that fmap is sane:

     fmap (f . g) = fmap f . fmap g

then the naturality of return is precisely its free theorem, and ditto
for bind.

So perhaps this law:

     (f <=< g) . h === f <=< (g . h)

is actually the fmap law in disguise?

Cheers,
Andrew Bromage
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: A question about "monad laws"

askyle
ajb-2 wrote
One thing that may help is that if you can prove that fmap is sane:
     fmap (f . g) = fmap f . fmap g
I get stuck after expanding the rhs into:
((return . f) <=< id) . ((return . g) <=< id)

ajb-2 wrote
then the naturality of return is precisely its free theorem, and ditto
for bind.
Care to develop? IIRC the free theorems have a certain parametericity
requirement (which probably holds in all interesting cases, but still sounds
like an additional assumption). I'm not too familiar with these, so a link
would be appreciated =)

ajb-2 wrote
So perhaps this law:
     (f <=< g) . h === f <=< (g . h)
is actually the fmap law in disguise?
Could be. Maybe the fmap law is this one in disguise ;)
1234