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

Volker Wysk <[email protected]> Mon, 21 Nov 2022 20:37:20 +0100
Newsgroups	gmane.comp.lang.mercury.general
Message-ID	<[email protected]>
Am Freitag, dem 18.11.2022 um 22:16 +1100 schrieb Mark Brown:
> On Fri, Nov 18, 2022 at 4:42 AM Volker Wysk <[email protected]> wrote:
> > 
> > Am Mittwoch, dem 16.11.2022 um 14:27 +1100 schrieb Julien Fischer:
> > 
> > > 
> > > > 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".
> > > 
> > > In this case, the explanation is: the compiler has to generate an
> > > out-of-line predicate to implement the unification of P1 and P2. That
> > > generated predicate is declared to be semidet, which is why you are
> > > getting the determinism error. The unification should to be det, since
> > > filling in the holes in P1 with the args from P2 will aways succeed.
> > > The fact that the compiler does not know that is one of the limitations
> > > I was referring to.

Does this out-of-line predicate fail to have the correct determinism
category, because one of the terms to be unificated is partially
instantiated? Or what unifications are affected?

> > 
> > The question is, what does a mere user of the Mercury language need to know
> > in order to understand this, and what does he need to know in order to work
> > around it?
> 
> That is a good question. The knowledge and reasoning I used was
> roughly as follows (this is going to take longer to type than it took
> to actually happen):
> 
> 1. The error message points to a unification in the first argument to
> p, but unifications aren't always explicit. I'll need to think about
> what unifications the compiler sees.
> 
> 2. The strict sequential semantics says, "Function calls, conjunctions
> and disjunctions are all executed in depth-first left-to-right order."
> I know that this determines what the compiler will see before mode
> analysis, namely that the "function call" of -/2 will be before the
> call to p.

So that's the reason why a partially instantiated term is constructed before
the call to p. My intuition was that the output of p would be deconstructed
after the call, since it's an output argument. 

The default semantics is the strict commutative semantics. So you're saying
that the rule "Function calls, conjunctions and disjunctions are all
executed in depth-first left-to-right order." applies here as well.

> 3. I can't see any place where the code could fail, in particular
> because -/2 is the only data constructor of the pair type so it won't
> fail on that account..

Exactly.

> 4. I can, however, see that the unification would construct a
> partially instantiated term. Ugh, it could be a mode analyser
> limitation.
> 
> 5. The mode of p's first argument is out, so this unification is
> probably meant to be a deconstruction that occurs after p returns.
> 
> 6. If I put the unification after the call to p, the mode analyser
> won't need to reorder it to get it to the right place. Maybe that will
> avoid the reordering bug?

So the answer is: The mode analyser has issues with partially instantiated
terms. Such terms will sometimes be implicitly constructed, according to the
strict sequential semantics. Also, unifications can be implicitly
constructed in the process. This may lead to non-obvious error messages.
Making such constructions explicit and moving them around can be the
solution to the observed error. 

> If that hadn't have worked I might have looked at the HLDS dump for
> more clues (or I might have done that in order to explain it to
> someone, as Julien did above).

I've tried that. It's a good way to improve understanding.

> So to answer your question, I think step 2 was probably the obscure
> one (that process is part of what is done in the conversion to
> superhomogeneous form).
> 
> Hope that helps!

Yes, thank you.

Volker

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