logic - mercury 中的 ADT 特性

我想知道为什么 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 :
它甚至可以决定检测:

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

最佳答案

我对带有条件的确定性的 Mercury 规则(如下)的阅读是，为了将其视为确定性的，您应该将 -> 替换为 ,
来自 Mercury 引用手册:

关于logic - mercury 中的 ADT 特性，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/3359972/

MERCury

logic - mercury 中的 ADT 特性