[m-users.] comprehension question

[Zoltan Somogyi]

On Fri, 25 Oct 2019 14:49:27 +0200, Volker Wysk <post at volker-wysk.de> wrote:
> Does that mean that
> 
>   ( if p
>     then q
>     else r )
> 
> is operationally equivalent to
> 
>   ( p,
>     q
>   ; not(p), 
>     r
>   )
> 
> ?

No. Those two pieces of code are equivalent semantically,
but not operationally.

> I don't understand the soundness part.

There are many possible definitions of soundness,
one for every theoretical property that an implementation
may or may not implement correctly, i.e. soundly.
In this case, the relevant one is mode correctness.

If the condition of an if-then-else binds a variable that occurs
only in the condition and the then-part of that if-then-else,
then all those occurrences see that binding, and everything is fine.

If the condition of an if-then-else binds a variable that occurs
not just in the condition and the then-part of that if-then-else,
but elsewhere as well, either in the else-part or in code outside
the if-then-else itself, then there are problems. Any occurrences
in the else-part cannot see the binding (since execution reaches
them only if the binding has been backtracked over), while any
occurrences after the if-then-else may or may not see the binding,
depending on whether the condition succeeded or not. Unlike Prolog,
Mercury does not allow code in which the question of whether
a variable is bound at a given program point has different answers
depending on how execution reached that program point.

In the case of your code, the else part does not contain an occurrence
of Num, the nonlocal variable bound by the condition in the out,in mode,
but the rest of the predicate does: specifically, the clause head.
In your case, execution cannot reach the point where it returns Num
to its caller if the condition fails, but the mode checker does not know that.
Requiring to know that would complicate the language significantly
for no good reason.

> How should the predicate to be
> done?

The idiomatic Mercury for this problem would use two separate predicates,
like this:

:- module errno.
:- interface.

:- type errno
    --->    e2BIG
    ;       eACCES
    ;       eAGAIN.

:- pred errno_int(errno, int).
:- mode errno_int(in, out) is det.
:- mode errno_int(out, in) is semidet.

:- pred int_to_errno(int::in, errno::out) is det.

:- implementation.
:- import_module require.

errno_int(Errno, Int) :-
    ( Errno = e2BIG, Int = 0
    ; Errno = eACCES, Int = 1
    ; Errno = eAGAIN, Int = 2
    ).

int_to_errno(N, Errno) :-
    ( if errno_int(ErrnoPrime, N) then
        Errno = ErrnoPrime
    else
        unexpected($pred, "N is not a valid errno")
    ).

You *could* possibly implement your original interface for error1
using mode-specific clauses and a promise-equivalent-clauses pragma,
but that would not be a good idea.

Zoltan.