Next: Constrained polymorphic modes, Previous: Insts modes and mode definitions, Up: Modes [Contents]
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 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.
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.)
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,
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
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.
Next: Constrained polymorphic modes, Previous: Insts modes and mode definitions, Up: Modes [Contents]