unsorted_solutions/2

[Fergus Henderson]

Don Smith wrote:
> (I don't want to burden the mailing list.  But you can forward it there
> is you wish.)

I'm currently working on a paper which explains this issue in more detail,
but the documentation on committed choice nondeterminism in the existing
Mercury implementation doesn't explain the rationale, and Mercury's
approach is a bit different to Prolog's approach in this respect,
so I think this is definitely worth explaining to the mailing list.

(I'd best not explain _too_ well, though, lest any future referees for
the paper read this email and then decide that the paper's results
are "obvious" ;-)

> My 700 line application needs to collect an unsorted list of solutions
> at some point (because calling solutions/2 causes it to completely sort
> the list, which is terribly expensive and unnecessary in my case).  But
> when I use unsorted_solutions/2, I get determinism checking errors.
> 
> The documentation on unsorted_solutions/2 says
> 
>      % unsorted_solutions/2 returns [the solutions] as an unsorted list with
>      % possible duplicates; since there are an infinite number of such lists,
>      % this must be called from a context in which only a single solution
>      % is required.
> 
>      :- pred unsorted_solutions(pred(T), list(T)).
>      :- mode unsorted_solutions(pred(out) is multi, out) is cc_multi.
>      :- mode unsorted_solutions(pred(out) is nondet, out) is cc_multi.
> 
> When (naughty) I modified the std_util.int file and changed the modes
> to "det", my application compiled (and seems to run) fine.
>
> I don't understand the rationale for making unsorted_solutions/2
> cc_multi, rather than det.  In fact, it returns only a single list,
> right?  If the programmer doesn't care about the order (any order is
> OK), then why make life difficult for him?  Seems perverse to me.
> After all, at the top level, main/2 returns an arbitrary solution.
> People curse programming languages that tie their hands too much.
>
> Similarly, I'm all in favor of a one_solution/2 predicate which returns
> an (arbitrary) solution to its first argument in the second, in any
> context.
> 
> Seem to me that somebody has an overly narrow notion of what is
> declarative.   But, heck, I'm open to being convinced otherwise.
> 
>    Don (dsmith at cirl.uoregon.edu, dsmith at cs.waikato.ac.nz)

Well, the aim is not to make life difficult for the programmer ;-)
However, we do want the programmer to document the distinction
between procedures which have only one solution, and procedures
which have multiple solutions but for which the programmer doesn't
care which he gets.  So we're not tying the programmer's hands,
we're just imposing some minimum documentation requirements.

The reason for imposing this documentation requirement is so that
the compiler can ensure that procedures whose semantics only makes
sense if called from a place where you don't care which answer
you get are not called from places where you _do_ care which answer
is returned.

The correct solution to this problem is to push the `cc_multi' modes
up the call-graph, rather than pushing `det' down.  In other words,
you should declare the procedure which calls unsorted_solutions/2
as cc_nondet or cc_multi too, and perhaps its caller, and its caller's
caller, and so on up to main if necessary.  Keep declaring things
as cc_multi until you get to a goal which really has only one
solution.  If the goal has no output variables, the compiler will
realize that it can have at most one solution, but for other cases
you may need to use `promise_one_solution' (explained below).

> After all, at the top level, main/2 returns an arbitrary solution.

No, if main/2 is declared `det' rather than `cc_multi', then that
is not the case.  If main/2 is declared `det', then there is only
one solution, and so main/2 returns THE solution, not an abitrary
solution.  Only if main/2 is declared `cc_multi' will it return
an arbitrary solution.

The distinction is important, because we want the implementation to
have the freedom to reorder clauses or to compute solutions in a different
order than ordering found by the usual Prolog left-to-right depth-first
search.  

Giving implementations this freedom means that the behaviour unspecified,
which does have drawbacks, as well as gains.  For example, it can make
testing more difficult.  So it is important to explicitly label the
parts of the program which may have unspecified behaviour.  If the
behaviour at the top level will be unspecified, then the programmer
ought to explicitly say so.

> Similarly, I'm all in favor of a one_solution/2 predicate which returns
> an (arbitrary) solution to its first argument in the second, in any
> context.

Something like this _is_ needed, for cases where all the answers
are guaranteed to be the same.  An example of this is if say you
are trying to find the maximum solution to a goal, by first
finding all solutions using unsorted_solutions/2, and then taking
the maximum of the list.

But this is only safe if there really is only one solution to the
predicate, logically speaking.  (And only needed in cases where the
compiler can't figure that out for itself.)  If there are multiple
(unequal) solutions, then your one_solution/2 predicate would be
incomplete and in the presence of negation it would be unsound. 
In such cases, you should declare the procedure cc_multi (or
cc_nondet) and move the call to one_solution/2 into the caller.

Since it is only safe in limited circumstances, its use must constitute
a promise to the compiler.  I originally named the procedure
`promise_unique', rather than `one_solution', but this issue has
nothing to do with unique modes, so `promise_one_solution' is probably
a better name.  Also I made it a function, rather than a predicate.
I've appended an implementation of it below.

[`promise_one_solution' or something similar will probably go in the
standard library eventually.  The main reason that it is not there yet
is that in fact it would be preferable to have a more general version.
The generalization (called say `promise_independent') would take two
goals; it would be equivalent to conjunction, except that it would also
promise that the set of answers to the second goal was independent of
the choice of answers for the first.  Unfortunately there are some
technical difficulties in implementing a sufficiently generic version
of `promise_independent'...]

%-----------------------------------------------------------------------------%
:- module unsafe.
	% This module contains predicates/functions that are potentially
	% unsafe if used improperly; there is no compile-time or even
	% run-time checking for these predicates/functions.
	% Beware that misuse of this module may lead to unsound results.
	% If you lie to the compiler, the compiler will get its revenge!

%-----------------------------------------------------------------------------%
:- interface.

	% A call to `promise_one_solution(Pred)' constitutes a promise
	% on the part of the caller that `Pred' has at most one
	% solution, i.e. that
	%	not some [X1, X2] (Pred(X1), Pred(X2), X1 \= X2).
	%
	% `promise_one_solution(Pred)' presumes that this assumption is
	% satisfied, and returns the X for which Pred(X) is true
	% (by assumption, there can be only one such X).
	%
:- func promise_one_solution(pred(T)) = T.
:- mode promise_one_solution(pred(out) is cc_multi) = out is det.
:- mode promise_one_solution(pred(out) is cc_nondet) = out is semidet.

%-----------------------------------------------------------------------------%
:- implementation.

promise_one_solution(Pred) = OutVal :-
	call(cc_cast(Pred), OutVal).

:- func cc_cast(pred(T)) = pred(T).
:- mode cc_cast(pred(out) is cc_nondet) = out(pred(out) is semidet) is det.
:- mode cc_cast(pred(out) is cc_multi) = out(pred(out) is det) is det.

:- pragma c_code(cc_cast(X::(pred(out) is cc_multi)) =
			(Y::out(pred(out) is det)),
		will_not_call_mercury,
		"Y = X;").
:- pragma c_code(cc_cast(X::(pred(out) is cc_nondet)) =
			(Y::out(pred(out) is semidet)),
		will_not_call_mercury,
		"Y = X;").

%-----------------------------------------------------------------------------%

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