[m-rev.] For review: make impure goals with inst any vars in negated contexts

[Fergus Henderson]

On 28-Oct-2005, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> +++ NEWS	28 Oct 2005 03:33:07 -0000
> @@ -5,6 +5,8 @@
>  ==========
>  
>  Changes to the Mercury language:
> +* Goals in negated contexts using inst any non-local variables or lambda
> +  expressions containing inst any non-locals must now be marked as impure.
>  * The Mercury typeclass system now supports functional dependencies.
>  * We now have support for optional module initialisation and finalisation.
>  * We now have support for impure module-local mutable variables.

I don't think that should be the first thing in the list.
I'd put it towards the end of that list.  The list doesn't need
to be strictly in order of importance but in general it's probably
better if additions of new features (e.g. functional dependencies)
get listed before changes that restrict the use of the language
or that remove old features.

Also, you mentioned this change in the "HIGHLIGHTS" section but not in the
"DETAILED LISTING".  The "DETAILED LISTING" section should give a brief
rationale for the change.

Also the description is probably a bit tricky for non-experts to understand.
s/any/"any"/ would help a little, but perhaps a more drastic rewording
would be better?

In the HIGHLIGHTS section summary, you don't need to mention lambda
expressions.  A lambda expression _is_ a negated context
according to the definition of "negated context" in the language
reference manual.  It may be worth reminding users of this
in the DETAILED LISTING part.

So I suggest the following:

HIGHLIGHTS
...
* To ensure soundness, goals in negated contexts using non-local variables
  with dynamic modes (inst "any") must now be marked as impure.

DETAILED SUMMARY
...
* To ensure soundness, goals in negated contexts using non-local variables
  with dynamic modes (inst "any") must now be marked as impure.

  If a goal uses a variable with a dynamic mode (inst "any"),
  and that goal occurs inside a negated context (such as the
  condition of an if-then-else, or a lambda expression),
  and the variable also occurs outside of that negated context,
  then the compiler will infer that goal to be impure,
  and so such goals must normally be marked as "impure".

  This change was required because Mercury implements negation using
  the standard negation-as-failure approach, which is not sound if the
  negated goal binds any non-local variables.

  As usual, the programmer can use "promise_pure" if they are
  sure that the goal is in fact pure, e.g. because they know that
  the goal inside the negation will not instantiate the variable.

-- 
Fergus Henderson                    |  "I have always known that the pursuit
                                    |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------