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

[Mark Brown]

On 15-Dec-2005, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> Mark Brown, Thursday, 15 December 2005:
> > @@ -2910,18 +2912,16 @@
> >  
> >  Because of this possibility, predicates or functions which are defined
> >  using different code for different modes are by default assumed to be
> > -impure; the programmer must either (1) carefully ensure that the
> > -logical meaning of the clauses is the same for all modes,
> > -in which case a @samp{pragma promise_pure} declaration can be used
> > -or (2) declare the predicate or function as impure.
> > +impure; the programmer must therefore place a purity annotation on the
> > +declaration.
> >  @xref{Impurity}.
> >  
> >  In the example with @samp{append} above, the two ways of implementing
> > -append do have the same declarative semantics, so we can safely use
> > -the first approach:
> > +append do have the same declarative semantics, so we can safely promise
> > +it to be pure:
> >  
> >  @example
> > -	:- pragma promise_pure(append/3).
> > +	:- promise_pure pred append(list(T), list(T), list(T)).
> >  @end example
> 
> Just as a matter of style, it would be bad to have `promise_pure' on 
> an exported predicate; in that case I'd use the pragma instead.

That's a good point, and one I didn't consider.  The intent was actually to
abolish that pragma entirely -- it never seemed right to me that the promise
was made via a pragma, even though such pragmas are currently considered
a standard part of the language (see the start of chapter 16).  The rules
I've set out imply that this append definition will be inferred impure, and
therefore that an annotation on the declaration would be necessary -- either
impure, promise_pure or promise_semipure.

However, the principle that implementation details shouldn't have to be
exposed in the interface is a good one, so perhaps we should keep the
pragmas after all, or find some other way to make the promise in the
implementation.  Anyone got any suggestions?

> 
> >  In the example with @samp{var/1} above, the two clauses have different
> > @@ -8480,14 +8492,21 @@
> >  
> >  @table @dfn
> >  @item pure
> > -For pure procedures, the set of solutions depends only on the
> > -values of the input arguments.
> > -They do not interact with the ``real'' world (i.e., do any
> > -input/output) without taking an io.state (@pxref{Types}) as input and
> > -returning one as output, and do not change the value of any data
> > -structure that will not be undone on backtracking (unless the data
> > -structure would be unreachable on backtracking).  Note that equality
> > -axioms are important when considering the value of data structures.
> > +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.
> 
> What about user defined equality?

Not sure what you mean.  Do you mean that I should change "determines" to
"determines (modulo the equality theory)"?  Or is there something I'm
missing?

> 
> > +There are four purity annotations that can be used to assert purity
> > +levels in code.
> > +The first two of these, @samp{impure} and @samp{semipure},
> > +are used to declare that a predicate, function or goal has a certain purity.
> > +These two annotations are checked by the compiler
> > +according to the rules in @ref{Purity inference},
> > +and it is an error if they do not match the purity level it infers.
> > +The remaining two, @samp{promise_pure} and @samp{promise_semipure},
> > +are used to assert that a predicate, function or goal is known to have
> > +a certain purity even though it can't be inferred.
> > +The compiler does not insist that these annotations match the inferred purity;
> > +it instead checks that the promised purity exceeds the inferred purity ---
> > +these annotations indicate points in the program where the programmer
> > +assumes responsibility for the safety of the code.
> > +(As with all such promises, you should use these with the utmost caution:
> > +if you lie to the compiler it will have its revenge!)
> > +
> > +Note that since Mercury code is pure by default,
> > +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.
> 
> I think you should mention impure_true here (which should be a builtin,
> and we should make semidet_true and semidet_false builtins, too).

I'd be happy with that.  And don't forget semipure_true!  There are other
determinism-casting builtins we may also want for completeness.

> 
> > +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.
> > +The places where a purity annotation is required are as follows:
> > + at itemize @bullet
> > + at item
> > +In @samp{pred} and @samp{func} declarations for which the definition
> > +is inferred to be something other than pure.
> > + at item
> > +In front of a goal which introduces impurity or semipurity.
> 
> Do you mean "atomic goal" here?

No, since negations and if-then-elses can also introduce impurity.
The definitive list of goals that "introduce impurity" is in the following
section, so this is one of the cases where the cross-references can be
improved.

> 
> > +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.)
> 
> Yes, I was bitten by this one today.

I know, and I happened to be writing that paragraph when it occurred.  :-)

Cheers,
Mark.

--------------------------------------------------------------------------
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
--------------------------------------------------------------------------