3

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.
ony
  • 12,457
  • 1
  • 33
  • 41

3 Answers3

2

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.

RD1
  • 3,305
  • 19
  • 28
  • In this case `ResStream` may unify with `io.ok(Stream)`, but also may unify with `io.error(Err)`. That's depends on result of opening file. There is two branches for that. To get exclusive "or" I use "if-the-else" construction and as according to your citation it should suit. But Mercury can't infer that `not(ResStream = ok(_)) => ResStream = error(_)`. – ony Jul 29 '10 at 17:56
  • 1
    In your case, the else branch is `ResStream = io.error(Err), ResFreqs = io.error(Err)` which will fail if ResStream is io.ok(X). The rule I quoted doesn't say anything about adding the negation of the condition. I agree that logically it could be added, but the reference manual indicates that it isn't. In contrast, disjunctions are treated specially if they have the form of a "switch" - which seems to allow conjunction in the disjuncts but not conditionals. I guess the reasoning is that in the common case the patterns don't intersect, and in that case "," and "->" do the same thing. – RD1 Jul 29 '10 at 18:16
  • Patterns can intersect and Mercury finds those intersections with infering determinism "multi". See additional example. If you will decide det. only by head than `read_freqs` (in update) will be marked as multi. – ony Jul 30 '10 at 04:41
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.

Paul Bone
  • 802
  • 4
  • 9
  • At this moment, for me it's easier to understand through `(X = yes, true; not(X = yes), X = no)` (that's what I expect from `(X = yes -> true; X = no)`) will be infered to nondet because of `not/1`. – ony Feb 07 '11 at 07:16
  • That's true until the condition becomes more complicated. If either there are more symbols than yes or no, or there is more than one unification in the condition. – Paul Bone Feb 09 '11 at 08:46
1

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?

ony
  • 12,457
  • 1
  • 33
  • 41
  • 1
    My first answer to "why?" is because that's what the Mercury reference manual says should happen. But, I guess you mean "why is Mercury designed that way?". My guess is that switches need to be treated in a special way, and the designers didn't want to make them any more complicated than necessary, and avoiding negative information really simplifies things. Plus, my impression is that Mercury generally encourages switches in preference to conditionals. Indeed there's a switch --inform-ite-instead-of-switch to enable reporting of conditionals that should be replaced by switches. – RD1 Jul 30 '10 at 06:49
  • Thanks, that's useful option "--inform-ite-instead-of-switch". – ony Jul 30 '10 at 08:30