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

[David Glen JEFFERY]

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

Sounds like the Wrong Thing to me. Dave's example is a nice example of the
practical reasons why.

Consider the explanation of equivalence types from the language reference
manual:

	Mercury treats an equivalence type as an abbreviation for the type on
	the right hand side of the definition; the two are equivalent in all
	respects in scopes where the equivalence type is visible. 

`equivalent in all respects' is a property worth preserving, IMHO, and this
means that equality should also be equivalent.

Another way of thinking about it is that equivalence types are really just
syntactic sugar; if point in compilation at which they are expanded affects 
the meaning of your program, then you step away from the simple notion of
syntactic equivalence that we have been using. You would have to be very,
very careful about how you define things. Dave's example shows that
(even if you did give such a carefully constructed meaning to equivalences),
that the behaviour of the program would not necessarily to obvious to the
programmer (even if it were well defined).

I actually think that requiring the user to wrap a functor around things is
a good thing to do; using an extra functor makes explicit that values of this
type have a different interpretation than their unwrapped counterparts.


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