Mercury Bugs - mercury
View Issue Details
IDProjectCategoryView StatusDate SubmittedLast Update
0000015mercuryBugpublic2007-10-05 13:252009-12-11 06:46
Reporterpjrm 
Assigned Tojuliensf 
PrioritynormalSeveritymajorReproducibilityalways
StatusresolvedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version 
Summary0000015: wrong variable scoping in `if ( some[X] p(X) ) then q(X) ...'
Description:- module ifsome.
:- interface.
:- import_module io.
:- pred main(io::di, io::uo) is det.
:- implementation.
:- import_module string.
main(!IO):-
        X = "outer",
        ( if ( some[X] X = "inner" ) then
                io.write_string(X, !IO),
                io.nl(!IO)
         else
                true
        ).

This prints "inner", but one would expect it to print "outer" (both from one's expectations from standard predicate logic notation and from the point of view of the Mercury reference manual: "some Vars Goal ... The variables in Vars are local to the goal Goal", and the definition of if-then-else says nothing to contradict that: its statement about the declarative semantics of if-then-else is false for this example, or at least (if we want an example that still compiles after the transformation) for similar examples not involving I/O in the then/else goals).

Fixing this bug is made harder by the fact that an example program in mercury_faq.texi depends on this behaviour (at least in absence of parens around the `some' goal): search for `if some'.

In the example I've given, the severity of the bug is reduced by the fact that we get an `unused variable' warning (or a `shadowed variable' warning if we add another use of X). However, it is possible to construct examples that don't produce warnings by not having X outside of the if-then-else but where the behaviour differs according to whether X is bound or free on entry to the `then' goal (e.g. if the if-then-else is in semidet context and the `then' goal is `generate(X), test(X)'; and a similar generate(X),test(X) construct in the condition to avoid appears-only-once warning/objection). (I can send a 40-line example if that's useful, it's just not as succinct as the above.)

This bug doesn't arise all that often, but is nevertheless a "psychologically" important bug, in that it results in a program that gives a wrong result rather than abort; it attacks Mercury's claim to logical consistency and ease of reasoning about program behaviour.

pjrm.
Additional InformationI haven't checked a current ROTD.
TagsNo tags attached.
Relationships
Attached Files

Notes
(0000219)
pjrm   
2009-11-28 02:23   
Can someone please at least comment on what they think is the best course of action, e.g. whether to introduce an `ifsome' keyword, whether to change the behaviour of `if (some[VARS] GOAL(VARS))' to match the documentation [and, more importantly, to match what I believe to be programmer/logician expectations], whether to change the documentation to match the current behaviour, etc.?

FWIW, I think the right things would be:

First of all, change mercury_faq.texi (near the end of the Programming node) so as not to use this construct, e.g. simply comment out the `if some' version of the example and its following `The explicit existential quantifier...' comment, leaving the implicit-quantifier version (and add a link to this bug report). This takes about one minute; please, if you have commit rights then do it now.

As to the appropriate behaviour of `if some[VARS]' or `if (some[VARS]...)':
The contradictions in the documentation on this point is evidence of contradictory expectations. I believe most people would expect the parenthesized version to have VARS local to the parenthesized expression. For `if some', I could accept either behaviour, so long as the documentation is changed to explicitly describe the behaviour for this case that evidently has contradictory expectations.

The question of whether to introduce an `ifsome' keyword depends in part on how `if some' and `if (some...)' are resolved. If both are changed to match the language reference manual documentation, or if both are made to produce a warning, then there's a strong case for adding an ifsome keyword. Otherwise, the decision is harder, and I suspect that different people will answer differently according to how they see Mercury being used; FWIW, I currently lean towards still introducing one.
(0000224)
wangp   
2009-12-02 20:57   
I agree that `if (some ...) then' is misleading, but the scoping behaviour is useful to keep. I think the best course of action is to make the compiler distinguish between `if (some ...)' and `if some ...', in line with our intuition.

The problem does not warrant a new keyword. I don't think I've ever seen it in practice -- the quantifier is optional, so the shorter and clearer code would leave it out.
(0000225)
pbone   
2009-12-02 21:08   
isn't this a Prolog compatibility feature?

I believe the work around is:

(
   some [X] cond(X),
   true
->
   then
;
   else
).

This makes the condition a conjunction rather than an existentially quantified goal. I seem to recall having this conversation with Julian.
(0000226)
wangp   
2009-12-02 22:36   
Here is one relevant thread:
http://thread.gmane.org/gmane.comp.lang.mercury.devel/1151
(0000228)
juliensf   
2009-12-04 00:30   
The current behaviour is intended (although not documented properly), i.e.
if the top-level goal of the condition of an if-then-else is an existential quantification
then the quantified variables are quantified over both the condition and the then branch.
The rationale for this behaviour is that there is no other way to write an existential quantification
over both the condition and then branch in Mercury otherwise.

Note that the proposed "if some [Vars]" or "( some [Vars if ...") syntax does not extend
to the ( c-> t ; e) syntax. In any case, I think that introducing new syntax to deal with what
is a very rare usage is not worth it.

IMO, the appropriate resolution to this is just to document that conditions whose top-level
goal is an existential quantification are scoped over both the condition and then then branch.
(Indeed, I have a diff somewhere that changes the reference manual to say precisely this.)
(0000229)
juliensf   
2009-12-04 00:35   
(Last edited: 2009-12-04 02:33)
Hi Paul,

The difference between:

( some [X] C, true -> T ; G)

and

( some [X] C -> T ; G)

is that the in the latter X is quantified over C and T because the top-level goal of the condition
is an existential quantification; in the former case the top-level goal is a conjunction, so here
X is only quantified over C.
(0000230)
pbone   
2009-12-04 09:26   
Julien:

This has jogged my memory, I remember discussing this with you now. The thing that I forgot was that in the latter example that the existential quantification covered T, I knew it did something unexpected but couldn't remember what.

Cheers.
(0000233)
juliensf   
2009-12-11 06:45   
I have committed a change to the reference manual that documents the behaviour
of i.t.e conditions that are explicit existential quantifiers.
(See r1.436 of doc/reference_manual.texi.)

The confusing example in the FAQ has been deleted.

Any further discussion about alternative syntax for existentially quantifying over
the condition and then branch can take place on mercury-developers. (IMO, adding
such syntax is not worth it however.)

Issue History
Date ModifiedUsernameFieldChange
2007-10-05 13:25pjrmNew Issue
2007-10-12 17:44anonymousNote Added: 0000013
2007-10-12 18:39anonymousNote Deleted: 0000013
2007-10-13 18:09anonymousNote Added: 0000019
2007-10-13 18:50anonymousNote Deleted: 0000019
2007-10-13 22:52anonymousNote Added: 0000021
2007-10-13 22:52anonymousNote Added: 0000022
2007-10-14 03:12anonymousNote Added: 0000023
2007-10-14 06:56anonymousNote Added: 0000024
2007-10-14 10:26anonymousNote Deleted: 0000021
2007-10-14 10:27anonymousNote Deleted: 0000024
2007-10-14 10:27anonymousNote Deleted: 0000022
2007-10-14 10:28anonymousNote Deleted: 0000023
2007-10-14 10:35anonymousNote Added: 0000025
2007-10-14 10:50anonymousNote Deleted: 0000025
2009-11-28 02:23pjrmNote Added: 0000219
2009-12-02 20:57wangpNote Added: 0000224
2009-12-02 21:08pboneNote Added: 0000225
2009-12-02 22:36wangpNote Added: 0000226
2009-12-04 00:30juliensfNote Added: 0000228
2009-12-04 00:35juliensfNote Added: 0000229
2009-12-04 02:33juliensfNote Edited: 0000229
2009-12-04 09:26pboneNote Added: 0000230
2009-12-11 06:45juliensfNote Added: 0000233
2009-12-11 06:45juliensfStatusnew => resolved
2009-12-11 06:45juliensfResolutionopen => fixed
2009-12-11 06:45juliensfAssigned To => juliensf