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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
