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

[David Glen JEFFERY]

On 02-Mar-2000, Zoltan Somogyi <zs at cs.mu.OZ.AU> wrote:
> 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).

Of course. That is (part of) the passage from the reference manual that I
originally quoted, and my subsequent use of "equivalent in all respects" was
intended to refer to that passage.

> 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).

A reasonably compelling example, but I would argue that if you wanted your
pretty printer to behave differently, you should define 

:- type map(K, V) ---> map(assoc_list(K, V)) where....

> 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.

Yes, that's a fair summary of my position.

> 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. 

Indeed. My gut feeling is that we won't find an alternatives which gives
us so many benefits that I'd be prepared to sacrifice the idea that equivalence
types are equivalent in all respects (in scopes where the equivalence type is
visible). I'd be more than happy to be proven wrong, though.

> 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.

My main objection to this particular idea is that I imagine it may be
reasonably difficult for the programmer to predict exactly what is going on.
Just my instinct, though.

Note also that this proposal (as, I expect, will *any* others that throw away
the idea of simple syntactic equivalence) would mean that the compiler *must*
avoid expanding equivalence types. This is a significant drawback, IMHO.

> 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).

I realise that this is just a straw-man, but I really don't think it is
desirable (or feasible). We would have the situation that given, for example,
this equivalence:

:- type t(T) == list(T).

the following code would give a type error:

:- pred p(t(T), list(T)).
p(T, L) :-
	T = L.	% t(T) == list(T), therefore error

but this would not:

p(T, L) :-
	T1 = T,	% list(T) := t(T), therefore OK
	T1 = L. % list(T) == list(T), therefore OK

This seems more than a little weird to me...

So, to sum up my feelings on the issue, I would say that the notion of
equivalence types as being truly equivalent is a very appealing one.
You have shown a couple of quite compelling examples (sets as sorted lists,\
pretty printing), but the tradeoffs don't seem worth it to me, particularly
given that no-tag types are really so easy to use. As I have said before,
I think that making programmers use an extra functor where appropriate tends to
be a good thing as it encourages the programmer to be explicit about the
meaning of a value.


dgj
-- 
David Jeffery (dgj at cs.mu.oz.au) | If your thesis is utterly vacuous
PhD student,                    | Use first-order predicate calculus.
Dept. of Comp. Sci. & Soft. Eng.|     With sufficient formality
The University of Melbourne     |     The sheerist banality
Australia                       | Will be hailed by the critics: "Miraculous!"
                                |     -- Anon.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------