Alexander Solla alex.solla at gmail.com
Thu Jun 21 16:34:30 CEST 2012

```On Thu, Jun 21, 2012 at 7:00 AM, George Giorgidze <giorgidze at gmail.com>wrote:
>
> >
> > Regarding antisymmetry, if I also define
> >
> > instance Ord Foo where
> >   (==) = (==) `on` a
> >
> > then would that count as satisfying the law?
>
> Probably, you mean here Eq instead of Ord.
>
> If a <= b and b <= a then a = b (antisymmetry)
>
> It all depends on what one means by "=". Opinions differ on this, see
> [1]. If we mean "==", which is a function to Bool, from the Eq class,
> then it does satisfy the antisymmetry law.
>
> But in this case, the question arises what are the laws that Eq
> instances should satisfy.
>
> Should it be that x == y implies x = y? But once again what does "="
> mean here. It depends on who you ask (once again see [1]).
>
>
These nits don't need to be picked.  The theory of equivalence relations is
extremely well understood.  This is a topic covered by the sophomore
mathematics level.

>
> But, my opinion is that if you can write a pure function f that can
> tell them apart (i.e., f x /= f y), I find it a very strange notion of
> equality.

There's your problem.  It is straight-forward to generate an equivalence
relation that can tell things apart with respect to a different equivalence
relation.  Equivalence relations do not need to agree!

If you really want to keep distinct equivalence relations apart
semantically, just use a newtype wrapper to explicitly "name" the relation.

> I am not saying that this is a trivial undertaking, but would be a
> more principled approach. It would require the Haskell community and,
> especially, standard library and language specification developers to
> agree on a suitable notion of equality that Eq instances should
> satisfy.
>

That has already happened.  A relation merely has to satisfy the
equivalence relation axioms.
-------------- next part --------------
An HTML attachment was scrubbed...