[mercury-users] Understanding why a predicate using try/2 is multi (instead of cc_multi)

[Ian MacLarty]

Hi Andrew,

On Wed, Oct 19, 2011 at 5:35 PM, Andrew Ross
<andrew at bubblehelicopter.com> wrote:
> Hi all, I'm hoping someone here and can help me understand why my mmc infers
> that my predicate is multi instead of cc_multi. I've tried compiling with
> --debug-det but the only extra output I got was comments of the form:
>
>  Inferred new detism det for predicate`test_do_overflow_safe.run_test'/3 mode 0
>  Inference pass complete
>  Inferred old detism det for predicate`test_do_overflow_safe.run_test'/3 mode 0
>  Inference pass complete
>  Inferred new detism det for predicate`test_do_overflow_safe.main'/2 mode 0
>
> I'm writing unit tests and want to catch exceptions so I can run multiple
> (related) tests sequentially within a single executable. Test case predicates
> are passed to a wrapper predicate that is responsible for calling them and
> catching exceptions.
>
> Here is a dummy test function and an implementation of run_test that silently
> swallows the exception:
>
> :- pred main(io::di, io::uo) is det.
>
> main(!IO) :-
>    Test1 = ((pred(N::out) is det) :- N = 0),
>    run_test(Test1, !IO).
>
> :- pred run_test(pred(T), io, io) is det.
> :- mode run_test(in(pred(out) is det), di, uo).
>
> run_test(TestPred, !IO) :-
>    try(TestPred, _Result).
>
> This compiles and runs correctly. By adding a trace goal to Test1 you can see
> that it is being executed.
>
> As soon as I try to do something with the result of try/2 (such as printing it
> with io.write), mmc infers that run_test is multi:
>
>  In `main'(di, uo):
>   error: determinism declaration not satisfied.
>   Declared `det', inferred `multi'.
>   call to `test_do_overflow_safe.run_test'(di(/*
>   unique */(pred((free >> ground)) is det)), di,
>   uo) can succeed more than once.
>  In clause for `main(di, uo)':
>   mode error: argument 2 did not get sufficiently
>   instantiated.
>   Final instantiatedness of `STATE_VARIABLE_IO'
>   was `mostly_unique',
>   expected final instantiatedness was `unique'.
>  In `run_test'(di(/* unique */(pred((free >>
>   ground)) is det)), di, uo):
>   error: invalid determinism for a predicate with
>   I/O state arguments.
>   Valid determinisms are det, cc_multi and
>   erroneous.
>  Inferred :- pred run_test((pred T), io.state,
>   io.state).
>  Inferred :- mode run_test(di(/* unique
>   */(pred((free >> ground)) is det)), di, uo) is
>   multi.
>  Error: call to predicate `exception.try'/2 with
>   determinism `cc_multi' occurs in a context which
>   requires all solutions.
>
> Wrapping try/2 in promise_equivalent_solutions allows the compilation to
> succeed, but I'm wary of using that without fully understanding why run_test is
> being treated as multi.
>
> I read the thread at
> http://www.mercury.csse.unimelb.edu.au/mailing-lists/mercury-users/mercury-users.201005/0011.html
> but that deals with why you need to explicitly convert cc_multi to det with
> promise_equivalent_solutions, where as I would be happy for cc_multi to bubble
> up to main.

In your example above, you've declared main as det.  You can declare
it as cc_multi if you want to avoid the promise_equivalent_solutions
in run_test.

The reason try is cc_multi is because it could return either a result
or an exception, but (declaratively) you don't know which.  If you
ignore try's result, then the result of run_test is unaffected by what
value try returns, so it's inferred to be det.  However if you do
something with try's result that affects the output of run_test (for
example using to modify the io state by passing it to io.write), then
run_test's output depends on try's output and so it too must be
cc_multi.

I'm not sure exactly why the system infers run_test to be multi
instead of cc_multi if you omit the mode declarations.  I'd guess it's
probably just a weakness in the mode inference.  Usually you're better
off adding explicit mode and type declarations to all your predicates.

Ian.

--------------------------------------------------------------------------
mercury-users mailing list
Post messages to:       mercury-users at csse.unimelb.edu.au
Administrative Queries: owner-mercury-users at csse.unimelb.edu.au
Subscriptions:          mercury-users-request at csse.unimelb.edu.au
--------------------------------------------------------------------------