[m-rev.] For review: change the way we handle inst any non-locals in negated contexts (again)

[Julien Fischer]

On Thu, 15 Dec 2005, Mark Brown wrote:

> The reference manual is meant to be self-explanatory so I will omit
> any preliminary remarks at this stage, except to note that one section
> (marked with an XXX) is not complete, and that some of the cross-referencing
> is not ideal and will be improved later.
>
> Enjoy!
>

...

> @@ -1876,6 +1865,12 @@
>  :- pred f(int, T, U) = U.
>  @end example
>
> +Predicate and function declarations may also include a purity annotation.
> +If @code{`with_type`} is used then the actual purity is determined by the
> +annotation on the declaration, however this annotation must be consistent
> +with that of the given higher-order type.
> + at xref{Impurity}.
> +

Could we avoid referring to `with_type` since `:` is also acceptable?
How about:

	If an explicit type qualification is used then the ...


> +Negation is implemented using ``negation-as-failure'', which is unsound
> +if non-local variables can become bound inside a negation.
> +It is not generally possible to determine whether a non-local variable
> +with inst @code{any} will become bound at a point where it is used,
> +which means that a negation containing such a variable,
> +or an if-then-else whose condition contains such a variable,
> +cannot be proven to be safe.
> +Such goals are therefore inferred to be impure.
> +

Delete therefore.

> +Similarly, referential transparency can be violated if a non-local variable

s/may/can/

> +with inst @code{any} is used in a lambda expression.  Programs are therefore
> +required to declare such lambda expressions to be @code{impure}.
> +
> + at xref{Impurity}.
>

...

>  @menu
>  * Purity levels::       	Choosing the right level of purity.
> -* Purity ordering::     	How purity levels are ordered
> +* Purity annotations::		Marking the purity level of code.
> +* Purity inference::		How the purity of code is determined.
>  * Impurity semantics::  	What impure code means.
> -* Declaring impurity::  	Declaring predicates impure.
> -* Impure goals::        	Marking a goal as impure.
> -* Promising purity::    	Promising that a predicate is pure.
>  * Impurity Example::    	A simple example using impurity.
>  * Higher-order impurity::    	Using impurity with higher-order code.
> +* Purity and type qualifiers::	Extra rules for declarations.

A minor point, I suggest you call that last section:

	Purity and explicit type qualification

since that fits in better with the exiting type qualification section.

...

> -A @emph{declarative} semantics of impure Mercury code would be largely
> -useless, because the declarative semantics cannot capture the intent of
> -the programmer.  Impure predicates are executed for their side-effects,
> -which by definition are not part of their declarative semantics.  Thus
> -it is the @emph{operational} semantics of impure predicates that Mercury
> -must specify, and Mercury compilers must respect.
> +Purity annotations can be used in a number of places:

I suggest:

	Purity annotate can be used in the following places:

It seems a bit vague otherwise.

> + at itemize @bullet
> + at item
> +In @samp{:- pred} and @samp{:- func} declarations,
> +immediately after the @samp{:-}.
> + at item
> +Immediately preceding a goal.
> + at item
> +In the head of a lambda expression,
> +immediately preceding the @samp{pred} or @samp{func}.
> + at item
> +In the attributes of a @code{foreign_proc} declaration
> +(@pxref{Foreign code attributes}).
> +Only @code{promise_pure} and @code{promise_semipure} may be used here.
> + at item
> +Immediately preceding a method in a typeclass declaration.
> +Only @code{impure} and @code{semipure} may be used here.
> +An instance of the type class must provide method implementations that are
> +at least as pure as the method declaration.
> + at item
> +In a higher-order type expression,
> +immediately preceding the @samp{pred} or @samp{func}.
> +Only @code{impure} and @code{semipure} may be used here.
> + at end itemize
>
> -The operational semantics of a Mercury predicate which invokes
> - at emph{impure} code is a modified form of the @emph{strict sequential}
> -semantics (@pxref{Semantics}).  @emph{Impure} goals may not be reordered
> -relative to any other goals; not even ``minimal'' reordering as implied
> -by the modes is permitted.  If any such reordering is needed, this is a
> -mode error.  However, @emph{pure} and @emph{semipure} goals may be
> -reordered as the compiler desires (within the bounds of the semantics
> -the user has specified for the program) as long as they are not moved
> -across an impure goal.  Execution of impure goals is strict: they must
> -be executed if they are reached, even if it can be determined that the
> -computation cannot lead to successful termination.
> +Purity annotations are compulsory in some, but not all, places.
> +The compiler will report an error if any purity annotation

I suggest:

	It is an error if any purity annotation is not
	consistent ...

> +The only exception to this is that purity annotations are not compulsory
> +on goals that are within an @code{infer_purity} scope (@pxref{Goals}).
> +Inside such a scope, unannotated goals which introduce impurity (semipurity)
> +are treated as if they had an @code{impure} (@code{semipure}) annotation,
> +and all other goals are left unchanged.
> +(Note, however, that there is a current limitation that the purity level
> +of higher-order calls cannot be inferred,
> +so omitting the annotation from a higher-order call is likely to lead
> +to a type error.
> +XXX there may also be a similar limitation whereby argument unifications
> +are not handled properly without an explicit annotation.)
> +
> +The requirement that goals which introduce impurity (semipurity)

I suggest:

	The requirement for goals that introduce impurity (semipurity)
	to be marked with ...

> +be marked with @code{impure} (@code{semipure}) allows someone
> +reading the code to tell which goals are not pure and why,
> +making code which relies on side effects somewhat less mysterious.
> +Furthermore, it means that if a call is @emph{not} preceded by
> + at code{impure} or @code{semipure}, then the reader can rely on the call
> +having a proper declarative semantics, without hidden side-effects,
> +can rely on negations being implemented soundly,
> +and can rely on expressions being referentially transparent.
> +


> + at node Purity inference
> + at section Purity inference
> +
> +Purity inference for goals is a fairly straightforward bottom-up analysis.
> +Some goals, listed below, introduce impurity, and this impurity propagates
> +upwards until a ``promise'' removes it, or until it is encapsulated in a
> +lambda expression.
>

Whether purity inference for goals is fairly straightforward or not really
isn't a matter the reference manual needs to mention.  All this section
really needs to convey is that impurity propgates upwards until it is
dealt with.

...

> +A @emph{declarative} semantics of impure Mercury code would be largely
> +useless, because the declarative semantics cannot capture the intent of

Is there any point in quantifying the degree of uselessness?

> +the programmer.  Impure predicates are executed for their side-effects,
> +which by definition are not part of their declarative semantics.  Thus
> +it is the @emph{operational} semantics of impure predicates that Mercury
> +must specify, and Mercury compilers must respect.
>

Elsewhere in the reference manual we use the terminology "Mercury
implementations" rather than "Mercury compilers".


> -The programmer may promise that a predicate or function is pure or semipure
> -using the @code{promise_pure} and @code{promise_semipure} pragmas:
> +The operational semantics of a Mercury predicate which contains
> + at emph{impure} goals is a modified form of the @emph{strict sequential}
> +semantics (@pxref{Semantics}).  Goals which have an @code{impure} annotation
> +may not be reordered relative to any other goals;

s/cannot/may not/

> +not even ``minimal'' reordering as implied by the modes is permitted.
> +If any such reordering is needed, this is a mode error.

then it is a mode error

...

> + at node Purity and type qualifiers
> + at section Purity and type qualifiers
> +
> +Predicate and function declarations that make use of @code{`with_type`}
> +can contain purity annotations in more than one location.
> +These must be consistent, but they need not match exactly.
> +The rules for which combinations are legal,
> +and determining the purity level that results,
> +are as follows:
> +

See my comments about type qualification above.

Cheers,
Julien.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------