Next: , Up: Modes   [Contents]

4.1 Insts, modes, and mode definitions

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(ground).

which is equivalent to writing

:- inst maybeskel == bound(no ; yes(ground)).

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.

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. data structures with “free” holes in them. (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 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
	--->	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) ---> [] ; [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.

Next: , Up: Modes   [Contents]