Some clarity please! (was Re: [Haskell-cafe] Re: (flawed?) benchmark : sort)

[Conor McBride]

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