Next: Higher-order, Previous: Determinism, Up: Top [Contents]
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 representation. 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 not 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 (not including subtypes):
:- 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 comparison predicate can also be supplied.
:- type set(T) ---> set(list(T)) where equality is set_equals, comparison is set_compare. :- pred set_compare(builtin.comparison_result::uo, set(T)::in, set(T)::in) is det. set_compare(Result, Set1, Set2) :- promise_equivalent_solutions [Result] ( set_compare_2(Set1, Set2, Result) ). :- pred set_compare_2(set(T)::in, set(T)::in, builtin.comparison_result::uo) is cc_multi. set_compare_2(set(List1), set(List2), Result) :- builtin.compare(Result, list.sort(List1), list.sort(List2)).
If a comparison predicate is supplied and the unification predicate is omitted, a unification predicate is generated by the compiler in terms of the comparison predicate. For the ‘set’ example, the generated predicate would be:
set_equals(S1, S2) :- set_compare((=), S1, S2).
If a unification predicate is supplied without a comparison predicate, the compiler will generate a comparison predicate which throws an exception of type ‘exception.software_error’ when called.
A type declaration for a type ‘foo(T1, …, TN)’ may contain a ‘where equality is equalitypred’ specification only if it declares a discriminated union type or a foreign type (see Using foreign types from Mercury) and the following conditions are satisfied:
:- pred equalitypred(foo(T1, …, TN)::in, foo(T1, …, TN)::in) is semidet.
It is legal for the type, mode and determinism to be more permissive:
the type or the mode’s initial insts may be more general
(e.g. the type of the equality predicate
could be just the polymorphic type ‘pred(T, T)’)
and the mode’s final insts or the determinism may be more specific
(e.g. the determinism of the equality predicate
could be any of det
, failure
or erroneous
).
Types with user-defined equality can only be used in limited ways. Because there are 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 specifying ‘where equality is equalitypred’ on the type declaration for a type T are as follows:
cc_multi
.
cc_multi
or cc_nondet
will result in a run-time error.
A type declaration for a type ‘foo(T1, …, TN)’ may contain a ‘where comparison is comparepred’ specification only if it declares a discriminated union type or a foreign type (see Using foreign types from Mercury) and the following conditions are satisfied:
:- pred comparepred(builtin.comparison_result::uo, foo(T1, …, TN)::in, foo(T1, …, TN)::in) is det.
As with equality predicates, it is legal for the type, mode and determinism to be more permissive.
compare_eq(X, Y) :- comparepred((=), X, Y).
must be an equivalence relation; that is, it must be symmetric, reflexive, and transitive. The compiler is not required to check this.
compare_leq(X, Y) :- comparepred(R, X, Y), (R = (=) ; R = (<)). compare_geq(X, Y) :- comparepred(R, X, Y), (R = (=) ; R = (>)).
must be total order relations: that is they must be antisymmetric, reflexive and transitive. The compiler is not required to check this.
For each type for which the declaration has a ‘where comparison is comparepred’ specification, any calls to the standard library predicate ‘builtin.compare/3’ with arguments of that type are evaluated as if they were calls to comparepred.
A type declaration may contain a ‘where equality is equalitypred, comparison is comparepred’ specification only if in addition to the conditions above, ‘all [X, Y] (comparepred((=), X, Y) <=> equalitypred(X, Y))’. The compiler is not required to check this.
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 (see Formal semantics), i.e. the behaviour of the program is undefined.
Next: Higher-order, Previous: Determinism, Up: Top [Contents]