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

Volker Wysk <[email protected]> Thu, 17 Nov 2022 14:53:40 +0100
Newsgroups	gmane.comp.lang.mercury.general
Message-ID	<[email protected]>
Am Mittwoch, dem 16.11.2022 um 12:46 +1100 schrieb Mark Brown:
> On Wed, Nov 16, 2022 at 6:07 AM Volker Wysk <[email protected]> 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.

So do I, with my limited level of understanding.

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

A better word would be "to concern oneself with". (Sorry, English isn't my
native language.)

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

Actually, I have. But I couldn't understand why it didn't work the way it
did it first. So now, I'm trying to come to an understanding of what's going
on.

But I don't think the code is easier to comprehend when you put the
unification after the call. 

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

But you get an unintelligible error message, the way it is now. When you
know what's wrong, you can make a workaround. But in my case, I didn't
understand what's going on.

> I do agree that we could document the
> rules better, however, e.g., by characterizing exactly which modes a
> unification can have.

Yes, this sounds like what I'm after.


Best regards,
Volker

_______________________________________________
users mailing list
[email protected]
https://lists.mercurylang.org/listinfo/users
signature.asc (application/pgp-signature, 833 B)