[Haskell-cafe] Specification for Eq?

Roman Leshchinskiy rl at cse.unsw.edu.au
Sun Mar 16 21:36:36 EDT 2008

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?


More information about the Haskell-prime mailing list