[mercury-users] Re: unsorted_solutions/2

[Fergus Henderson]

Bart Demoen, you wrote:
> 
> Fergus quotes from what Don wrote to him:
> 
> > 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.
> 
> I agree wholeheartedly with Don - maybe for different reasons, but
> that's ok. For me a one_solution/2 predicate will help me in
> convincing the Mercury compiler that some goal is det, but more
> importantly, it will let me reuse code more easely.
> 
> Both can be achieved in other ways, but these ways are awkward
> compared to using a one_solution/2 predicate ! I think.

If the problem you are trying to solve is that you have a goal
which is logically `det', but which the Mercury compiler is not
able to infer is `det', then using promise_one_solution/2 is a fine
solution.

But if the goal is not logically `det', then using a one_solution/2
predicate is not a good idea.  If you do, your program is inconsistent,
and hence according to the Mercury language reference manual the behaviour
is undefined.  It may work fine with the current Mercury implementation,
but there is no guarantee that it will work with future implementations.

That's the status quo, anyway.  I hope you agree that given this status
quo, misusing a one_solution predicate is not a good idea.  Maybe
you find declaring things as `cc_multi' instead of `det' to be awkward
(I haven't found this to be a problem, myself), but surely you agree
that it would be far more awkward if your program simply stopped working
or gave bogus results with a future implementation of Mercury.

Maybe you are advocating some change to the status quo which would mean
that the behaviour was not undefined in such cases.  But if so, I'm not
sure exactly what change you are advocating, so if that is the case,
it would help if you could elaborate the details of your proposed
change.  (Possible changes in this direction would include making
the behaviour defined even for inconsistent programs, or dropping
some or all of the "mode-determinism assertion" axioms, but each of
these have significant drawbacks, IMHO.)

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