[Haskell-cafe] Re: (flawed?) benchmark : sort

[Luke Palmer]

On Thu, Mar 13, 2008 at 3:02 AM, Adrian Hey <ahey at iee.org> wrote:
>  The report doesn't state that for all Ints, (x==y = True) implies that
>  x=y. There's no reason to suppose the Int instance is in any way
>  special, so do you really seriously consider the possibility that
>  this might not hold in your Int related code?
>
>  if (x==y) then f x else g x y
>
>  might not mean the same as..
>
>  if (x==y) then f y else g x y

Of course not :-).  However, on what grounds am I to assume that these
two will be semantically equivalent for instances other than Int?
Int *is* special insofar as its implementation of Eq differs from that
of other types (of course, all other instances of Eq are special then,
too).  So it's reasonable that == means observational equivalence for
Int but not for other types, since it's possible to implement them
that way and there is no (explicitly stated) law which requires it.

But I agree that Eq should have some laws, just maybe not
observational equivalence because it is very limiting from a user's
perspective (that is, if I have a data type, requiring observational
equivalence makes it much less likely that I will be able to write an
instance of Eq, even if it makes sense in some stretch of the
imagination).

Saying that it's reasonable for everyone, everywhere to assume that Eq
means what you want it to mean is a stretch.  I believe every for
function I've written which was polymorphic in Eq it would have
sufficed for Eq to be any equivalence relation. What reason do I have
to restrict the users of my functions to those who can implement
observational equivalence?

But I'm just blabbering.  Here's my position on the issue with an
argument for why I think it's a good one:

Eq should be allowed to be any equivalence relation, because there are
many data types for which it is impossible to satisfy the constraint
of observational equivalence, thus reducing the usefulness of data
structures written over types with Eq.  On the other hand, (and this
is anecdotal), no data structures have been unable to cope with Eq not
implying observational equivalence.

Here's another argument.  Since Eq has no stated laws in the report,
give Eq no assumptions*, and allow the community to create an empty
subclass of Eq (ObsEq, say) which documents the necessary laws.  Then
a data structure which relies on the observational equivalence
property can specify it explicitly.

But really the thing that makes me choose this position is that it
sucks not to be able to use someone's code only because it is
impossible to satisfy instance laws, even though the code would be
perfectly reasonable anyway (though it isn't a strong argument,
consider the case of the broken ListT, still, it's enough to convince
me for the time being).

* No assumptions at all would be strange, but also okay with me, as
long as functions which rely on Eq specify that they need it to
conform to certain laws.  But I consider equivalence relation
reasonable because (1) everyone here seems to be on common ground that
it should *at least* be that, and (2) all the prelude functions on Eq
assume that (and note that none assume obs. eq.).  Indeed, "group" is
almost meaningless if Eq imples obs. eq.

Luke