Hi On 14 Mar 2008, at 03:48, Roman Leshchinskiy wrote:
Adrian Hey wrote:
I would ask for any correct Eq instance something like the law: (x==y) = True implies x=y (and vice-versa) which implies f x = f y for all definable f which implies (f x == f y) = True (for expression types which are instances of Eq). This pretty much requires structural equality for concrete types. For abstract types you can do something different provided functions which can give different answers for two "equal" arguments are not exposed.
How do you propose something like this to be specified in the language definition? The report doesn't (and shouldn't) know about abstract types.
Why not? Why shouldn't there be at least a standard convention, if not an abstype-like feature for establishing an abstraction barrier, and hence determine the appropriate observational equality for an abstract type?
So you can either require your law to hold everywhere, which IMO isn't a good idea, or you don't require it to hold. From the language definition point of view, I don't see any middle ground here.
Why not demand it in the definition, but allow "unsafe" leaks in practice? As usual. Why are you so determined that there's nothing principled to do here? People like to say "Haskell's easy to reason about". How much of a lie would you like that not to be?
Also, when you talk about definable functions, do you include things like I/O? What if I want to store things (such as a Set) on a disk? If the same abstract value can have multiple representations, do I have to convert them all to some canonical representation before writing them to a file?
Canonical representations are not necessary for observational congruence. Representation hiding is enough.
This might be rather slow and is, IMO, quite unnecessary.
From a more philosophical points of view, I'd say that the appropriate concept of equality depends a lot on the problem domain.
It's certainly true that different predicates may respect different equivalence relations. The equivalence relation you call equality should be the finest of those, with finer representational distinctions abstracted away. What that buys you is a class of predicates which are guaranteed to respect equality without further ado...
Personally, I quite strongly disagree with restricting Eq instances in the way you propose. I have never found much use for strict structural equality (as opposed to domain-specific equality which may or may not coincide with the structural one).
...which is how we use equality when we think. I certainly don't think "strict structural equality" should be compulsory. In fact, for Haskell's lazy data structures, you rather need lazy structural simulation if you want to explain why cycle "x" = cycle "xx" What would be so wrong with establishing a convention for saying, at each given type (1) this is the propositional equivalence which we expect functions on this type to respect (2) here is an interface which respects that equivalence (3) here are some unsafe functions which break that equivalence: use them at your own risk ? Why is it pragmatically necessary to make reasoning difficult? I'm sure that wise folk out there have wise answers to that question which they don't consider to be an embarrassment. When representation-hiding is bliss, 'tis folly to be wise. All the best Conor