[Haskell-cafe] Specification for Eq?
apfelmus
apfelmus at quantentunnel.de
Fri Mar 14 13:15:34 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 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
More information about the Haskell-Cafe
mailing list