Next: Unique modes, Previous: Types, Up: Top [Contents]
The mode of a predicate, or function, is a mapping from the initial state of instantiation of the arguments of the predicate, or the arguments and result of a function, to their final state of instantiation. To describe states of instantiation, we use information provided by the type system. Types can be viewed as regular trees with two kinds of nodes: or-nodes representing types and and-nodes representing constructors. The children of an or-node are the constructors that can be used to construct terms of that type; the children of an and-node are the types of the arguments of the constructors. We attach mode information to the or-nodes of type trees.
An instantiatedness tree is an assignment of an instantiatedness — either free or bound — to each or-node of a type tree, with the constraint that all descendants of a free node must be free.
A term is approximated by an instantiatedness tree if for every node in the instantiatedness tree,
When an instantiatedness tree tells us that a variable is bound, there may be several alternative function symbols to which it could be bound. The instantiatedness tree does not tell us which of these it is bound to; instead for each possible function symbol it tells us exactly which arguments of the function symbol will be free and which will be bound. The same principle applies recursively to these bound arguments.
Mercury’s mode system allows users to declare names for instantiatedness trees using declarations such as
:- inst listskel == bound([] ; [free | listskel]).
This instantiatedness tree describes lists
whose skeleton is known but whose elements are distinct variables.
As such, it approximates the term [A,B]
but not the term [H|T] (only part of the skeleton is known),
the term [A,2] (not all elements are variables),
or the term [A,A] (the elements are not distinct variables).
As a shorthand, the mode system provides free and ground
as names for instantiatedness trees
all of whose nodes are free and bound respectively
(with the exception of solver type values
which may be semantically ground,
but be defined in terms of non-ground solver type values;
see Solver types for more detail).
The shape of these trees is determined
by the type of the variable to which they apply.
A more concise, alternative syntax exists
for bound instantiatedness trees:
:- inst maybeskel
---> no
; yes(free).
which is equivalent to writing
:- inst maybeskel == bound(no ; yes(free)).
You can specify what type (actually what type constructor)
an inst is intended to be used on
by adding for, followed by the name and arity of that type constructor,
after the name of the inst, like this:
:- inst maybeskel for maybe/1
---> no
; yes(free).
This can be useful documentation, and the compiler will generate an error message when an inst that was declared to be for values of one type constructor is applied to values of another type constructor.
As execution proceeds, variables may become more instantiated.
A mode mapping is a mapping
from an initial instantiatedness tree to a final instantiatedness tree,
with the constraint that no node of the type tree
is transformed from bound to free.
Mercury allows the user to specify mode mappings directly
by expressions such as inst1 >> inst2,
or to give them a name using declarations such as
:- mode m == inst1 >> inst2.
Two standard shorthand modes are provided, corresponding to the standard notions of inputs and outputs:
:- mode in == ground >> ground. :- mode out == free >> ground.
Though we do not recommend this, Prolog fans who want to use the symbols ‘+’ and ‘-’ can do so by simply defining them using a mode declaration:
:- mode (+) == in. :- mode (-) == out.
These two modes are enough for most functions and predicates. Nevertheless, Mercury’s mode system is sufficiently expressive to handle more complex data-flow patterns, including those involving partially instantiated data structures, i.e. terms that contain both function symbols and free variables, such as ‘f(a, b, X)’. In the current implementation, partially instantiated data structures are unsupported due to a lack of alias tracking in the mode system. For more information, please see the LIMITATIONS.md file distributed with Mercury.
For example, consider an interface to a database that associates data with keys, and provides read and write access to the items it stores. To represent accesses to the database over a network, you would need declarations such as
:- type operation
---> lookup(key, data)
; set(key, data).
:- inst request for operation/0
---> lookup(ground, free)
; set(ground, ground).
:- mode create_request == free >> request.
:- mode satisfy_request == request >> ground.
‘inst’ and ‘mode’ declarations can be parametric. For example, the following declaration
:- inst listskel(Inst) for list/1
---> []
; [Inst | listskel(Inst)].
defines the inst ‘listskel(Inst)’ to be a list skeleton
whose elements have inst Inst;
you can then use insts such as ‘listskel(listskel(free))’,
which represents the instantiation state of a list of lists of free variables.
The standard library provides the parametric modes
:- mode in(Inst) == Inst >> Inst. :- mode out(Inst) == free >> Inst.
so that for example the mode ‘create_request’ defined above could have be defined as
:- mode create_request == out(request).
There must not be more than one inst definition with the same name and arity in the same module. Similarly, there must not be more than one mode definition with the same name and arity in the same module.
Note that user-defined insts and modes may not have names that have meanings in Mercury. (Most of these are documented in later sections.)
The list of reserved inst names is
=< any bound bound_unique clobbered clobbered_any free ground is mostly_clobbered mostly_unique mostly_unique_any not_reached unique unique_any
The list of reserved mode names is
= >> any_func any_pred func is pred
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,
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.
Mode declarations for predicates and functions may also have inst parameters. However, such parameters must be constrained to be compatible with some other inst. In a predicate or function mode declaration, an inst of the form ‘InstParam =< Inst’, where InstParam is a variable and Inst is an inst, states that InstParam is constrained to be compatible with Inst, that is, InstParam represents some inst that can be used anywhere where Inst is required. If an inst parameter occurs more than once in a declaration, it must have the same constraint on each occurrence.
For example, in the mode declaration
:- mode append(in(list_skel(I =< ground)), in(list_skel(I =< ground)),
out(list_skel(I =< ground))) is det.
I is an inst parameter which is constrained to be ground.
If ‘append’ is called with the first two arguments
having an inst of, say, ‘list_skel(bound(f))’,
then after ‘append’ returns,
all three arguments will have inst ‘list_skel(bound(f))’.
If the mode of append had been simply
:- mode append(in(list_skel(ground)), in(list_skel(ground)),
out(list_skel(ground))) is det.
then we would only have been able to infer an inst of ‘list_skel(ground)’ for the third argument, not the more specific inst.
Note that attempting to call ‘append’ when the first two arguments do not have ground insts (e.g. ‘list_skel(bound(g(free)))’) is a mode error because it violates the constraint on the inst parameter.
To avoid having to repeat a constraint everywhere that an inst parameter occurs, it is possible to list the constraints after the rest of the mode declaration, following a ‘<=’. E.g. the above example could have been written as
:- (mode append(in(list_skel(I)), in(list_skel(I)),
out(list_skel(I))) is det) <= I =< ground.
Note that in the current Mercury implementation this syntax requires parentheses around the ‘mode(…) is Det’ part of the declaration.
Also, if the constraint on an inst parameter is ‘ground’ then it is not necessary to give the constraint in the declaration. The example can be further shortened to
:- mode append(in(list_skel(I)), in(list_skel(I)), out(list_skel(I)))
is det.
Constrained polymorphic modes are particularly useful when passing objects with higher-order types to polymorphic predicates, since they allow the higher-order mode information to be retained (see Higher-order).
Because the compiler automatically reorders conjunctions to satisfy the modes, it is often possible for a single clause to satisfy different modes. However, occasionally reordering of conjunctions is not sufficient; you may want to write different code for different modes.
For example, the usual code for list append
append([], Ys, Ys).
append([X|Xs], Ys, [X|Zs]) :-
append(Xs, Ys, Zs).
works fine in most modes, but is not very satisfactory for the ‘append(out, in, in)’ mode of append, because although every call in this mode only has at most one solution, the compiler’s determinism inference will not be able to infer that. This means that using the usual code for append in this mode will be inefficient, and the overly conservative determinism inference may cause spurious determinism errors later.
For this mode, it is better to use a completely different algorithm:
append(Prefix, Suffix, List) :-
list.length(List, ListLength),
list.length(Suffix, SuffixLength),
PrefixLength = ListLength - SuffixLength,
list.split_list(PrefixLength, List, Prefix, Suffix).
However, that code does not work in the other modes of ‘append’.
To handle such cases, you can use mode annotations on clauses, which indicate that particular clauses should only be used for particular modes. To specify that a clause only applies to a given mode, each argument Arg of the clause head should be annotated with the corresponding argument mode Mode, using the ‘::’ mode qualification operator, i.e. ‘Arg :: Mode’.
For example, if ‘append’ was declared as
:- pred append(list(T), list(T), list(T)). :- mode append(in, in, out). :- mode append(out, out, in). :- mode append(in, out, in). :- mode append(out, in, in).
then you could implement it as
append(L1::in, L2::in, L3::out) :- usual_append(L1, L2, L3).
append(L1::out, L2::out, L3::in) :- usual_append(L1, L2, L3).
append(L1::in, L2::out, L3::in) :- usual_append(L1, L2, L3).
append(L1::out, L2::in, L3::in) :- other_append(L1, L2, L3).
usual_append([], Ys, Ys).
usual_append([X|Xs], Ys, [X|Zs]) :- usual_append(Xs, Ys, Zs).
other_append(Prefix, Suffix, List) :-
list.length(List, ListLength),
list.length(Suffix, SuffixLength),
PrefixLength = ListLength - SuffixLength,
list.split_list(PrefixLength, List, Prefix, Suffix).
This language feature can be used to write “impure” code that does not have any consistent declarative semantics. For example, you can easily use it to write something similar to Prolog’s (in)famous ‘var/1’ predicate:
:- mode var(in). :- mode var(free>>free). var(_::in) :- fail. var(_::free>>free) :- true.
As you can see, in this case the two clauses are not equivalent.
Because of this possibility, predicates or functions which are defined using different code for different modes are by default assumed to be impure; the programmer must either (1) carefully ensure that the logical meaning of the clauses is the same for all modes, which can be declared to the compiler through a ‘pragma promise_equivalent_clauses’ declaration, or a ‘pragma promise_pure’ declaration, or (2) declare the predicate or function as impure. See Impurity.
In the example with ‘append’ above, the two ways of implementing append do have the same declarative semantics, so we can safely use the first approach:
:- pragma promise_equivalent_clauses(append/3).
The pragma
:- pragma promise_pure(append/3).
would also promise that the clauses are equivalent, but on top of that would also promise that the code of each clause is pure. Sometimes, if some clauses contain impure code, that is a promise that the programmer wants to make, but this extra promise is unnecessary in this case.
In the example with ‘var/1’ above, the two clauses have different semantics, so the predicate must be declared as impure:
:- impure pred var(T).
Previous: Constrained polymorphic modes, Up: Modes [Contents]