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 Eq instance.) Regards, apfelmus