Conor McBride wrote:
Hi
On 14 Mar 2008, at 03:48, Roman Leshchinskiy wrote:
Adrian Hey wrote:
I would ask for any correct Eq instance something like the law:
(x==y) = True implies x=y (and vice-versa)
which implies f x = f y for all definable f
which implies (f x == f y) = True (for expression types which are
instances of Eq). This pretty much requires structural equality
for concrete types. For abstract types you can do something different
provided functions which can give different answers for two "equal"
arguments are not exposed.
How do you propose something like this to be specified in the language
definition? The report doesn't (and shouldn't) know about abstract types.
Why not? Why shouldn't there be at least a standard convention,
if not an abstype-like feature for establishing an abstraction
barrier, and hence determine the appropriate observational
equality for an abstract type?
Adrian's original question/proposal was about the language report. I'm
only pointing out that all other considerations aside, it's not clear
how to distinguish between the implementation part of the ADT and
everything else in the report.
So you can either require your law to hold everywhere, which IMO
isn't a good idea, or you don't require it to hold. From the language
definition point of view, I don't see any middle ground here.
Why not demand it in the definition, but allow "unsafe" leaks
in practice? As usual. Why are you so determined that there's
nothing principled to do here? People like to say "Haskell's
easy to reason about". How much of a lie would you like that
not to be?
I'm not sure what you mean here. 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?
"Unsafe leaks" are ok as long as they are rarely used. If you have to
resort to unsafe leaks to define an ADT, then something is wrong.
Also, when you talk about definable functions, do you include things
like I/O? What if I want to store things (such as a Set) on a disk? If
the same abstract value can have multiple representations, do I have
to convert them all to some canonical representation before writing
them to a file?
Canonical representations are not necessary for observational
congruence. Representation hiding is enough.
I beg to disagree. 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.
Actually, we don't even need the disk. What about ADTs which implement
Storable, for instance?
What would be so wrong with establishing a convention
for saying, at each given type
(1) this is the propositional equivalence which
we expect functions on this type to respect
(2) here is an interface which respects that
equivalence
(3) here are some unsafe functions which break
that equivalence: use them at your own risk
My (probably erroneous) understanding of the above is that you propose
to call (==) "propositional equivalence" and to require that for every
type, we define what that means. To be honest, I don't quite see how
this is different from saying that the meaning of (==) should be
documented for every type, which I wholeheartedly agree with. But the
"unsafe" bit really doesn't make sense to me.
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?
To summarise my views on this: an Eq instance should define a meaningful
equivalence relation and be documented. Requiring anything beyond that
just doesn't make sense to me.
Roman
_______________________________________________
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
