[Haskell-cafe] Specification for Eq?
rl at cse.unsw.edu.au
Sun Mar 16 21:36:36 EDT 2008
> 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
> "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-Cafe