[Haskell-cafe] Specification for Eq?

[apfelmus]

Roman Leshchinskiy wrote:
> 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?

"for all exported f"
"(except functions whose names are prefixed with 'unsafe')"

While not perfect, I think that this is a reasonable specification of 
"observational equality for ADTs". (Whether all  Eq  instance should 
behave that way is another question.)

Note that if the ADT abstraction would be done via existential types 
instead of namespace control, we could honestly say "for all f".

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

The trick here is to blame any observable differences on the 
nondeterminism of the IO monad

   serialize :: MyADT -> IO String

It only guarantees to print out a "random" representation. Of course, in 
reality, serialize  just prints the internal representation at hand, but 
we may not know that.

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

Thanks for throwing in an example :) And a good one at that. So, 
alpha-equivalence is a natural  Eq  instance, but not an observational 
equivalence. Are there other such good examples? On the other hand, I'm 
not sure whether the Prelude functions like  nub  make sense / are that 
useful for alpha-equivalence. Furthermore,  Expr  is not an  Ord  instance.

(Of course, one could argue that  Var String  is "the wrong way" or "a 
very unsafe way" to implement stuff with names. For instance, name 
generation needs a monad. There are alternatives like De Bruijn indices 
and even representations based on parametric polymorphism. But I think 
that this doesn't touch the issue of alpha-conversion being a natural 
Eq  instance.)


Regards,
apfelmus