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

[Fergus Henderson]

Andrew Bromage, you 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...

(Terminology nit: we're not really overloading =/2.  We're just defining
its semantics when applied to different types.)

You can think of the proposed user-defined equality in terms of type classes.
By default, there is an implicit instance declaration for every user-defined
type that defines equality on that types.  The `where equality is ...'
declaration just overrides this default, so that the implicit instance
declaration uses the specified equality predicate rather than the standard
structural equality.

Note that even if we had type classes, we would still want these implicit
instance declarations.  And for reasons of convenience, as well as for
backwards compatibility, we want them to be the default.

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

This would be nice in some ways, but it would be inconvenient,
causes problems for backwards compatibility, and interacts badly
with the mode system.  I'm willing to break `list__sort/3', but
I'm not really willing to break `append/3'.

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

No.  If it were cc_multi, the compiler ought to complain, since
functions are not allowed to be cc_multi, except in reverse modes.
(But the current compiler doesn't complain about that, I know).

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

That is an error.  It should be a predicate, not a function,
because functions mustn't be cc_multi.  (Also, see my other mail.)
Change it to

	:- pred deconstruct_new_unit(new_unit::in, int::out) is cc_multi.
	deconstruct_new_unit(new_unit(X), X).

Note that when the `where equality is' declaration is supported, the
deconstruction will be inferred cc_multi, so you can't declare it `det'.

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

Change that to

	f(NewUnit) = R :- deconstruct_new_unit(NewUnit, R).

That is an error, because f/1 is declared det, but
deconstruct_new_unit/2 is cc_multi.

> Either the current determinism checker inferred the wrong determinism
> for f (should be cc_multi)

Yes, it did -- that's because `where equality is' is not yet supported,
and so the compiler thinks the deconstruction is det, whereas really it
is cc_multi.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>   |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>   |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3         |     -- the last words of T. S. Garp.