[m-users.] Is this a compiler bug?

[Mark Brown]

On Wed, Nov 16, 2022 at 6:07 AM Volker Wysk <post at volker-wysk.de> wrote:
>
> Hi there.
>
> Am Dienstag, dem 15.11.2022 um 16:05 +1100 schrieb Julien Fischer:
> > On Sat, 12 Nov 2022, Volker Wysk wrote:
> >
> > > The following program fails to compile:
> > >
> > > :- module pairbug.
> > > :- interface.
> > > :- import_module io.
> > >
> > > :- pred main(io::di, io::uo) is det.
> > >
> > > :- implementation.
> > > :- import_module pair, string.
> > >
> > > :- pred p(pair(string, string)::out, io::di, io::uo) is det.
> > > p("foo" - "bar", !IO).
> > >
> > > main(!IO) :-
> > >    p(A - B, !IO).    % <- line 19
> > >
> > >
> > > The message is:
> > >
> > > pairbug.m:006: In `main'(di, uo):
> > > pairbug.m:006:   error: determinism declaration not satisfied.
> > > pairbug.m:006:   Declared `det', inferred `semidet'.
> > > pairbug.m:006:   The reason for the difference is the following.
> > > pairbug.m:019:   In argument 1 of call to predicate `pairbug.p'/3:
> > > pairbug.m:019:   unification with `V_9' can fail.
> > >
> > >
> > > But the following works:
> > >
> > > main(!IO) :-
> > >    p(P, !IO),
> > >    P = A - B.
> > >
> > >
> > > This must either be something stupid or a compiler bug...
> >
> > It is a consequence of the following:
> >
> > - how the clauses are translated into superhomogenous form;
> > - the fact that A and B are unused;
> > - the fact that the current Mercury implementation does not support
> >    partial instantiation properly.
> >
> > (Superhomogenous form is the form by which clauses are represented
> > inside the compiler.)
> >
> > Here's what the compiler sees for the first version immediately
> > before mode analysis:
> >
> >     main(STATE_VARIABLE_IO_0, STATE_VARIABLE_IO) :-
> >        V_8 = A - B,
> >        p(V_9, STATE_VARIABLE_IO_0, STATE_VARIABLE_IO),
> >        V_8 = V_9.
> >
> > (The variables prefixed with 'V_' or 'STATE_VARIABLE_' are introduced
> > by the compiler.)
> >
> > Here's what the compiler sees for the second version immediately
> > before mode analysis:
> >
> >     main(STATE_VARIABLE_IO_0, STATE_VARIABLE_IO) :-
> >         p(P, STATE_VARIABLE_IO_0, STATE_VARIABLE_IO),
> >         P = A - B.
> >
> > The first version constructs a partially-instantiated term, e.g.
> > pair(<<free>>, <<free>>), puts the output of p/3 into V_9 and then
> > attempts to unify them (which I suspect is where it falls over).
> > Is that what you were intending?
>
> Yes, it is. And you're right about the point where it falls over. See below.
>
> > You might ask: why doesn't mode analysis reorder the first version to
> > be like the second. The answer is: it doesn't have any reason to do
> > such reordering.
> >
> > One of the other pieces of compiler you get from that program is:
> >
> >     pairbug.m:014: In clause for predicate `main'/2:
> >     pairbug.m:014:   warning: variables `A, B' occur only once in this scope.
> >
> > If I have a version of the program, that uses A or B, e.g.
> >
> >      main(!IO) :-
> >        p(A - B, !IO),
> >        io.print(A, !IO).
> >
> > then mode analysis will reorder things appropriately.
>
> You talk about "reordering" of the clauses, which make up the two
> superhomogenous forms. The second form, you say, could or could not be a
> reordered version of the first. But the two superhomogenous forms can't be
> reordered versions of each other, because the first one consists of three
> clauses, whereas the second one consists of two clauses. I don't fully get
> what you're saying.

Mode analysis can also introduce unifications like the V_8 = V_9 above.

>
> I'm wondering if there's some documentation about superhomogenous forms and
> mode analysis. The word "superhomogenous" doesn't occur in the language
> reference manual. But "mode analysis" is mentioned a couple of times. I'm
> going to study it.
>
>
> The following version of main fails to compile (like expected) with
> "Unification of `P1' and `P2' can fail". (Here we have the point of
> failure). Even though that isn't the case:
>
> main(!IO) :-
>     P1 = A - B,
>     p(P2, !IO),
>     P1 = P2.
>
> I suppose this due to what you described as "the fact that the current
> Mercury implementation does not support partial instantiation properly".
>
> If I remember correctly, this has already been addressed at some point in
> this mailing list. And that the full support of partial instantiation had
> been implemented, but then was dropped again, because it made the compiler
> too slow.
>
> I find the state of affairs a bit disappointing. The programmer shouldn't
> have to cope with superhomogenous forms and mode analysis.

Strong modes and determinism have both advantages and disadvantages:
Mercury takes the view that the former greatly outweigh the latter.
One of the consequences of this is that not all program
transformations that are logically correct are mode/determinism
correct, so programmers will necessarily have to "cope" with it to
some extent. But you're right that the compiler could do more in cases
like this one.

> Maybe the proper
> support of partial instantiation can be implemented after all, with the
> computers becoming more powerful all the time...?

A rule of thumb that I find helps deal with this is, "If your code is
easier for a programmer to analyse, then it is easier for the compiler
to analyse." So I think the first thing I would have done in this
situation would be to just try putting the unification with A - B
after the call, since it's an output of the call, and see if the
compiler gets it.

Given that the workaround for this problem usually makes your code
easier to read, I don't consider it a priority to attempt to improve
the compiler in this regard. I do agree that we could document the
rules better, however, e.g., by characterizing exactly which modes a
unification can have.

Mark


>
>
> Cheers,
> Volker
> _______________________________________________
> users mailing list
> users at lists.mercurylang.org
> https://lists.mercurylang.org/listinfo/users