logic - mercury 的 ADT 属性

Question

我想知道为什么 Mercury (10.04) 无法推断下一个片段的确定性:

:- 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)
    ).

它提示:

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).

更新 #1:它甚至可以决定 det:

:- 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

我对带条件的确定性规则的 Mercury 规则(如下)的解读是，要将其视为确定性的，您应该将 -> 替换为 ,

来自 Mercury 引用手册:

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.