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

[Thomas Conway]

On Thu, Mar 02, 2000 at 02:08:06PM EST, Zoltan Somogyi wrote:
> At the moment, we allow user-defined equality only on discriminated union
> types, but not on equivalence types. This is a pain in defining ADTs such
> as sets as unsorted lists, since it requires you to wrap a functor around
> the list, even though there is no runtime efficiency penalty for using a
> notag type versus an equivalence type.
> 
> The reason for that restriction was that equivalence types were unfolded
> early. After Rob's proposed change, that reason will no longer apply, and
> I think we should then lift that restriction. The rtti changes required
> will be fairly trivial.
> 
> Comments?

I think it sounds like a reasonable idea.

Let me play the devil's advocate for a moment and suggest that if you're
redefining equality on a type, then making it non-unifiable with the
existing type seems like a good idea.  eg:

	:- type a ---> ....

	:- type b == a.

	:- pred p(a, b).

	p(X, X).

seems like a fine thing to do if `a' and `b' have the same definition
of equality, but what is going to if they have different definitions
of equality?

Actually, having stated the against case, I'm not so sure it is a good
idea after all.

-- 
 Thomas Conway )O+     Every sword has two edges.
     Mercurian            <conway at cs.mu.oz.au>
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------