[m-dev.] For review: Make Mercury cope with impure code (part 2/2)

[Fergus Henderson]

Peter Schachte, you wrote:
> + at node Purity
> + at section Purity declarations
> +
> +Clearly the C interface makes it quite possible to create an impure
> +Mercury predicate.  By ``impure'' we mean a predicate that does not have
> +a consistent logical semantics, though it does have a procedural
> +semantics.  It is also quite possible to implement predicates that have
> +a perfectly consistent logical semantics although they call predicates
> +that do not.  The purpose of Mercury's impurity system is to allow users
> +to do this without having the Mercury compiler incorrectly compile the
> +impure code because it made invalid assumptions about impure predicates
> +that would have been valid for pure code, while still allowing the
> +compiler to optimize pure code agressively.  For example, if two
> +identical pure goals appear in a conjunction, one of them may safely be
> +removed; however, if the identical goals modify some global state,
> +removing one of them may not preserve the procedural semantics.
> +
> +One important aim of the impurity system is to make the distinction
> +between the pure and impure code very clear.  This is done by requiring
> +every impure predicate to be so declared, and by requiring every call to
> +an impure predicate to be flagged as such.  Predicates that are
> +implemented in terms of impure predictes are assumed to be impure
> +themselves unless they are explicitly promised to be pure.

I think we need some more material here on both rationale (why do we
have impurity declarations?) and advice about usage (when should
programmers use impure code?).  You say "The purpose of Mercury's
impurity system is to allow users to do this [use impure code] without
[various problems]", but why allow users to use impure code in the
first place?

Also the definition of `consistent logical semantics' is not clear.
Somewhere here we should mention something about the procedural
semantics being sound with respect to the declarative semantics.

The "Semantics" chapter also needs revisiting.
The documentation here does not adequately document
the operational semantics of impure goals.

Probably we should sit down together and have a go at both of these.

> + at node Purity levels
> + at subsection Choosing the right level of purity
> +
> +Mercury distinguishes three ``levels'' of purity:
> +
> + at table @dfn
> + at 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
> +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 behavior of other
> +predicates is never affected by the invocation of pure predicates, nor
> +is the behavior of pure predicates ever affected by the invocation of
> +other predicates.
> +
> +Most Mercury predicates are pure.  
> +
> + at item semipure
> +Semipure predicates are just like pure predicates, except that their
> +behavior may be affected by the invocation of impure predicates.  That
> +is, they are sensitive to the state of the computation other than as
> +reflected by their input arguments, though they do not affect the state
> +themselves.
> +
> + at item impure
> +Impure predicates may do anything, including changing the state of the
> +computation.

There are some interactions between purity and determinism that need to
be discussed here.  E.g. `det' doesn't really mean deterministic for
impure goals.  Also the compiler should not automatically prune impure goals
with no output variables.

> + at node Impure calls
> + at subsection Marking a call as impure
> +
> +If a predicate is impure (semipure), all calls to it must be preceded
> +with the word @code{impure} (@code{semipure}).  This allows someone
> +reading the code to tell which goals are not pure, making code which
> +relies on side effects somewhat less mysterious.  See @ref{Impurity
> +Example} for an example of this.  Note that only predicate calls need to
> +be prefixed with @code{impure} or @code{semipure}, compound goals never
> +need this.

I'd be inclined to drop the last sentence.

> + at node Promising purity
> + at subsection Promising a predicate is pure
> +
> +Some predicates which call impure or semipure predicates are themselves
> +pure.  In fact, the main purpose of the Mercury impurity system is to
> +allow users to write pure predicates using impure ones, while protecting
> +the procedural implementation from aggressive compiler optimizations.
> +Of course, the Mercury compiler cannot verify that a predicate is pure,
> +so this is the user's responsibility.

What happens if the user gets it wrong?
You should document that the behaviour is undefined in that case.

> + at node Impurity Example
> + at subsection An example using impurity
> +
> +The following example illustrates how a pure predicate may be
> +implemented using impure code.  Note that this code has some important
> +flaws (though it does work), and so is not useful as is.  It is meant
> +only as an example.

What are the flaws?

> + at example
> +:- pragma c_header_code("int max;").
> +
> +:- impure pred init_max is det.
> +:- pragma c_code(init_max,
> +        will_not_call_mercury,
> +        "max = (int)(~(((unsigned)(~0))>>1));").

How about "max = INT_MIN" instead?
(You'd also need `:- pragma c_header_code("#include <limits.h>")'.)

> +:- impure pred set_max(int::in) is det.
> +:- pragma c_code(set_max(X::in),
> +        will_not_call_mercury,
> +        "if (X>max) max = X;").

s/>/ > /


> diff -u -r1.15 nc_builtin.nl
> --- nc_builtin.nl	1997/07/27 15:06:59	1.15
> +++ nc_builtin.nl	1997/10/02 05:45:10
> @@ -41,8 +41,6 @@
>  % :- op(1199, fx, (use_op)).
>  
>  % :- op(1199, fx, (rule)).
> -% :- op(1199, fx, (pred)).
> -:- op(1199, fx, (func)).
>  
>  :- op(1199, fx, (pragma)).
>  :- op(1199, fx, (mode)).
> @@ -51,6 +49,11 @@
>  :- op(1175, xfx, (::)).
>  
>  :- op(950, fxy, (lambda)).
> +
> +% :- op(800, fx, (pred)).
> +:- op(800, fx, (func)).

The reason that the original `:- op' declaration for `pred'
was commented out in nc_builtin.nl is that NU-Prolog already
has `pred' as a built-in operator, with precedence 1199.

But if you're changing the precedence to 800, then you'll
need to redefine it (using the same technique as is done
for `:').

> Index: library/ops.m
> +ops__op_table("impure", before, fy, 800).	% Mercury extension (NYI)
[...]
> +ops__op_table("semipure", before, fy, 800).	% Mercury extension (NYI)

You can delete `(NYI)' since they're implemented now.

> New File: compiler/purity.m
> ===================================================================
> %-----------------------------------------------------------------------------%
> % Copyright (C) 1995 University of Melbourne.

Copyright date is wrong.

> % This file may only be copied under the terms of the GNU General
> % Public License - see the file COPYING in the Mercury distribution.
> %-----------------------------------------------------------------------------%
> % 
> % File      : purity.m
> % Authors   : pets (Peter Schachte)
> % Stability : low

The "Stability" comments are intended only for library modules.
I don't think there is much point putting them on modules in the
compiler directory.

> %  Calls to impure predicates may not be optimized away.  Neither may they be
> %  reodered relative to any other goals in a given conjunction; ie, an impure
> %  goal cleaves a conjunction into the stuff before it and the stuff after it.
> %  Both of these groups may be reordered separately, but no goal from either
> %  group may move into the other.

Ditto for disjunctions.

> %  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 jsut
> %      won't be as natural as one might think at first.

s/jsut/just/

> %  Sort of a "maximum" for impurity.
> :- pred worst_purity(purity, purity, purity).
> :- mode worst_purity(in, in, out) is det.

Gee, the use of "worst" seems like a bit of a value-judgement to me ;-)

> %  Add the the feature corresponding to a purity to a feature list.
> :- pred add_goal_info_purity_feature(hlds_goal_info, purity, hlds_goal_info).
> :- mode add_goal_info_purity_feature(in, in, out) is det.

s/the the/the/

> add_goal_info_purity_feature(GoalInfo0, pure, GoalInfo) :-
> 	goal_info_remove_feature(GoalInfo0, (semipure), GoalInfo1),
> 	goal_info_remove_feature(GoalInfo1, (impure), GoalInfo).

That behaviour doesn't match the documentation.

> infer_goal_info_purity(GoalInfo, Purity) :-
> 	(   goal_info_has_feature(GoalInfo, (impure)) ->
> 		Purity = (impure)
> 	;
> 	     goal_info_has_feature(GoalInfo, (semipure)) ->
> 		Purity = (semipure)
> 	;
> 		Purity = pure
> 	).

Slightly inconsistent indentatino.

[... to be continued...]

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