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 |
In reply to this post by Wolfgang Jeltsch-2
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 =) |
In reply to this post by ajb@spamcop.net
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 |
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 |
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 |
In reply to this post by ajb@spamcop.net
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. |
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 |
I get stuck after expanding the rhs into: ((return . f) <=< id) . ((return . g) <=< id) 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 =) Could be. Maybe the fmap law is this one in disguise ;) |
Free forum by Nabble | Edit this page |