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

[Zoltan Somogyi]

On 02-Mar-2000, David Overton <dmo at ender.cs.mu.oz.au> wrote:
> What equality predicate would be used for something such as:
> 
> 	:- type my_int == int where equality is my_equality.
> 	:- pred p(int::in, my_int::in) is semidet.
> 	p(X, X).

Good question.

The obvious answer: the one for int.

The general case is more complex, because one can have a tree like this:

:- type t0.
:- type t1 == t0.
:- type t2 == t0.
:- type t3 == t1.
:- type t4 == t1.
:- type t5 == t2.
:- type t6 == t2.

When unifying two values of type ti and tj, one should apply the unification
algorithm appropriate for the closest common ancestor of ti and tj. For
example, for i=3 and j=4, this would be t1's, but for i=3 and j=6, it would nt
t0's. You'd have to do this for the type constructor, and recursively for its
arguments.

Of course, some of those equivalences may be behind abstraction barriers and
hence invisible. If the search for the closest common ancestor does not succeed
before coming to such a barrier, the unification would be disallowed.

The complexity of this scheme is a point against my proposal.

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