[m-dev.] Re: proposal: user-defined equality predicates

[Andrew Bromage]

G'day.

Peter Schachte wrote:

> My rationale for wanting this is that non-canonical types don't work in
> Mercury (or any other logic programming language I know of).  Fergus'
> set-as-unordered-list example illustrates it quite well.

I understand why implementing sets as unordered lists and defining
equality on them in a nice way is a good idea.  However I think that
it is incorrect to overload =/2 in this way.  What I think would be
better is to handle this in type classes...

> If sets are
> implemented as unordered lists, *users* of that type have to be very
> careful never to unify two such entities, or they may get the wrong
> result.

...with perhaps some new feature to prevent people from using
unification/compare/whatever where it is not meaningful to do so.

> > 	- (X = Y) => (p(X) <=> p(Y))
> 
> Aside from the caveat Fergus put in the footnote, and aside from problems 
> the compiler will complain about when you have a goal that can fail after 
> a deconstruction (which will be cc_multi) I think this property is
> maintained.  I'm sure Fergus can argue this more convincingly.

Some code speaks a thousand words, so here goes.  Here's a new
replacement for the `unit' type implemented using the current
installed compiler and using ideas from the proposed equality
system:

<< new_unit.m
:- module new_unit.
:- interface.

:- type new_unit.

:- pred new_unit_equals(new_unit :: in, new_unit :: in) is semidet.

:- func new_unit_1 = new_unit.
:- func new_unit_2 = new_unit.
:- func f(new_unit) = int is det. % Should this be cc_multi?

:- implementation.

:- type new_unit
        --->    new_unit(int).
        % where equality is new_unit_equals.

	% This is indeed an equivalence relation.  It also
	% encapsulates the intuitive meaning of `unit'.
new_unit_equals(_X, _Y).

	% Must deconstruct using this function only.
:- func deconstruct_new_unit(new_unit) = int is cc_multi.
deconstruct_new_unit(new_unit(X)) = X.

new_unit_1 = new_unit(1).
new_unit_2 = new_unit(2).
f(NewUnit) = deconstruct_new_unit(NewUnit).
>>

<< test.m
:- module test.

:- interface.
:- import_module new_unit, io.

:- pred main(io__state :: di, io__state :: uo) is det.

main -->
        ( { new_unit_equals(new_unit_1, new_unit_2) } ->
                io__write_string("X = Y\n")
        ;
                io__write_string("X \\= Y\n")
        ),
        ( { f(new_unit_1) = f(new_unit_2) } ->
                io__write_string("f(X) = f(Y)\n")
        ;
                io__write_string("f(X) \\= f(Y)\n")
        ).
>>

And the output is...

<<
X = Y
f(X) \= f(Y)
>>

Either the current determinism checker inferred the wrong determinism
for f (should be cc_multi) or det functions are no longer single valued
under the new scheme.

> > 	- It always terminates.  If you ignore higher-order values.
> 
> and functions.

Okay, qualification: unifying two variables always terminates.
Unifying with a function is unifying with the result of a call.

Cheers,
Andrew Bromage