[mercury-users] Re: unsorted_solutions/2

Peter Schachte pets at students.cs.mu.oz.au
Mon Oct 27 16:20:01 AEDT 1997


On Sun, 26 Oct 1997, Fergus Henderson wrote:

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

It might be the best that can be done without modifying the
language/compiler, but I wouldn't say it was fine.  This information really
should be declarative information about a predicate, not extra packaging
around a call.  Ie, it belongs in the mode declaration, or perhaps a pragma.
Something like this would be pleasant:

	:- pred max(int,int,int).
	:- mode max(in,in,out) is promised det.

	max(X, Y, X) :- X >= Y.
	max(X, Y, Y) :- X =< Y.

After determinism checking max/3, if the inferred mode is multi (or det),
then the promise of det would be accepted, otherwise it's an error. 
Similarly for nondet->semidet.

And yes, I know you can kind of fake this with two predicates:  the real
one which is multi, and the public one which calls it wrapped with
promise_one_solution.  But this is pretty ugly, and not very declarative,
and probably a significant efficiency penalty for simple predicates like
this one.

I suspect, however, that this wouldn't satisfy Bart either (not to put words
into Bart's fingers...).

How about a predicate first_of/2 which deterministically returns the first
of a number of (potential) solutions: 

	:- pred first_of(list(pred(T)), T).
	:- mode first_of(list_skel_in(pred(out) is semidet), out) is semidet.

	:- pragma inline(first_of/2).

	first_of([Goal|Goals], Result) :-
		(   Goal(Result1) ->
			Result = Result1
		;   first_of(Goals, Result)
		).

Granted, the syntax is abysmal, but the idea is basically to commit to the
first of a number of goals to succeed.  By putting the alternatives in a
specific order, the problem of nondeterminism is avoided.

The only trouble with this is that the current Mercury mode/determininsm
checking algorithm is pretty fussy about uses of this predicate.  You can
coax it to work, but forget about using type/mode/determinism inference.


-Peter Schachte			| Some lies are so well disguised to resemble
pets at cs.mu.OZ.AU		| truth, that we should be poor judges of the
http://www.cs.mu.oz.au/~pets/	| truth not to believe them. -- Anonymous 
PGP key available on request	| 




More information about the users mailing list