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