6.3 Replacing compile-time checking with run-time checking

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/2’ 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 semidet, 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!")
    ).

The predicate error/1 has determinism erroneous, which means the compiler knows that it will never succeed or fail, so the inferred determinism for the body of q/2 is det. (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.)