| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0000015 | mercury | Bug | public | 2007-10-05 13:25 | 2009-12-11 06:46 | ||||
| Reporter | pjrm | ||||||||
| Assigned To | juliensf | ||||||||
| Priority | normal | Severity | major | Reproducibility | always | ||||
| Status | resolved | Resolution | fixed | ||||||
| Product Version | |||||||||
| Target Version | Fixed in Version | ||||||||
| Summary | 0000015: 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 Information | I haven't checked a current ROTD. | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
pjrm (reporter) 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. |
|
wangp (developer) 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. |
|
pbone (administrator) 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. |
|
wangp (developer) 2009-12-02 22:36 |
Here is one relevant thread: http://thread.gmane.org/gmane.comp.lang.mercury.devel/1151 |
|
juliensf (administrator) 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.) |
|
juliensf (administrator) 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. |
|
pbone (administrator) 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. |
|
juliensf (administrator) 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.) |
| Notes |
| Issue History |
|||
| Date Modified | Username | Field | Change |
|---|---|---|---|
| 2007-10-05 13:25 | pjrm | New Issue | |
| 2007-10-12 17:44 | anonymous | Note Added: 0000013 | |
| 2007-10-12 18:39 | anonymous | Note Deleted: 0000013 | |
| 2007-10-13 18:09 | anonymous | Note Added: 0000019 | |
| 2007-10-13 18:50 | anonymous | Note Deleted: 0000019 | |
| 2007-10-13 22:52 | anonymous | Note Added: 0000021 | |
| 2007-10-13 22:52 | anonymous | Note Added: 0000022 | |
| 2007-10-14 03:12 | anonymous | Note Added: 0000023 | |
| 2007-10-14 06:56 | anonymous | Note Added: 0000024 | |
| 2007-10-14 10:26 | anonymous | Note Deleted: 0000021 | |
| 2007-10-14 10:27 | anonymous | Note Deleted: 0000024 | |
| 2007-10-14 10:27 | anonymous | Note Deleted: 0000022 | |
| 2007-10-14 10:28 | anonymous | Note Deleted: 0000023 | |
| 2007-10-14 10:35 | anonymous | Note Added: 0000025 | |
| 2007-10-14 10:50 | anonymous | Note Deleted: 0000025 | |
| 2009-11-28 02:23 | pjrm | Note Added: 0000219 | |
| 2009-12-02 20:57 | wangp | Note Added: 0000224 | |
| 2009-12-02 21:08 | pbone | Note Added: 0000225 | |
| 2009-12-02 22:36 | wangp | Note Added: 0000226 | |
| 2009-12-04 00:30 | juliensf | Note Added: 0000228 | |
| 2009-12-04 00:35 | juliensf | Note Added: 0000229 | |
| 2009-12-04 02:33 | juliensf | Note Edited: 0000229 | |
| 2009-12-04 09:26 | pbone | Note Added: 0000230 | |
| 2009-12-11 06:45 | juliensf | Note Added: 0000233 | |
| 2009-12-11 06:45 | juliensf | Status | new => resolved |
| 2009-12-11 06:45 | juliensf | Resolution | open => fixed |
| 2009-12-11 06:45 | juliensf | Assigned To | => juliensf |
| Issue History |