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?
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,
> Haskell-Cafe mailing list
> [hidden email] > http://www.haskell.org/mailman/listinfo/haskell-cafe >
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 =)
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
> So you're either not taking (>=>) as primitive or you're stating the
> 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
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
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:
1. m :: * -> *
2. return :: a -> m a
3. (<=<) :: (b -> m c) -> (a -> m b) -> (a -> m c)
1. return <=< f === f <=< return === f
2. (f <=< g) <=< h === f <=< (g <=< h)
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.
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)
then the naturality of return is precisely its free theorem, and ditto
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 =)
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 ;)