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

[Roman Leshchinskiy]

Conor McBride wrote:
> 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?

Adrian's original question/proposal was about the language report. I'm 
only pointing out that all other considerations aside, it's not clear 
how to distinguish between the implementation part of the ADT and 
everything else in the report.

>>  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?

I'm not sure what you mean here. Should the report say something like "a 
valid Eq instance must ensure that x == y implies f x == f y for all f"? 
  Probably not, since this requires structural equality which is not 
what you want for ADTs. Should it be "for all f which are not part of 
the implementation of the type"? That's a non-requirement if the report 
doesn't specify what the "implementation" is. So what should it say?

"Unsafe leaks" are ok as long as they are rarely used. If you have to 
resort to unsafe leaks to define an ADT, then something is wrong.

>> 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.

I beg to disagree. If the representation is stored on the disk, for 
instance, then it becomes observable, even if it's still hidden in the 
sense that you can't do anything useful with it other than read it back. 
Actually, we don't even need the disk. What about ADTs which implement 
Storable, for instance?

> 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

My (probably erroneous) understanding of the above is that you propose 
to call (==) "propositional equivalence" and to require that for every 
type, we define what that means. To be honest, I don't quite see how 
this is different from saying that the meaning of (==) should be 
documented for every type, which I wholeheartedly agree with. But the 
"unsafe" bit really doesn't make sense to me.

As an example, consider the following data type:

data Expr = Var String | Lam String Expr | App Expr Expr

The most natural notion of equality here is probably equality up to 
alpha conversion and that's what I usually would expect (==) to mean. In 
fact, I would be quite surprised if (==) meant structural equality. 
Should I now consider the Show instance for this type somehow unsafe? I 
don't see why this makes sense. Most of the time I probably don't even 
want to make this type abstract. Are the constructors also unsafe? Why?

To summarise my views on this: an Eq instance should define a meaningful 
equivalence relation and be documented. Requiring anything beyond that 
just doesn't make sense to me.

Roman