[mercury-users] Getting 'any' insts to ground

[Lee Naish]

In message <199711101256.XAA15090 at mundook.cs.mu.OZ.AU>Fergus wrote:
>	:- pred is_ground(var(T), maybe(T)).
>	:- mode is_ground(in(any), out) is cc_multi.
>
>Operationally, is_ground(Var, Result) returns Result = no
>if Var is non-ground, and Result = yes(Value) if Var is ground;

If this is guartanteed to be the case then isn't it possible to use
something like promise_one_solution to write a correct non-logical 
version which is det/semidet?  Of course you have to tell a little
white lie: is_ground has one solution.

I think its important that at least the documentation and predicate
naming makes it reasonably obvious that this kind of thing is BAD.
I suspect many novice Mercury programmers would not realise that calling
is_ground inside promise_one_solution is telling a lie - they would
think that its a legitimate way of getting the mode checker to stop
producing those stupid error messages.

There is a fine line between logical and nonlogical code/languages once
you introduce pruning.  In Goedel its possible to implement a version of
is_var which works *if* you have a fixed clause selection rule.  Since
Goedel doesn't guarantee this, you can argue that its theoretically
impossible write a correct version of is_var (of course in practice you
can write one which works, since the only existing Goedel implementation
does used a fixed selection rule).

In Mercury there are options to fix the selection rule, which makes
things more dangerous, but the mode system forces us to use cc_ modes
and keeps things logical.  The logic is lost when the promise in
promise_one_solution is broken.  I think it fine to have predicates such
as promise_one_solution (though this name is poor -  six possible
interpretations are "there is at least/exactly/at most one solution according
to the declarative/procedural semantics"), but it is desirable to have
debugging support for the cases where promises are broken (since this is
one source of bugs).

Ideally there should be some debugging/paranoid version/mode for such
predicates which allows promises to be checked.  For example,
promise_one_solution called with a nondet procedure could find all
solutions and check there is the right number.  The "right" thing to do
for promise_one_solution calling a cc_nondet procedure would be to have
a nondet version of the procedure and call that instead, as above.  This
might be a bit tricky to arrange - we would need non-cc versions of
each cc procedure in general.  However, I think its important that there
are ways of automatically checking that no promise is broken, for a
particular input to the program.

	lee