propriétés ADT dans Mercury

Question

Je vagabonder pourquoi Mercury (10,04) ne peut pas déduire le déterminisme du prochain extrait:

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

Il se plaint:

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.

Mais io.res ont seulement io.ok/1 et io.error/1.
Et suivant bout de code compile bien:

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

Mise à jour # 1: Il peut décider det même:

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

Ma lecture des règles de mercure pour le déterminisme avec conditionals (ci-dessous) est que pour cela être considéré comme déterministe, vous devez remplacer le -> par un ,

du Mercury re manuel Conférence:

Si l'état d'un if-then-else ne peut pas échouer, l'if-then-else est équivalente à la conjonction de la condition et la partie « then », et son déterminisme est calculé en conséquence. Sinon, un if-then-else peut échouer si la partie "then" ou la partie "else" peut échouer.

Answer 2

Ok, il peut déduire det pour:

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

Mais pourquoi la construction "if-then-else" introduit semidet?

Answer 3

Comme pour 'Pourquoi'. permet de regarder le code original avec if-then-else:

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

Si la condition échoue, la première dans le cas en conjonction avec d'autres est un test semidet. Le compilateur ne sait pas qu'il doit réussir (ce qui peut être inféré par la connaissance que cette condition a échoué). En d'autres termes, le compilateur n'est pas assez intelligent. Cela dit, il est rare de trouver ce problème, car la condition est généralement plus compliquée et ne permet pas cette inférence, il n'est donc pas important que le compilateur ne soit pas assez intelligent pour déterminer le déterminisme correct. ici.

Il est recommandé de programmer à l'aide de commutateurs autant que possible (comme dans cet exemple), cela évite le problème actuel et aide à s'assurer que vous avez couvert tous les cas possibles de ResStream. Par exemple, si dans le futur io.error était factorisé et pourrait être io.error_file_not_found ou io.error_disk_full etc, le compilateur ordonnerait au programmeur de réparer son switch car il serait maintenant incomplet.