[Haskell-cafe] Specification for Eq?

[Roman Leshchinskiy]

apfelmus wrote:
> 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"

This forces me to confine the implementation of my ADT to a single
module instead of a package. Also (just to be nitpicky :-), it doesn't 
deal with methods of classes of which my ADT is an instance since I 
don't export those.

It's quite interesting that so far in this discussion, nobody seems to
have to come up with a clear and practically useful (in this context, of
course) definition of observation. I suspect that this is because in 
practice, we can and, more importantly, want to observe a lot more than 
in theory. For instance, something like serialisation usually wouldn't 
even be mentioned in a theoretical paper about a data structure but is 
absolutely necessary for writing actual programs.

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

Hmm, I understand what you're saying but... So we go to all the trouble
of placing quite severe restrictions on (==) and now we can't even rely
on them when reasoning about effects?

Also, this requires that I artificially embed my perfectly pure 
serialisation function in IO. This doesn't really make reasoning about 
it easier but ultimately, isn't that what this is all about?

Roman