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

[Fergus Henderson]

Andrew Bromage, you wrote:
> >I propose to extend Mercury to support user-defined equality predicates
> >for user-defined types.  The following is a proposed new chapter for the
> >Mercury Language Reference Manual describing this feature.  It is probably
> >a bit short on rationale and examples, but please let me know what you think.
>                 ^^^^^^^^^
> I'd like to see some of this. :-)
> 
> What does this scheme buy you over an "equality" type class, and when
> we eventually do get type classes, does it make sense for Mercury to
> have these two solutions to the same problem?

Type classes and user-defined equality predicates really solve different
problems.  The problem that user-defined equality predicates address
is the problem of types that do not have a single representation for
each abstract value.  Probably the feature should be described as
"non-canonical types" rather than "user-defined equality predicates";
the reason I didn't do that is that I don't really like the term
"non-canonical type" much (any suggestions for a better alternative??).

> ... I'm a bit uneasy about
> using the same notation for unification as for equality, which to my
> mind are different concepts.

In a pure logic language, these concepts should be the same.
Unification should reflect the programmer's declarative notion of equality.

> Unification has the following two properties which IMO are important to
> maintain, but the compiler cannot ensure:
> 
> 	- (X = Y) => (p(X) <=> p(Y))
> 	  This is the biggie.  It's not enough to impose the property
> 	  that =/2 is an equivalence relation.  You have to ensure that
> 	  X = Y implies that X and Y are interchangable EVERYWHERE in
> 	  the ADT's interface.

Right.  This problem is the reason why every discussion I've had on
this topic over the last few years has ended in "oh, well, non-canonical
types would be nice, but I can't see any way to do them cleanly...".

The solution to this problem is to make deconstructions cc_multi.
Any time you attempt to examine the representation, then conceptually
speaking the implementation non-deterministically picks a representation.
This ensures that (X = Y) => (p(X) <=> p(Y)).

<happy smile>

To make this all work, the implementor of the ADT will need to insert
something equivalent to `cc_cast' in various places, so that the
cc-ness is isolated in the implementation, and doesn't escape out
to the interface.  The compiler won't be able to check those.
But I think this situation is better, because (a) the cc_casts will
syntactically clear, so it is easy for the reader to verify them
and (b) only the implementor of the ADT has to worry about it.
Previously, if you wrote an ADT and implemented it with a non-canonical
representation, it was the users responsibility to call foo_equal
rather than =/2, or risk getting wrong results, and furthermore
calls to =/2 could be hidden as calls to implied modes, etc.,
so it was basically very difficult to find them.

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

I think this will also be the case for any reasonable user-defined
equality predicate.  So I don't see this causing any signiciant
problems in practice.

> The termination behaviour of p now depends on which order the head
> unifications of test_foo are performed.

That can already be the case:

	test_foo(0, function_which_loops).

	p(...) :-
		test_foo(1, _).

I'm not sure whether the Mercury Language Reference Manual
is clear about this point, but in general the idea is that
if you use the strict sequential semantics, then head unifications
are performed left-to-right, and if you use the commutative
semantics, then the order is unspecified.

> We currently don't have this
> problem because any sequence of unifications can be reordered (so long
> as they still satisfy mode constraints) with no semantic or operational
> difference.

Not quite.  Unifications which are function calls can't be reordered,
if you are using the strict sequential semantics.

> I also think that a `(ui, ui) is semidet' (at least) mode makes
> sense. :-)

Mmm. 

We can get away with having mode-checking of unifications allow
the `(ui, ui)' mode, but having the compiler just generate a call
to the `(in, in)' mode of the user-defined predicate.  This is safe,
because the predicate has no output variables, thus if there are
no aliases before the call, there can be no aliases after the call.
The only potential trouble is that it might cause problems with
tabling or in other circumstances where a reference to a value
persists after a call.

In general it would be better for the implied modes to go the
other way (i.e. `ui' implies `in'), though.

> >   * If the program contains any deconstruction unification or switch
> >     on a variable of type T that could fail, other than unifications
> >     with mode `(in, in)', then it is a compile-time error.
> 
> Including in the ADT implementation?

Yep.  In fact in the case of ADTs, the type will be an abstract type,
so this error could _only_ happen in the ADT implementation.

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