[m-users.] comprehension question

[Mark Brown]

Hi Volker,

On Fri, Oct 25, 2019 at 6:21 PM Volker Wysk <post at volker-wysk.de> wrote:
>
> Hi!
>
> I have a question. I don't understand, why this doesn't work. This is
> the backwards direction of error() from the posix library:
>
> :- pred error1(int, posix.error).
> :- mode error1(out, in) is det.
> %:- mode error1(in, out) is det.
>
> error1(Num, Res) :-   ((  Num = 0,    Err = e2BIG
>     ;   Num = 1,    Err = eACCES
>     ;   Num = 2,    Err = eAGAIN
>     ;   Num = 3,    Err = eBADF
> (...)
>     ;   Num = 39,   Err = eSPIPE
>     ;   Num = 40,   Err = eSRCH
>     ;   Num = 41,   Err = eTIMEDOUT
>     ;   Num = 42,   Err = eXDEV
>     ) ->
>         Res = Err
>     ;
>         Res = unknown(Num, "unknown errno")
>     ).
>
> I get this message from the compiler:
>
> strerror.m:072: In clause for `error1(out, in)':
> strerror.m:072:   scope error: attempt to bind a non-local variable
> inside the
> strerror.m:072:   condition of an if-then-else.
> strerror.m:072:   Variable `Num' has instantiatedness `free',
> strerror.m:072:   expected instantiatedness was `unique(0)'.
> strerror.m:072:   The condition of an if-then-else is only allowed to
> bind
> strerror.m:072:   variables which are local to the condition or which
> occur
> strerror.m:072:   only in the condition and the `then' part.
>
>
> Shouldn't this work in both directions? I think it's logical...?

The relation is injective but not bijective, so it would not actually
be logical to declare the reverse mode det.

It would be logical to declare the reverse mode semidet, in the sense
that it would be consistent with the declarative semantics, but that
doesn't mean it should work operationally. Mercury uses
negation-as-failure to implement if-then-elses and this is unsound if
you bind variables in the way the error message describes; that's why
it is disallowed.

Mark