Question

I wander why Mercury (10.04) can t infer determinism of next snippet:

:- pred load_freqs(int::in, io.res(list(float))::out, io::di, io::uo) is det.
load_freqs(CPU, ResFreqs, !IO):-
    open_input(cpu_fn(CPU, "available_frequencies"), ResStream, !IO),
    (ResStream = io.ok(Stream) ->
        ResFreqs = io.ok([])
    ;ResStream = io.error(Err),
        ResFreqs = io.error(Err)
    ).

It complains:

cpugear.m:075: In `load_freqs (in, out, di, uo):
cpugear.m:075:   error: determinism declaration not satisfied.
cpugear.m:075:   Declared `det , inferred `semidet .
cpugear.m:080:   Unification of `ResStream  and `io.error(Err)  can fail.
cpugear.m:076: In clause for predicate `cpugear.load_freqs /4:
cpugear.m:076:   warning: variable `CPU  occurs only once in this scope.
cpugear.m:078: In clause for predicate `cpugear.load_freqs /4:
cpugear.m:078:   warning: variable `Stream  occurs only once in this scope.

But io.res have only io.ok/1 and io.error/1.
And next snippet of code compiles well:

:- pred read_freqs(io.res(io.input_stream)::in, io.res(list(float))::out, io::di, io::uo) is det.
read_freqs(io.ok(Stream), io.ok([]), IO, IO).
read_freqs(io.error(Err), io.error(Err), IO, IO).

Update #1: It can decide det even for:

:- pred read_freqs(bool::in, io.res(io.input_stream)::in, io.res(list(float))::out, io::di, io::uo) is det.
read_freqs(no, ResStream, io.ok([]), IO, IO):- ResStream = io.ok(_).
read_freqs(F, io.ok(_), io.ok([]), IO, IO):- F = yes.
read_freqs(yes, io.error(Err), io.error(Err), IO, IO).
read_freqs(F, ResStream, io.error(Err), IO, IO):- ResStream = io.error(Err), F = no.

Answer 1

My reading of the Mercury rules for determinism with conditionals (below) is that for this to be considered deterministic, you should replace the -> with a ,

From the Mercury reference manual:

If the condition of an if-then-else cannot fail, the if-then-else is equivalent to the conjunction of the condition and the “then” part, and its determinism is computed accordingly. Otherwise, an if-then-else can fail if either the “then” part or the “else” part can fail.

Answer 2

As for Why . lets look at the original code with the if-then-else:

(ResStream = io.ok(Stream) ->
    ResFreqs = io.ok([])
;ResStream = io.error(Err),
    ResFreqs = io.error(Err)
).

If the condition fails, then the first conjunct in the else case is a semidet test. The compiler doesn t know that it must succeed (which can be inferred by the knowledge that this condition failed). In other words, the compiler is not smart enough.

That said, it s vary rare to find this problem, because usually the condition is more complicated and won t allow for this inference to be made, so it s not important that the compiler is not smart enough to determine the correct determinism here.

It is recommended to program using switches whenever possible (such as this example), it prevents the current problem and helps ensure that you ve covered all the possible cases of ResStream. For example, if in the future io.error was re factored and could be io.error_file_not_found or io.error_disk_full etc the compiler would direct the programmer to fix their switch as it would now be incomplete.

Answer 3

Ok, it can infer det for:

:- pred load_freqs(int::in, io.res(list(float))::out, io::di, io::uo) is det.
load_freqs(CPU, ResFreqs, !IO):-
    open_input(cpu_fn(0, "available_frequencies"), ResStream, !IO),
    (ResStream = io.ok(Stream),
        ResFreqs = io.ok([])
    ;ResStream = io.error(Err),
        ResFreqs = io.error(Err)
    ).

But why "if-then-else" construction introduces semidet?

友情链接