[m-dev.] for review: impure functions

[Fergus Henderson]

On 12-Apr-2000, Tyson Dowd <trd at cs.mu.OZ.AU> wrote:
> On 06-Apr-2000, Fergus Henderson <fjh at cs.mu.OZ.AU> wrote:
> > On 04-Apr-2000, Tyson Dowd <trd at cs.mu.OZ.AU> wrote:
> > > Impure functions can be declared just like impure preds.
> > > However, they can only be called in an explicit unification preceeded
> > > by a purity level:
> > > 
> > > 	impure X = some_impure_func(Y, Z)
> > 
> > It would be much nicer if that syntax could be
> > 
> > 	X = impure some_impure_func(Y, Z)
> 
> I like the idea that only goals can be impure, and impurity
> declarations come before the goal.  (of course, not *all* sorts of
> goals can be impure).
> 
> That way there is only one thing to look for and one place to look
> for it.  It jumps out at you because it's always on the left-hand-side
> of the goal.
> 
> With any other feature I would agree that your placement of the
> annotation is a nicer place.  But this one has some other goals
> that conflict with the "correct" placement.

Yes, it's a delicate trade-off.  There are advantages both ways.

> > > @@ -5372,13 +5379,15 @@
> > >  input/output) without taking an io__state (@pxref{Types}) as input and
> > >  returning one as output, and do not make any changes to any data
> > >  structure that will not be undone on backtracking (unless the data
> > > -structure would be unreachable on backtracking).  The behaviour of other
> > > -predicates is never affected by the invocation of pure predicates, nor
> > > -is the behaviour of pure predicates ever affected by the invocation of
> > > -other predicates.
> > > +structure would be unreachable on backtracking).  The behaviour of pure
> > > +predicates is never affected by the invocation of pure predicates.
> > > +It is possible for the invocation of pure predicate to affect the
> > > +behaviour of non-pure predicates and vice versa.
> > 
> > That change misses the point.  The sentence "The behaviour of pure predicates
> > is never affected by the invocation of pure predicates" is not correct.
> > For pure procedures with determinism `cc_nondet' or `cc_multi',
> > the invocation of other pure predicates can affect which solution
> > you get. 
> 
> Hmmm...
> 
> I view the committed choice determinisms as a statement about the
> semantics of the order of results.
> 
> In the strict sequential semantics the statement "The behaviour of pure
> predicates is never affected by the invocation of pure predicates"
> should be true (without qualification).
>
> In other semantics, it is permissible for the results of these
> operations to be non-deterministic.  The fact that operationally
> some pure predicates might affect the operation of cc_* predicates is
> irrelevant -- declaratively these predicates are non-deterministic,
> anything at all can affect them.  So the declarative "behaviour" of pure
> predicates is unaffected by the invocation of pure predicates.
> 
> (this makes me think that perhaps benchmarking requires an I/O state
> after all, since in strict sequential semantics an I/O state is the only
> way you can account for different timing results brought about by the
> external environment).
> 
> Am I completely off target here?  Are we really disputing the word
> "behaviour"?  (I'd prefer to use something else).

Yes, mainly I am disputing the use of the word "behaviour".
In my terminology, the term "declarative behaviour" is meaningless;
you have "declarative semantics", which is a set of statements in
predicate calculus, "operational semantics", which is a set of possible 
behaviours, and "behaviour", which is how the program actually
behaves at runtime.

But you have raised some very good questions here, and answering
your questions takes us into some very murky waters ;-)
I'll move that discussion to a new thread.

> > > +++ impure_func_t2.err_exp	Sun Mar 26 17:53:07 2000
> > > @@ -0,0 +1,4 @@
> > > +impure_func_t2.m:016: In call to impure function `impure_func_t2:get_counter/0':
> > > +impure_func_t2.m:016:   error: call must be in an explicit unification
> > > +impure_func_t2.m:016:   which is preceded by `impure' indicator.
> > 
> > It might be nicer if the error message specified which of these
> > two conditions was not satisfied.
> 
> The impure indicator is *always* the problem.
> 
> It is possible that in addition to having an impure indicator, the impure
> call occurs somewhere where it is not in an explicit unification.
> It *would* be nice to give this as a separate error message.
> Unfortunately flattening makes this a little difficult.
> 
> I can wish-list this, but currently I don't know an easy way to tell the
> difference between user-written unifications and introduced ones after
> unravel_unifications is called.

Fine.

> One outstanding open issue is that we don't specify what happens
> when you put an impure call such as
> 		
> 		impure some_pred(foo(42), bar(17))
> 
> Where do the extra unifications get scheduled?

I think the unifications should get scheduled before
the call to the impure procedure.  This is in accordance
with the general principle that in the strict sequential
semantics such unifications get executed depth-first,
and that other semantics are based on the strict sequential
semantics with additional reordering allowed but not over
impure goals.

I think the code that you posted this time does the right thing
with regard to this issue.

> @@ -6527,19 +6634,34 @@
>  			% Should this be insert_... rather than append_...?
>  			% No, because that causes efficiency problems
>  			% with type-checking :-(
> +			% But for impure unifications, we should do
> +			% this, because we can't reorder around the
> +			% functor unification.
> +			( { Purity = pure } ->

I suggest a minor rewording of that comment:

			% But for impure unifications, we need to do
			% this, because mode reordering can't reorder
			% around the functor unification.

> --- purity.m	2000/04/05 08:23:42	1.1
> +++ purity.m	2000/04/11 04:28:47
> @@ -75,13 +75,35 @@
>  %  semipure or impure predicates.  This promise cannot be checked, so we must
>  %  trust the programmer.
>  %
> -%  XXX The current implementation doesn't handle impure functions.  The main
> -%      reason is that handling of nested functions is likely to get pretty 
> -%      confusing.  Because impure functions can't be reordered, the execution
> -%      order would have to be strictly innermost-first, left-to-right, and 
> -%      predicate arguments would always have to be evaluated before the
> -%      predicate call.  Implied modes are right out.  All in all, they just
> -%      won't be as natural as one might think at first.
> +%  See the language reference manual for more information on syntax and
> +%  semantics.
> +%
> +%  The current implementation now handles impure functions. 
> +%  They are limited to being used as part of an explicit unification
> +%  with a purity indicator before the goal.
> +%
> +%  	impure X = some_impure_func(Arg1, Arg2, ....)
> +%  
> +%  Any non-variable arguments to the function are flattened into
> +%  unification goals (see make_hlds__unravel_unifications) which are 
> +%  placed as pure goals before the function call itself.
> +%  This eliminates any need to define some order of evaluation of nested
> +%  impure functions.
> +%  Of course it also eliminates the benefits of using functions to
> +%  cut down on the number of variables introduced.  The main use of
> +%  impure functions is to interface nicely with foreign language
> +%  functions.  

The addition of the sentence starting with "Any non-variable ..."
makes the word "This" in the next sentence refer to the wrong thing.

I suggest you move the "Any non-variable ..." sentence to the end.

> +impure_unification_expr_error(Context, Purity) -->
> +	io__set_exit_status(1),
> +	prog_out__write_context(Context),
> +	io__write_string("Purity error: unification with expression was\n"),
> +	prog_out__write_context(Context),
> +	io__write_string("  "),
> +	write_purity(Purity),
> +	io__write_string(", but expression was not a function call.\n").

I suggest changing "was <purity>" to "was declared `<purity>'".

>  %-----------------------------------------------------------------------------%
> 
> 
> 
> --- reference_manual.texi	2000/04/05 08:24:13	1.1
> +++ reference_manual.texi	2000/04/07 03:47:25
> @@ -4665,7 +4669,8 @@
>  
>  Impure C code relaxes some of these restrictions.  
>  Impure C code may perform I/O and although it cannot update its
> -arguments directly it may update something pointed to by its arguments.
> +arguments directly (unless they have mode @samp{di}) it may update
> +something pointed to by its arguments.

Actually `di' doesn't cover it fully; there's also `mdi',
not to mention more obscure modes such as `bound(...) -> dead'.
Therefore I suggest the following change:

	s/unless they have mode @samp{di}/unless they have an
	appropriate unique mode, e.g. @samp{di}/

> @@ -5374,14 +5380,15 @@
>  
>  @table @dfn
>  @item pure
> -Pure predicates and functions always return the same outputs given the
> -same inputs.  They do not interact with the ``real'' world (i.e., do any
> +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 make any changes to any data
>  structure that will not be undone on backtracking (unless the data
>  structure would be unreachable on backtracking).  The behaviour of pure
>  predicates is never affected by the invocation of pure predicates.
> -It is possible for the invocation of pure predicate to affect the
> +It is possible for the invocation of pure predicates to affect the
>  behaviour of non-pure predicates and vice versa.

I would prefer just dropping the last two sentences.
But that is an existing flaw, not something introduced
by this change, so I don't mind if you go ahead and commit
this change without fixing that; we can debate that point
at length ;-)

> @@ -5527,14 +5538,14 @@
>  @section Promising that a predicate is pure
>  
>  Predicates that are implemented in terms of impure or semipure predicates are
> -assumed to have the @emph{worst impurity} of the goals in their body.
> +assumed to have the lowest bound of the purity of the goals in their body.

"lowest bound" is not quite the right term here.
"greatest lower bound" would be technically correct.
Or more simply you could just write "least" or "least purity".

Apart from the minor points mentioned above, this change looks fine now.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------