Next: Predicate and function mode declarations, Up: Modes [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
Next: Predicate and function mode declarations, Up: Modes [Contents]