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"
"(except functions whose names are prefixed with 'unsafe')"
While not perfect, I think that this is a reasonable specification of
"observational equality for ADTs". (Whether all Eq instance should
behave that way is another question.)
Note that if the ADT abstraction would be done via existential types
instead of namespace control, we could honestly say "for all f".
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.
As an example, consider the following data type:
data Expr = Var String | Lam String Expr | App Expr Expr
The most natural notion of equality here is probably equality up to
alpha conversion and that's what I usually would expect (==) to mean. In
fact, I would be quite surprised if (==) meant structural equality.
Should I now consider the Show instance for this type somehow unsafe? I
don't see why this makes sense. Most of the time I probably don't even
want to make this type abstract. Are the constructors also unsafe? Why?
Thanks for throwing in an example :) And a good one at that. So,
alpha-equivalence is a natural Eq instance, but not an observational
equivalence. Are there other such good examples? On the other hand, I'm
not sure whether the Prelude functions like nub make sense / are that
useful for alpha-equivalence. Furthermore, Expr is not an Ord instance.
(Of course, one could argue that Var String is "the wrong way" or "a
very unsafe way" to implement stuff with names. For instance, name
generation needs a monad. There are alternatives like De Bruijn indices
and even representations based on parametric polymorphism. But I think
that this doesn't touch the issue of alpha-conversion being a natural
Haskell-Cafe mailing list