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

[Mark Brown]

On 15-Dec-2005, Ian MacLarty <maclarty at cs.mu.OZ.AU> wrote:
> On Thu, Dec 15, 2005 at 04:06:54PM +1100, Mark Brown wrote:
> 
> > + at item @code{infer_purity @var{Goal}}
> > +Introduces a scope within which the purity of all goals is inferred
> > +by the compiler.  
> 
> I don't like this sentence.  It seems to suggest that the compiler
> doesn't infer the purity of goals not in an infer_purity scope (which it
> must in order to prove the code is pure).

Okay.  Actually, I'll go through the whole change and make sure this
implicit purity thing is dealt with consistently, since I don't think the
semantics chapter deals with it very well as it stands.

Incidentally, should that scope perhaps be named "implicit_purity" instead?
I was undecided which one was better when I originally wrote it, but given
the objection above I think "infer_purity" is probably the poorer choice.
It just seemed to be more consistent with "--infer-types" and
"--infer-modes".

Another alternative is a set of scopes which allow implicit purity, but which
also assert what the purity of the scope actually is.  That is, these scopes
would be "pure_implicit", "semipure_implicit" and "impure_implicit", and
they would be similar to the "promise_*_implicit" scopes that have been
removed, except that they wouldn't be making any promises.  Come to think of
it, I like these scopes better, but I'd be happier if I could think of
better names for them.

> 
> >  @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.
> > +
> 
> Can you leave the sentence "For pure procedures, the set of solutions
> depends only on the values of the input arguments." in?  In my (humble)
> opinion it's easier to understand than what you've replaced it with.

I removed it because I found it objectionable on a couple of grounds:

	- It isn't really procedures that are pure, it is predicates and
	  functions that are.  All of the procedures (i.e., modes) of a
	  predicate or function must agree on the declarative semantics
	  for it to be pure, but that first sentence doesn't impose this
	  requirement.

	- When you have partially instantiated data (e.g., solver variables),
	  it doesn't make much sense to talk about input and output arguments.
	  They tend to be all inputs, and they don't really have a value as
	  such -- they have a domain (i.e., set of values) at entry and a
	  possibly smaller domain at exit.

How does the following sound:

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

I'd like to say just that pure predicates and functions must _have_ a
declarative semantics, but that's too much like a circular definition: if
readers know what a declarative semantics is then they probably don't need
to be told what "pure" means.

Keep it coming!

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