[m-rev.] for review: user-defined comparison
Simon Taylor
stayl at cs.mu.OZ.AU
Wed Feb 12 13:52:17 AEDT 2003
On 31-Oct-2002, Mark Brown <dougl at cs.mu.OZ.AU> wrote:
> On 29-Oct-2002, Simon Taylor <stayl at cs.mu.OZ.AU> wrote:
> > Estimated hours taken: 20
> > Branches: main
> >
> > Allow user-defined comparison functions using the syntax
> > :- type t ---> t where equality is t_equal, comparison is t_compare.
> > .
> > Index: doc/reference_manual.texi
> > ===================================================================
> > RCS file: /home/mercury1/repository/mercury/doc/reference_manual.texi,v
> > retrieving revision 1.259
> > diff -u -u -r1.259 reference_manual.texi
> > --- doc/reference_manual.texi 1 Oct 2002 08:13:26 -0000 1.259
> > +++ doc/reference_manual.texi 25 Oct 2002 06:42:19 -0000
> > @@ -3355,29 +3357,67 @@
> > subset(S2, S1).
> > @end example
> >
> > +A comparison predicate can also be supplied.
>
> Perhaps make it clearer that you may supply either or both. E.g.:
>
> A comparison predicate may also be supplied, or both an equality
> predicate and a comparison predicate may be supplied.
That's already described below.
> > +If a unification predicate is supplied without a comparison predicate,
> > +the compiler will generate a comparison predicate which throws an
> > +exception when called.
>
> It would be useful to document what exception is thrown.
Done.
> > +
> > A type declaration for a type @samp{foo(T1, @dots{}, TN)} may contain a
> > - at samp{where equality is @var{equalitypred}} specification only
> > -if the following conditions are satisfied:
> > + at samp{where equality is @var{equalitypred}, comparison is @var{comparepred}}
> > +specification only if the following conditions are satisfied:
>
> I think it would be better to separate these constraints into two lists:
> one for the constraints on equality preds and one for the constraints on
> comparison preds.
Done.
> > @@ -3427,6 +3467,15 @@
> > implementation may compute any answer at all (@pxref{Semantics}),
> > i.e.@: the behaviour of the program is undefined.}.
> >
> > + at item
> > +Any comparisons of type @var{T} are computed using the specified predicate
> > + at var{comparepred}.
> > +
> > + at item
> > + at var{comparepred} should be a partial order relation: that is
> > +it must be antisymmetric, reflexive and transitive. The
> > +compiler is not required to check this.
> > +
>
> This point should go in the constraints list, rather than the semantics
> list.
>
> Also, I'm not convinced that requiring a _partial_ order is the right
> constraint. Why not a total order? The mode of the comparison
> predicate implies that all pairs of elements are comparable anyway.
> Suggesting that they only need to be partial orders is misleading,
> because many library predicates (e.g. list__sort) depend on the order
> being total.
>
> Perhaps you mean that the order is partial because the predicate can
> throw an exception when the elements are not comparable? If so, this
> is an abuse of the notion of exception, IMHO. In a partial order (e.g.,
> the subset relation) it is perfectly normal to find two elements that
> are not comparable (e.g., sets {1} and {2}) -- it is not an exceptional
> circumstance at all -- so using an exception to indicate this is bad
> design.
>
> Finally, on a technical note, the adjectives "reflexive", etc, usually
> apply to binary operators but the comparison predicate has arity three,
> and you haven't explicitly stated what they mean in this context.
Fixed.
> > Index: library/builtin.m
> > ===================================================================
> > @@ -178,6 +180,9 @@
> > % unify(X, Y) is true iff X = Y.
> > :- pred unify(T::in, T::in) is semidet.
> >
> > +:- type unify(T) == pred(T, T).
> > +:- inst unify == (pred(in, in) is semidet).
> > +
> > :- type comparison_result ---> (=) ; (<) ; (>).
> >
> > % compare(Res, X, Y) binds Res to =, <, or >
> > @@ -191,6 +196,9 @@
> > :- mode compare(uo, ui, in) is det.
> > :- mode compare(uo, in, ui) is det.
> >
> > +:- type compare(T) == pred(comparison_result, T, T).
> > +:- inst compare == (pred(uo, in, in) is semidet).
> > +
>
> You should document the constraints on values of these types here, in
> addition to the reference manual.
>
> It would also be useful to document here the distinction between compare
> and comparison_pred, that is, that the former are used for the "where ..."
> part of type declarations.
Done.
I'll commit this soon unless there are any objections.
Simon.
Index: doc/reference_manual.texi
===================================================================
RCS file: /home/mercury1/repository/mercury/doc/reference_manual.texi,v
retrieving revision 1.269
diff -u -u -r1.269 reference_manual.texi
--- doc/reference_manual.texi 9 Feb 2003 08:09:53 -0000 1.269
+++ doc/reference_manual.texi 11 Feb 2003 03:48:01 -0000
@@ -89,8 +89,9 @@
safely use destructive update to modify that value.
* Determinism:: Determinism declarations let you specify that a predicate
should never fail or should never succeed more than once.
-* Equality preds:: User-defined types can have user-defined equality
- predicates.
+* User-defined equality and comparison::
+ User-defined types can have user-defined equality and
+ comparison predicates.
* Higher-order:: Mercury supports higher-order predicates and functions,
with closures, lambda expressions, and currying.
* Modules:: Modules allow you to divide a program into smaller parts.
@@ -100,7 +101,7 @@
* Semantics:: Declarative and operational semantics of Mercury
programs.
* Foreign language interface:: Calling code written in other programming
- languages from Mercury code
+ languages from Mercury code
* C interface:: The C interface allows C code to be called
from Mercury code, and vice versa.
* Impurity:: Users can write impure Mercury code.
@@ -2283,7 +2284,7 @@
@end example
As for type declarations, a predicate or function can be defined
-to have a given higher-order inst (@pxref{Higher-order modes} by using
+to have a given higher-order inst (@pxref{Higher-order modes}) by using
@code{`with_inst`} in the mode declaration.
For example,
@@ -3216,7 +3217,8 @@
satisfied, then the behaviour is undefined.
Note that specifying a user-defined equivalence relation
-as the equality predicate for user-defined types (@pxref{Equality preds})
+as the equality predicate for user-defined types
+(@pxref{User-defined equality and comparison})
means that the @samp{promise_only_solution/1} function
can be used to express more general forms of equivalence.
For example, if you define a set type which represents sets as unsorted lists,
@@ -3289,7 +3291,7 @@
Another reason is for doing I/O, which is allowed only in @samp{det}
or @samp{cc_multi} predicates, not in @samp{multi} predicates.
Another is for dealing with types that use non-canonical representations
-(@pxref{Equality preds}).
+(@pxref{User-defined equality and comparison}).
And there are a variety of other applications.
@c XXX fix semantics for I/O + committed choice + mode inference
@@ -3334,8 +3336,8 @@
@c ).
@c @end example
- at node Equality preds
- at chapter User-defined equality predicates
+ at node User-defined equality and comparison
+ at chapter User-defined equality and comparison
When defining abstract data types,
often it is convenient to use a non-canonical representation ---
@@ -3382,29 +3384,107 @@
subset(S2, S1).
@end example
+A comparison predicate can also be supplied.
+
+ at example
+:- type set(T) ---> set(list(T))
+ where equality is set_equals, comparison is set_compare.
+
+:- pred set_compare(comparison_result::uo, set(T)::in, set(T)::in) is det.
+set_compare(promise_only_solution(set_compare_2(Set1, Set2)), Set1, Set2).
+
+:- pred set_compare_2(set(T)::in, set(T)::in,
+ comparison_result::uo) is cc_multi.
+set_compare_2(set(List1), set(List2), Result) :-
+ compare(Result, list__sort(List1), list__sort(List2)).
+ at end example
+
+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 @samp{set} example,
+the generated predicate would be:
+
+ at example
+set_equals(S1, S2) :-
+ set_compare((=), S1, S2).
+ at end example
+
+If a unification predicate is supplied without a comparison predicate,
+the compiler will generate a comparison predicate which throws an
+exception of type @samp{require__software_error} when called.
+
A type declaration for a type @samp{foo(T1, @dots{}, TN)} may contain a
- at samp{where equality is @var{equalitypred}} specification only
-if the following conditions are satisfied:
+ at samp{where equality is @var{equalitypred}} specification only it declares
+a discriminated union type or a foreign type
+(@pxref{Using foreign types from Mercury}) and the
+following conditions are satisfied:
@itemize @bullet
@item
-The type @samp{foo(T1, @dots{}, TN)} must be a discriminated union type;
-it may not be an equivalence type
+ at var{equalitypred} must be the name of a predicate with signature
+ at example
+:- pred @var{equalitypred}(foo(T1, @dots{}, TN)::in,
+ foo(T1, @dots{}, TN)::in) is semidet.
+ at end example
+
+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 @samp{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 @samp{det}, @samp{failure} or @samp{erroneous}).
+
+ at item
+The equality predicate must be ``pure'' (@pxref{Impurity}).
@item
- at var{equalitypred} must be the name of a predicate which can
-be called with two ground arguments of type @samp{pred(foo(T1, @dots{}, TN))},
-and whose determinism in that mode is @samp{semidet}.
-Typically the equality predicate would have type
- at samp{pred(foo(T1, @dots{}, TN), foo(T1, @dots{}, TN)}
-and mode @samp{(in, in) is semidet}, but it is also 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 could be just the polymorphic type @samp{pred(T, T)})
-and the mode's final insts or the determinism may be more
-specific (e.g.@: the determinism could be any of @samp{det},
- at samp{failure} or @samp{erroneous}).
-The equality predicate must also be ``pure'' (@pxref{Impurity}).
+ at var{equalitypred} should be an equivalence relation; that is, it must be
+symmetric, reflexive, and transitive. However, the compiler is not required
+to check this at footnote{If @var{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 (@pxref{Semantics}),
+i.e.@: the behaviour of the program is undefined.}.
+
+ at end itemize
+
+A type declaration for a type @samp{foo(T1, @dots{}, TN)} may contain a
+ at samp{where comparison is @var{comparepred}} specification only it declares
+a discriminated union type or a foreign type
+(@pxref{Using foreign types from Mercury}) and the
+following conditions are satisfied:
+
+ at itemize @bullet
+ at item
+ at var{comparepred} must be the name of a predicate with signature
+ at example
+:- pred @var{comparepred}(comparison_result::uo, foo(T1, @dots{}, TN)::in,
+ foo(T1, @dots{}, TN)::in) is det.
+ at end example
+
+As with equality predicates, it is legal for the type, mode and
+determinism to be more permissive.
+
+ at item
+The comparison predicate must also be ``pure'' (@pxref{Impurity}).
+
+ at item
+The relation
+ at example
+compare_eq(X, Y) :- @var{comparepred}((=), X, Y).
+ at end example
+must be an equivalence relation; that is, it must be symmetric,
+reflexive, and transitive. The compiler is not required to check this.
+
+ at item
+The relations
+ at example
+compare_leq(X, Y) :- @var{comparepred}(R, X, Y), (R = (=) ; R = (<)).
+compare_geq(X, Y) :- @var{comparepred}(R, X, Y), (R = (=) ; R = (>)).
+ at end example
+must be total order relations: that is they must be antisymmetric,
+reflexive and transitive. The compiler is not required to check this.
@end itemize
@@ -3414,7 +3494,7 @@
is a conceptually non-deterministic operation.
In Mercury this is modelled using committed choice nondeterminism.
-The semantics of a specifying @samp{where equality is @var{equalitypred}}
+The semantics of specifying @samp{where equality is @var{equalitypred}}
on the type declaration for a type @var{T} are as follows:
@itemize @bullet
@@ -3445,14 +3525,8 @@
specified predicate @var{equalitypred}.
@item
- at var{equalitypred} should be an equivalence relation; that is, it must be
-symmetric, reflexive, and transitive. However, the compiler is not required
-to check this at footnote{If @var{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 (@pxref{Semantics}),
-i.e.@: the behaviour of the program is undefined.}.
+Any comparisons of type @var{T} are computed using the specified predicate
+ at var{comparepred}.
@end itemize
@@ -5549,6 +5623,15 @@
type will only be visible in Mercury clauses for predicates or functions with
@samp{pragma foreign_proc} clauses for all of the languages for which there
are @samp{foreign_type} declarations for the type.
+
+As with discriminated union types, programmers can specify the unification
+and comparison predicates to use for values of the type using the following
+syntax (@pxref{User-defined equality and comparison}):
+
+ at example
+:- pragma foreign_type(@var{Lang}, @var{MercuryTypeName}, @var{ForeignTypeDescriptor})
+ where equality is @var{EqualityPred}, comparison is @var{ComparePred}.
+ at end example
You can use Mercury foreign language interfacing declarations
which specify language @var{X} to interface to types that are actually
Index: library/builtin.m
===================================================================
RCS file: /home/mercury1/repository/mercury/library/builtin.m,v
retrieving revision 1.85
diff -u -u -r1.85 builtin.m
--- library/builtin.m 18 Dec 2002 16:06:58 -0000 1.85
+++ library/builtin.m 14 Jan 2003 14:07:18 -0000
@@ -154,7 +154,9 @@
:- func promise_only_solution(pred(T)) = T.
:- mode promise_only_solution(pred(out) is cc_multi) = out is det.
+:- mode promise_only_solution(pred(uo) is cc_multi) = uo is det.
:- mode promise_only_solution(pred(out) is cc_nondet) = out is semidet.
+:- mode promise_only_solution(pred(uo) is cc_nondet) = uo is semidet.
% `promise_only_solution_io' is like `promise_only_solution', but
% for procedures with unique modes (e.g. those that do IO).
@@ -178,6 +180,13 @@
% unify(X, Y) is true iff X = Y.
:- pred unify(T::in, T::in) is semidet.
+ % For use in defining user-defined unification predicates.
+ % The relation defined by a value of type `unify', must be an
+ % equivalence relation; that is, it must be symmetric, reflexive,
+ % and transitive.
+:- type unify(T) == pred(T, T).
+:- inst unify == (pred(in, in) is semidet).
+
:- type comparison_result ---> (=) ; (<) ; (>).
% compare(Res, X, Y) binds Res to =, <, or >
@@ -192,6 +201,25 @@
:- mode compare(uo, ui, in) is det.
:- mode compare(uo, in, ui) is det.
+ % For use in defining user-defined comparison predicates.
+ % For a value `ComparePred' of type `compare', the following
+ % conditions must hold:
+ %
+ % - the relation
+ % compare_eq(X, Y) :- ComparePred((=), X, Y).
+ % must be an equivalence relation; that is, it must be symmetric,
+ % reflexive, and transitive.
+ %
+ % - the relations
+ % 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.
+:- type compare(T) == pred(comparison_result, T, T).
+:- inst compare == (pred(uo, in, in) is det).
+
% ordering(X, Y) = R <=> compare(R, X, Y)
%
:- func ordering(T, T) = comparison_result.
@@ -322,9 +350,19 @@
%-----------------------------------------------------------------------------%
+% XXX The calls to unsafe_promise_unique below work around
+% mode checker limitations.
:- pragma promise_pure(promise_only_solution/1).
-promise_only_solution(CCPred) = OutVal :-
+promise_only_solution(CCPred::(pred(out) is cc_multi)) = (OutVal::out) :-
+ impure OutVal = get_one_solution(CCPred).
+promise_only_solution(CCPred::(pred(uo) is cc_multi)) = (OutVal::uo) :-
+ impure OutVal0 = get_one_solution(CCPred),
+ OutVal = unsafe_promise_unique(OutVal0).
+promise_only_solution(CCPred::(pred(out) is cc_nondet)) = (OutVal::out) :-
impure OutVal = get_one_solution(CCPred).
+promise_only_solution(CCPred::(pred(uo) is cc_nondet)) = (OutVal::uo) :-
+ impure OutVal0 = get_one_solution(CCPred),
+ OutVal = unsafe_promise_unique(OutVal0).
get_one_solution(CCPred) = OutVal :-
impure Pred = cc_cast(CCPred),
--------------------------------------------------------------------------
mercury-reviews mailing list
post: mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------
More information about the reviews
mailing list