On Thu, Mar 13, 2008 at 3:02 AM, Adrian Hey
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