Next: Solver types, Previous: Foreign language interface, Up: Top [Contents]
In order to efficiently implement certain predicates, it is occasionally necessary to venture outside pure logic programming. Other predicates cannot be implemented at all within the paradigm of logic programming, for example, all solutions predicates. Such predicates are often written using the foreign language interface. Sometimes, however, it would be more convenient, or more efficient, to write such predicates using the facilities of Mercury. For example, it is much more convenient to access arguments of compound Mercury terms in Mercury than in C, and the ability of the Mercury compiler to specialize code can make higher-order predicates written in Mercury significantly more efficient than similar C code.
One important aim of Mercury’s impurity system is to make the distinction between the pure and impure code very clear. This is done by requiring every impure predicate or function to be so declared, and by requiring every call to an impure predicate or function to be flagged as such. Predicates or functions that are implemented in terms of impure predicates or functions are assumed to be impure themselves unless they are explicitly promised to be pure.
Please note that the facilities described here are needed only very rarely. The main intent is for implementing language primitives such as the all solutions predicates, or for implementing interfaces to foreign language libraries using the foreign language interface. Any other use of ‘impure’ or ‘semipure’ probably indicates either a weakness in the Mercury standard library, or the programmer’s lack of familiarity with the standard library. Newcomers to Mercury are hence encouraged to skip this section.
Mercury distinguishes three “levels” of purity:
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 (see 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. The declarative semantics of pure predicates is never affected by the invocation of other predicates. It not is possible for the invocation of pure predicates to affect the operational behaviour of non-pure predicates and vice versa.
By default, Mercury predicates and functions are pure. Without using the foreign language interface, writing mode-specific clauses or calling other impure predicates and functions, it is impossible to write impure code in Mercury.
Semipure predicates are just like pure predicates, except that their declarative semantics 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.
Impure predicates may perform I/O or modify hidden state, even if these side effects alter the operational semantics of other code. However, impure predicates may not change the declarative semantics of pure code. They must be type-, mode-, determinism- and uniqueness correct.
The three levels of purity (which we will simply call the purity)
have a total ordering defined upon them: pure > semipure > impure.
It is important to the proper operation of impure and semipure code, to the flexibility of the compiler to optimize pure code, and to the semantics of the Mercury language, that a clear distinction be drawn between ordinary Mercury code and imperative code written with Mercury syntax. How Mercury draws this distinction will be explained below; the purpose of this section is to explain the semantics of programs with impure predicates.
A 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, which by definition are not part of their declarative semantics. Thus it is the operational semantics of impure predicates that Mercury must specify, and Mercury implementations must respect.
The operational semantics of a Mercury predicate which invokes impure code is a modified form of the strict sequential semantics (see Formal semantics). Impure goals 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, pure and 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 computation cannot lead to successful termination.
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 in the program), 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 executed, and so on. Mercury implementations must respect this contextual nature of the semantics of semipure goals; within a single context, an implementation may treat a semipure goal as if it were pure.
Every Mercury predicate or function has exactly two purity values associated with it. One is the declared purity of the predicate or function, which is given by the programmer. The other value is the inferred purity, which is calculated from the purity of goals in the body of the predicate or function.
A predicate is declared to be impure or semipure
by preceding the word pred in its pred declaration
with impure or semipure, respectively.
Similarly, a function is declared impure or semipure
by preceding the word func in its func declaration
with impure or semipure.
That is, the declarations
:- impure pred Pred(Arguments…). :- semipure pred Pred(Arguments…). :- impure func Func(Arguments…) = Result. :- semipure func Func(Arguments…) = Result.
declare the predicate Pred and the function Func to be impure and semipure, respectively.
Type class methods may also be declared as impure or semipure
by preceding the word pred or func
with the appropriate purity level.
An instance of the type class must provide method implementations
that are at least as pure as the method declaration.
If predicate p/N is declared to be impure (semipure)
then all calls to p/N must be annotated
with impure (semipure):
impure p(X1, X2, …, XN)
If function f/N is declared to be impure (semipure)
then all applications of f/N
must be obtained by unification with a variable
and the unification goal as a whole be annotated with impure
impure X = f(X1, X2, …, XN)
Any call or unification goal containing a non-local variable
with inst any that appears in a negated context
(i.e., in a negation or in the condition of an if-then-else goal)
must be given an impure annotation
because it may violate referential transparency.
Compound goals should not have purity annotations.
The compiler will report an error
if a required purity annotation is omitted from a call or unification goal
or if a semipure annotation is used
where an impure annotation is required.
The compiler will report a warning
if a semipure goal is annotated with impure
or a pure goal is annotated with semipure.
The requirement that impure or semipure calls
be marked with impure or semipure
allows someone reading the code to tell which goals are not pure,
making code which relies on side effects somewhat less mysterious.
Furthermore, it means that
if a call is not preceded by impure or semipure,
then the reader can rely on the call having a proper declarative semantics,
without hidden side-effects.
Predicates that are implemented in terms of impure or semipure predicates are assumed to have the least of the purity of the goals in their body. The declared purity of a predicate must not be more pure than the inferred purity; if it is, the compiler must generate an error. If the declared purity is less pure than the inferred purity, the compiler should issue a warning (this is similar to the above case for goals). Because the inferred purity of the predicate is calculated from the declared purity of the calls it executes, the lowest purity bound is propagated up from callee to caller through the program.
In some cases, the impurity of a predicate’s body is an implementation detail which should not be exposed to callers. These predicates are pure or semipure even though they call impure or semipure predicates. The only way for the programmer to stop the propagation of impurity is to explicitly promise that the predicate or function is pure or semipure.
Of course, the Mercury compiler cannot verify that the predicate’s purity matches the promise, so it is the programmer’s responsibility to ensure this. If a predicate is promised pure or semipure and is not, the behaviour of the program is undefined.
The programmer may promise that a predicate or function is pure or semipure
using the promise_pure and promise_semipure pragmas:
:- pragma promise_pure(Name/Arity). :- pragma promise_semipure(Name/Arity).
Programmers should be very careful about mixing code that is promised pure with impure predicates or functions that may manipulate the same hidden state (for example, the impure predicates used to implement a predicate that is promised pure); the ‘promise_pure’ declaration is supposed to promise that impure code cannot change the declarative semantics of pure code. The module system can be used to minimize the possibility of making errors with such code, by keeping impure predicates or functions behind the interface where code is promised pure.
Note that the ‘promise_pure’, ‘promise_semipure’, and ‘promise_impure’ scopes described in Goals may be used to promise purity at the finer level of goals within clauses.
The following example illustrates how a pure predicate may be implemented using impure code. Note that this code is not reentrant, and so is not useful as is. It is meant only as an example.
:- pragma foreign_decl("C", "#include <limits.h>").
:- pragma foreign_decl("C", "extern MR_Integer max;").
:- pragma foreign_code("C", "MR_Integer max;").
:- impure pred init_max is det.
:- pragma foreign_proc("C",
init_max,
[will_not_call_mercury],
"
max = INT_MIN;
").
:- impure pred set_max(int::in) is det.
:- pragma foreign_proc("C",
set_max(X::in),
[will_not_call_mercury],
"
if (X > max) max = X;
").
:- semipure func get_max = (int::out) is det.
:- pragma foreign_proc("C",
get_max = (X::out),
[promise_semipure, will_not_call_mercury],
"
X = max;
").
:- pragma promise_pure(max_solution/2).
:- pred max_solution(pred(int), int).
:- mode max_solution(pred(out) is multi, out) is det.
max_solution(Generator, Max) :-
impure init_max,
(
Generator(X),
impure set_max(X),
fail
;
semipure Max = get_max
).
Higher-order code can manipulate impure or semipure predicates and functions, provided that explicit purity annotations are used in three places: on the higher-order types, on lambda expressions, and on higher-order calls. (There are no purity annotations on higher-order insts and modes, however.)
Ordinary higher-order types,
such as ‘pred(T1, T2)’ and ‘func(T1, T2) = T’,
represent only pure predicates or pure functions.
But for each ordinary higher-order type Foo,
there are two corresponding types
‘semipure Foo’ and ‘impure Foo’.
These types can be used for higher-order code
that needs to manipulate impure or semipure procedures.
For example the type ‘impure func(int) = int’
represents impure functions from int to int.
There are no implicit conversions and no subtyping relationship between ordinary higher-order types and the corresponding impure or semipure higher-order types. However, a value of an ordinary higher-order type can be explicitly “converted” to a value of an impure (or semipure) higher-order type by wrapping it in an impure (or semipure) lambda expression that just calls the pure higher-order term.
Purity annotations are required on lambda expressions that call semipure or impure code. Lambda expressions can be declared as ‘semipure’ or ‘impure’ by including such an annotation before the ‘pred’ or ‘func’ identifier in the lambda expression. Such lambda expressions have the corresponding ‘semipure’ or ‘impure’ higher-order type. For example, the expression
(impure func(X) = Y :- semipure get_max(Y), impure set_max(X))
is an example of an impure function lambda expression with type ‘(impure func(int) = int)’, and the expression
(impure pred(X::in, Y::out) is det :-
semipure get_max(Y),
impure set_max(X))
is an example of an impure predicate lambda expression with type ‘impure pred(int, int)’.
Any calls to impure or semipure higher-order terms must be explicitly annotated as such. For impure or semipure higher-order predicates, the annotation is indicated by putting ‘impure’ or ‘semipure’ before the call. For example:
:- func foo(impure pred(int)) = int.
:- mode foo(in(pred(out) is det)) = out is det.
foo(ImpurePred) = X1 + X2 :-
% Using higher-order syntax.
impure ImpurePred(X1),
% Using the call/N syntax.
impure call(ImpurePred, X2).
For calling impure or semipure higher-order functions, the notation is different than what you might expect. In addition to using an ‘impure’ or ‘semipure’ operator on the unification which invokes the higher-order function application, you must also use ‘impure_apply’ or ‘semipure_apply’ rather than using ‘apply’ or higher-order syntax. For example:
:- func map(impure func(T1) = T2, list(T1)) = list(T2).
map(_ImpureFunc, []) = [].
map(ImpureFunc, [X|Xs]) = [Y|Ys] :-
impure Y = impure_apply(ImpureFunc, X),
impure Ys = map(ImpureFunc, Ys).
Previous: Purity annotations on lambda expressions, Up: Higher-order impurity [Contents]