[m-dev.] user-defined equality on equivalence types

[Zoltan Somogyi]

On 02-Mar-2000, David Glen JEFFERY <dgj at cs.mu.OZ.AU> wrote:
> `equivalent in all respects' is a property worth preserving, IMHO, and this
> means that equality should also be equivalent.

I think that "equivalent in all respects" is a property worth preserving
*only in some contexts*; in certain contexts, this property is already
violated. In particular, when an exported abstract type is defined by an
equivalence internal to its defining module, references to the abstract
type in other modules should not be compatible with the type that the
abstract type is equivalent to. If they were, the abstraction barrier
would be meaningless.

The property that may be worth preserving is that equivalence types
"are equivalent in all respects *in scopes where the equivalence type
is visible*" (from the reference manual).

There are other considerations, too. If we go ahead with a language extension
that allows programmers to define a prettyprinter for each type, then the
question arises whether one should be able to attach such a prettyprinter
to an equivalence type. A good argument can be made that the answer should be
yes. While the right prettyprinter for the type assoc_list(string, int)
would produce results such as ["banana" - 1, "apple" - 2, "orange" - 3],
for the type map(K,V) == assoc_list(K,V), one may want the same data to yield
{"apple" -> 2, "banana" -> 1, "orange" -> 3} (since for a map, the order
doesn't matter, one may want to standardize the order).

We now have two mechanisms for making one type "sortof" equivalent to another:
equivalences and notag types. I think what you are arguing for is that
programmers should be encouraged to use t1 == t2 only when t1 is a shorthand
for t2, but the programmer expects values of t1 and t2 to behave the same way
in all aspects; if t1 has an intended semantics that differs from t2 in the
smallest detail, they should be encouraged to use notag types instead.
(The manual does not currently contain this encouragement; in fact, it does
not mention notag types at all, as far as I can see. Such encouragement would
in effect commit all future Mercury implementations to implement notag types
in a way that is as efficient as equivalence types.) 

That is certainly a defensible position, and I think it is possible it would
be my preferred choice, but I think we should examine other alternatives first
as well. I can see two right off.

Alternative 1 is the one I outlined in my answer to David's email: one can
attach user-defined equality preds to equivalence types, and the one that
applies is the equality appropriate to the closest ancestor of the types
of the two values being unified.

Alternative 2 is to allow users to attach user-defined equality preds to
equivalence types, but outlaw all unifications between two values
of different but equivalent types except assignments (including those
implicit in parameter passing).

Zoltan.
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------