proposal: user-defined equality predicates

[Fergus Henderson]

Hi,

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.

-----------------------------------------------------------------------------

User-defined equality predicates
********************************

   When defining abstract data types, often it is convenient to use a
non-canonical representation -- that is, one for which a single
abstract value may have more than one different possible concrete
representations.  For example, you may wish to implement an abstract
type `set' by representing a set as an (unsorted) list.

     :- module set_as_unsorted_list.
     :- interface.
     :- type set(T).
     
     :- implementation.
     :- import_module list.
     :- type set(T) ---> set(list(T)).

In this example, the concrete representations `set([1,2])' and
`set([2,1])' would both represent the same abstract value, namely the
set containing the elements 1 and 2.

   For types such as this, which do not have a canonical representation,
the standard definition of equality is the desired one; we want
equality on sets to mean equality of the abstract values, not equality
of their representations.  To support such types, Mercury allows
programmers to specify a user-defined equality predicate for
user-defined types:

     :- type set(T) ---> set(list(T))
     	where equality is set_equals.

Here `set_equals' is the name of a user-defined predicate that is used
for equality on the type `set(T)'.  It could for example be defined in
terms of a `subset' predicate.

     :- pred set_equals(set(T)::in, set(T)::in) is semidet.
     set_equals(S1, S2) :-
     	subset(S1, S2),
     	subset(S2, S1).

   A type declaration for a type T may contain a `where equality is
EQUALITYPRED' specification only if the following conditions are
satisfied:

   * T must be a discriminated union type; it may not be an equivalence
     type

   * EQUALITYPRED must be the name of a predicate with type `pred(T,
     T)' and mode `(in, in) is semidet'.

   Types with user-defined equality can only be used in limited ways.
Because there multiple representations for the same abstract value, any
attempt to examine the representation of such a value is a conceptually
non-deterministic operation.  In Mercury this is modelled using
committed choice nondeterminism.

   The semantics of a specifying `where equality is EQUALITYPRED' on
the type declaration for a type T are as follows:

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

   * If the program contains any deconstruction unification or switch
     on a variable of type T that cannot fail, then that operation has
     determinism `cc_multi'.

   * In addition to the usual equality axioms, the declarative
     semantics of the program will contain the axiom `X = Y <=>
     EQUALITYPRED(X, Y)' for all X and Y of type `T'.

   * Any `(in, in)' unifications for type T are computed using the
     specified predicate EQUALITYPRED.

   * EQUALITYPRED should be an equivalence relation; that is, it must be
     symmetric, reflexive, and transitive.  However, the compiler is
     not required to check this(1).

   ---------- Footnotes ----------

   (1)  If EQUALITYPRED is not an equivalence relation, then the
program is inconsistent: its declarative semantics contains a
contradiction, because the additional axioms for the user-defined
equality contradict the standard equality axioms.  That implies that the
implementation may compute any answer at all (*note Semantics::.), i.e.
the behaviour of the program is undefined.

-----------------------------------------------------------------------------

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