proposal: user-defined equality predicates

[Andrew Bromage]

G'day.

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

I must admit I'm a bit biassed here and this will probably seem like a
scathing attach on the scheme, but basically I'm a bit uneasy about
using the same notation for unification as for equality, which to my
mind are different concepts.

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.

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

Violating the second property becomes an issue because unification in
a source program does not necessarily involve an explicit call to
=/2.  For example:

:- type foo where equality is foo_equals.

:- pred test_foo(foo :: in, foo :: in, foo :: in, foo :: in) is semidet.
test_foo(X, Y, Y, X).

p(...) :-
	generate_foo_which_makes_equality_predicate_loop(A),
	generate_foo_which_makes_equality_predicate_terminate(B),
	test_foo(A, B, B, A).

The termination behaviour of p now depends on which order the head
unifications of test_foo are performed.  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.  Incidentally, this is almost precisely the same semantic
problem that occurs with Miranda's repeated-variable pattern matching.

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

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

That's all off the top of my head.

Cheers,
Andrew Bromage