Note that “perfect” determinism inference is an undecidable problem, because it requires solving the halting problem. (For instance, in the following example
:- pred p(T, T). :- mode p(in, out) is det. p(A, B) :- ( something_complicated(A, B) ; B = A ).
‘p/2’ can have more than one solution
only if ‘something_complicated’ can succeed.)
Sometimes, the rules specified by the Mercury language
for determinism inference will infer a determinism
that is not as precise as you would like.
However, it is generally easy to overcome such problems.
The way to do this is to replace the compiler's static checking
with some manual run-time checking.
For example, if you know that a particular goal should never fail,
but the compiler infers that goal to be
you can check at runtime that the goal does succeed,
and if it fails, call the library predicate ‘error/1’.
:- pred q(T, T). :- mode q(in, out) is det. q(A, B) :- ( goal_that_should_never_fail(A, B0) -> B = B0 ; error("goal_that_should_never_fail failed!") ).
error/1 has determinism
which means the compiler knows that it will never succeed or fail,
so the inferred determinism for the body of
(Checking assumptions like this is good coding style anyway.
The small amount of up-front work that Mercury requires
is paid back in reduced debugging time.)
Mercury's mode analysis knows that
computations with determinism erroneous can never succeed,
which is why it does not require the “else” part to generate
a value for ‘B’.
The introduction of the new variable ‘B0’ is necessary
because the condition of an if-then-else is a negated context,
and can export the values it generates
only to the “then” part of the if-then-else,
not directly to the surrounding computation.
(If the surrounding computations had direct access
to values generated in conditions,
they might access them even if the condition failed.)