4.2 Predicate and function mode declarations

A predicate mode declaration assigns a mode mapping to each argument of a predicate. A function mode declaration assigns a mode mapping to each argument of a function, and a mode mapping to the function result. Each mode of a predicate or function is called a procedure. For example, given the mode names defined by

:- mode out_listskel == free >> listskel.
:- mode in_listskel == listskel >> listskel.

the (type and) mode declarations of the function ‘length’ and predicate ‘append’ are as follows:

:- func length(list(T)) = int.
:- mode length(in_listskel) = out.
:- mode length(out_listskel) = in.

:- pred append(list(T), list(T), list(T)).
:- mode append(in, in, out).
:- mode append(out, out, in).

Note that functions may have more than one mode, just like predicates; functions can be reversible.

Alternately, the mode declarations for ‘length’ could use the standard library modes ‘in/1’ and ‘out/1’:

:- func length(list(T)) = int.
:- mode length(in(listskel)) = out.
:- mode length(out(listskel)) = in.

As for type declarations, a predicate or function can be defined to have a given higher-order inst (see Higher-order insts and modes) by using `with_inst` in the mode declaration.

For example,

:- inst foldl_pred == (pred(in, in, out) is det).
:- inst foldl_func == (func(in, in) = out is det).

:- mode p(in) `with_inst` foldl_pred.
:- mode f(in) `with_inst` foldl_func.

is equivalent to

:- mode p(in, in, in, out) is det.
:- mode f(in, in, in) = out is det.

(‘is det’ is explained in Determinism.)

If a predicate or function has only one mode, the ‘pred’ and ‘mode’ declaration can be combined:

:- func length(list(T)::in) = (int::out).
:- pred append(list(T)::in, list(T)::in, list(T)::out).

:- pred p `with_type` foldl_pred(T, U) `with_inst` foldl_pred.

It is an error for a predicate or function whose ‘pred’ and ‘mode’ declarations are so combined to have any other separate ‘mode’ declarations.

If there is no mode declaration for a function, the compiler assumes a default mode for the function in which all the arguments have mode in and the result of the function has mode out. (However, there is no requirement that a function have such a mode; if there is any explicit mode declaration, it overrides the default.)

If a predicate or function type declaration occurs in the interface section of a module, then all mode declarations for that predicate or function must occur in the interface section of the same module. Likewise, if a predicate or function type declaration occurs in the implementation section of a module, then all mode declarations for that predicate or function must occur in the implementation section of the same module. Therefore, is an error for a predicate or function to have mode declarations in both the interface and implementation sections of a module.

A function or predicate mode declaration is an assertion by the programmer that for all possible argument terms and (if applicable) result term for the function or predicate that are approximated (in our technical sense) by the initial instantiatedness trees of the mode declaration and all of whose free variables are distinct, if the function or predicate succeeds, then the resulting binding of those argument terms and (if applicable) result term will in turn be approximated by the final instantiatedness trees of the mode declaration, with all free variables again being distinct. We refer to such assertions as mode declaration constraints. These assertions are checked by the compiler, which rejects programs if it cannot prove that their mode declaration constraints are satisfied.

Note that with the usual definition of ‘append’, the mode

:- mode append(in_listskel, in_listskel, out_listskel).

would not be allowed, since it would create aliasing between the different arguments — on success of the predicate, the list elements would be free variables, but they would not be distinct.

In Mercury it is always possible to call a procedure with an argument that is more bound than the initial inst specified for that argument in the procedure’s mode declaration. In such cases, the compiler will insert additional unifications to ensure that the argument actually passed to the procedure will have the inst specified. For example, if the predicate p/1 has mode ‘p(out)’, you can still call ‘p(X)’ if X is ground. The compiler will transform this code to ‘p(Y), X = Y’ where Y is a fresh variable. It is almost as if the predicate p/1 has another mode ‘p(in)’; we call such modes “implied modes”.

To make this concept precise, we introduce the following definition. A term satisfies an instantiatedness tree if for every node in the instantiatedness tree,

• if the node is “free”, then the corresponding node in the term (if any) is either a distinct free variable, or a function symbol.
• if the node is “bound”, then the corresponding node in the term (if any) is a function symbol.

The mode set for a predicate or function is the set of mode declarations for the predicate or function. A mode set is an assertion by the programmer that the predicate should only be called with argument terms that satisfy the initial instantiatedness trees of one of the mode declarations in the set (i.e. the specified modes and the modes they imply are the only allowed modes for this predicate or function). We refer to the assertion associated with a mode set as the mode set constraint; these are also checked by the compiler.

A predicate or function p is well-moded with respect to a given mode declaration if given that the predicates and functions called by p all satisfy their mode declaration constraints, there exists an ordering of the conjuncts in each conjunction in the clauses of p such that

• p satisfies its mode declaration constraint, and
• p satisfies the mode set constraint of all of the predicates and functions it calls

We say that a predicate or function is well-moded if it is well-moded with respect to all the mode declarations in its mode set, and we say that a program is well-moded if all its predicates and functions are well-moded.

The mode analysis algorithm checks one procedure at a time. It abstractly interprets the definition of the predicate or function, keeping track of the instantiatedness of each variable, and selecting a mode for each call and unification in the definition. To ensure that the mode set constraints of called predicates and functions are satisfied, the compiler may reorder the elements of conjunctions; it reports an error if no satisfactory order exists. Finally it checks that the resulting instantiatedness of the procedure’s arguments is the same as the one given by the procedure’s declaration.

The mode analysis algorithm annotates each call with the mode used.