[m-rev.] For review: change the way we handle inst any non-locals in negated contexts (again)
Mark Brown
mark at cs.mu.OZ.AU
Fri Dec 16 17:27:35 AEDT 2005
On 16-Dec-2005, Mark Brown <mark at cs.mu.OZ.AU> wrote:
> Thanks for the comments. I think I've addressed all the points that have
> come up so far -- relative diff follows.
Err, that was the full diff. Relative diff follows for real this time.
Cheers,
Mark.
diff -u doc/reference_manual.texi doc/reference_manual.texi
--- doc/reference_manual.texi 15 Dec 2005 05:01:53 -0000
+++ doc/reference_manual.texi 16 Dec 2005 06:16:36 -0000
@@ -486,7 +486,9 @@
promise_exhaustive fy 950
promise_pure fx 950
promise_semipure fx 950
-infer_purity fx 950
+implicitly_pure fx 950
+implicitly_semipure fx 950
+implicitly_impure fx 950
some fxy 950
, xfy 1000
& xfy 1025
@@ -650,11 +652,19 @@
@var{Goal} must be a valid goal.
See @ref{Impurity} for the possible purity annotations and their meanings.
- at item @code{infer_purity @var{Goal}}
-Introduces a scope within which the purity of all goals is inferred
-by the compiler. @var{Goal} must be a valid goal,
-with the exception that all purity annotations (@pxref{Impurity})
-that would otherwise be required on subgoals are optional.
+ at item @code{implicitly_pure @var{PureGoal}}
+ at itemx @code{implicitly_semipure @var{SemipureGoal}}
+ at itemx @code{implicitly_impure @var{ImpureGoal}}
+Introduces a scope within which purity annotations (@pxref{Impurity}) are
+optional, and all purity levels are inferred.
+ at var{PureGoal} must be a valid goal which is inferred pure.
+ at var{SemipureGoal} must be a valid goal which is inferred semipure.
+ at var{ImpureGoal} must be a valid goal which is inferred impure.
+(Note, however, that there is a current limitation that the purity level of
+higher-order predicate calls and function applications cannot be inferred,
+so omitting the annotations on these is likely to lead to a type error.
+There is also a similar limitation whereby argument unifications are not
+handled properly without a purity annotation.)
@item @code{promise_equivalent_solutions @var{Vars} @var{Goal}}
A determinism cast.
@@ -1866,10 +1876,10 @@
@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}.
+If an explicit type qualification 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{Purity and explicit type qualification}.
Type variables in predicate and function declarations
are implicitly universally quantified by default;
@@ -2379,10 +2389,9 @@
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.
+cannot be proven to be safe. Such goals are inferred to be impure.
-Similarly, referential transparency can be violated if a non-local variable
+Similarly, referential transparency may be violated if a non-local variable
with inst @code{any} is used in a lambda expression. Programs are therefore
required to declare such lambda expressions to be @code{impure}.
@@ -8481,7 +8490,7 @@
* Impurity semantics:: What impure code means.
* Impurity Example:: A simple example using impurity.
* Higher-order impurity:: Using impurity with higher-order code.
-* Purity and type qualifiers:: Extra rules for declarations.
+* Purity and explicit type qualification:: Extra rules for declarations.
@end menu
@@ -8492,12 +8501,13 @@
@table @dfn
@item pure
-For pure predicates and functions, there must exist a declarative semantics
-(that is, a set of ground solutions) which, given the bindings of
-arguments when called, fully determines all possible bindings at exit.
-All pure functions must be referentially transparent in the sense that
-any two expressions which are syntactically equal must be semantically
-equal.
+For pure predicates and functions, the set of solutions depends only on
+the initial bindings of the arguments (including the return value in the
+case of functions). That is, there must exist a declarative semantics
+(a set of ground solutions) which, given the bindings of arguments when
+called, fully determines all possible bindings at exit. All pure functions
+must be referentially transparent in the sense that any two function
+applications which are syntactically equal must be semantically equal.
Pure predicates and functions do not interact with the ``real'' world
(i.e., do any input/output) without taking an @code{io.state} (@pxref{Types})
@@ -8561,8 +8571,13 @@
there is no need for a @samp{pure} annotation.
Likewise, since asserting that code is impure imposes no burden of proof
on the programmer, there is no need for a @samp{promise_impure} annotation.
+A ``purity cast'' in the downwards direction can be effected by the
+use of one of the builtin predicates @samp{impure_true}, @samp{impure_false},
+ at samp{semipure_true} or @samp{semipure_false}.
+These are declaratively equivalent to @samp{true} or @samp{false},
+as appropriate, but are defined to be less pure.
-Purity annotations can be used in a number of places:
+Purity annotations can be used in the following places:
@itemize @bullet
@item
In @samp{:- pred} and @samp{:- func} declarations,
@@ -8587,17 +8602,17 @@
Only @code{impure} and @code{semipure} may be used here.
@end itemize
-Purity annotations are compulsory in some, but not all, places.
-The compiler will report an error if any purity annotation
-is not consistent with the inferred purity level,
-or if a purity annotation is not present where one is required.
+Purity annotations are compulsory in some, but not all, places. It is an
+error if any purity annotation is not consistent with the inferred purity
+level, or if a purity annotation is not present where one is required.
The places where a purity annotation is required are as follows:
@itemize @bullet
@item
In @samp{pred} and @samp{func} declarations for which the definition
is inferred to be something other than pure.
@item
-In front of a goal which introduces impurity or semipurity.
+In front of a goal which introduces impurity or semipurity
+(@pxref{Purity inference}).
@item
In the head of a lambda expression for which the body is inferred
to be something other than pure,
@@ -8606,19 +8621,19 @@
@noindent
The only exception to this is that purity annotations are not compulsory
-on goals that are within an @code{infer_purity} scope (@pxref{Goals}).
+on goals that are within an @code{implicitly_pure}, @code{implicitly_semipure},
+or @code{implicitly_impure} 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.)
+(Note, however, that there is a current limitation that the purity level of
+higher-order predicate calls and function applications cannot be inferred,
+so omitting the annotations on these is likely to lead to a type error.
+There is also a similar limitation whereby argument unifications are not
+handled properly without a purity annotation.)
-The requirement that goals which introduce impurity (semipurity)
-be marked with @code{impure} (@code{semipure}) allows someone
+The requirement for goals which introduce impurity (semipurity)
+to 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
@@ -8630,7 +8645,7 @@
@node Purity inference
@section Purity inference
-Purity inference for goals is a fairly straightforward bottom-up analysis.
+Purity inference for goals is a bottom-up process.
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.
@@ -8658,12 +8673,20 @@
@table @asis
@item @code{some @var{Vars} @var{Goal}}
@itemx @code{all @var{Vars} @var{Goal}}
- at itemx @code{infer_purity @var{Goal}}
@itemx @code{promise_equivalent_solutions @var{Vars} @var{Goal}}
@itemx @code{not @var{Goal}}
@itemx @code{\+ @var{Goal}}
The purity level is the same as that of @var{Goal}.
+ at item @code{implicitly_pure @var{Goal}}
+The purity level is @code{pure}.
+
+ at item @code{implicitly_semipure @var{Goal}}
+The purity level is @code{semipure}.
+
+ at item @code{implicitly_impure @var{Goal}}
+The purity level is @code{impure}.
+
@item @code{@var{Purity} @var{Goal}}
If @var{Purity} is @code{promise_pure} (@code{promise_semipure}) then
the purity level is @code{pure} (@code{semipure}).
@@ -8766,25 +8789,30 @@
between ordinary Mercury code and imperative code written with Mercury
syntax. How this distinction is drawn is explained above; the
purpose of this section is to explain the semantics of programs with
-impure predicates.
+impure code.
-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,
+For the purposes of this section, ``impure goals'' refers to goals that
+have an explicit @code{impure} annotation or goals that introduce impurity.
+The latter may not have an explicit annotation if they are within a
+scope which makes these optional, but the semantics is not affected by that.
+Similarly, ``semipure goals'' refers to goals that have an explicit
+ at code{semipure} annotation or goals that introduce impurity.
+
+A @emph{declarative} semantics of impure Mercury code would be useless,
+because the declarative semantics cannot capture the intent of
+the programmer. Impure goals 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.
+it is the @emph{operational} semantics of impure goals that Mercury
+must specify, and Mercury implementations must respect.
-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;
-not even ``minimal'' reordering as implied by the modes is permitted.
-If any such reordering is needed, this is a mode error.
-However, goals with a @code{semipure} annotation and goals with no annotation
-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 goal which is annotated @code{impure}.
+The operational semantics of a Mercury predicate that contains impure
+goals is a modified form of the @emph{strict sequential} semantics
+(@pxref{Semantics}). Impure goals will not be reordered relative to any
+other goals; not even ``minimal'' reordering as implied by the modes is
+permitted. It is a mode error if any such reordering is required.
+All other goals (including 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
@@ -8792,18 +8820,16 @@
Impure disjuncts cannot be pruned away even if the disjunction has
already succeeded and there are no output variables.
-Goals which are annotated @code{semipure} can be given a ``contextual''
-declarative semantics. They cannot have any side-effects,
-so it is expected that, given the context in which they are called
-(relative to any @code{impure} annotations in the program),
-their declarative semantics fully captures the intent of the
-programmer. Thus a semipure goal has a perfectly consistent declarative
-semantics, until a goal with an @code{impure} annotation is reached.
-After that, it has another (possibly different) declarative semantics,
-until the next goal with @code{impure} annotation is executed, and so on.
-Mercury compilers must respect this contextual nature of the semantics of
-semipure goals; within a single context, a compiler may treat a semipure
-goal as if it were pure.
+Semipure goals can be given a ``contextual'' declarative semantics.
+They cannot have any side-effects, so it is expected that, given the
+context in which they are called (relative to any impure goals),
+their declarative semantics fully captures the intent of the programmer.
+Thus a semipure goal has a perfectly consistent declarative semantics,
+until an impure goal is reached. After that, it has another (possibly
+different) declarative semantics, until the next impure goal is reached,
+and so on. Mercury compilers must respect this contextual nature of the
+semantics of semipure goals; within a single context, a compiler may treat
+a semipure goal as if it were pure.
@node Impurity Example
@section An example using impurity
@@ -8939,11 +8965,11 @@
impure Ys = map(ImpureFunc, Ys).
@end example
- at node Purity and type qualifiers
- at section Purity and type qualifiers
+ at node Purity and explicit type qualification
+ at section Purity and explicit type qualification
-Predicate and function declarations that make use of @code{`with_type`}
-can contain purity annotations in more than one location.
+Predicate and function declarations that make use of explicit type
+qualification may 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,
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------
More information about the reviews
mailing list