Modes and their precise meaning

[Note: If you want to follow or participate in the conversation please post see the Prolog Community Discourse area for this PIP]

Problem and objectives

What do we mean by modes?

In Prolog “modes” refer in general to the different ways in which a predicate can be called. For example, given the standard definition of length/2, one of the normally intended uses is to provide a list in the first argument and obtain an integer representing its length in the second argument. A different use is to provide the integer and obtain a list of variables. And there are more possible uses. These different uses are refereed to as the “modes” of the predicate. Such modes are useful for many purposes; a traditional one is program documentation.

In order to specify such predicate modes, usually some special terms are used to define the expected instantiation state of each of the arguments of the predicate. These special terms can be atoms (such as +, -, ?, @, etc.) or more complex terms (such as +list, -list, ?list, @list, etc.). These terms themselves are also sometimes referred to as modes. To distinguish the two uses of the word we will call them herein argument modes (also called ModeSpecs) and predicate modes. Predicate mode(s) can then be expressed using argument modes in a number of different ways:

‘Classical’ mode declarations (stemming from Dec10/Quintus Prolog) such as:
```
  :- mode length(+,-). % Computes the length of a list.
```

Modes are often used in comments, such as:

  % length(+list,-int): Computes the length of a list.

Some systems allow machine readable comments, which are generally used to generate documentation, such as:
```
  %! length(+list,-int): Computes the length of a list.
```
Predicate modes can also be expressed via assertions, which can also contain argument modes, such as in:
```
  :- pred length(+list,-int) # "Computes the length of a list.".
```

Focus for now

Our focus here (at least initially) is on the argument modes, rather than on the predicate modes in which they appear. We can deal with this later.
We will want to eventually add modes like :,
Another issue that we leave open for now is the names of the types or properties (list, int, etc.) used as arguments of modes.
Also, we should eventually extend the PIP to cover determinism and on-failure, but we are limiting to modes for now to focus discussion. That could also be a separate PIP.

Is there a problem with the argument modes?

The exact meaning of the terms used in argument modes (the +, -, etc.), or even modes in general, has not been traditionally a matter of debate among Prolog developers or programmers, probably because the classical understanding of modes has been sufficient for the traditional purpose of informal documentation.

However, there are indeed issues that need agreement on, specially if modes are used for other purposes such as precise documentation, and, specially, if they are used to guide program optimizations or in program verification.

As just an example, given a declaration such as:

:- mode length(+,-).

does it mean that the second argument can only be a variable (var/1) when the predicate is called? Does it mean that this argument will be bound (nonvar/1) on success? The ISO standard includes the following definition:

- : The argument shall be a variable that will be instantiated if the goal succeeds

The SICStus Prolog 4 manual states:

-ArgName : The argument is an output argument. Usually, but not always, this implies that the argument should be uninstantiated.

Whereas the SWI the manual states:

- : Argument is an output argument. It may or may not be bound at call-time.

This situation has been recognized by some Prolog systems. For example, Ciao Prolog addresses it by making modes definable and the problem is also acknowledged for example in the SWI manual.

The following section lists the stated meanings of argument modes in the standard and in some popular Prolog systems.

Modes in the standard and in different Prolog systems

Modes in the ISO standard

The ISO standard uses modes as a shorthand in the explanation of the different predicates, but does not give a role to modes within the language. The corresponding text in the standard is:

8.1.2.2 Mode of an argument

The mode of each argument defines whether or not an argument shall be instantiated when the built-in predicate is executed. The mode is one of the following atoms:

+ : the argument shall be instantiated,

? : the argument shall be instantiated or a variable,

@ : the argument shall remain unaltered,

- : the argument shall be a variable that will be instantiated if the goal succeeds

NOTE 1 - When the argument is an atomic term, there is no difference between the modes + and @. The mode @ is therefore used only when the argument may be a compound term.

Issue: @ also implies nonvar/1 on call?

Ciao

Ciao Prolog uses modes (and, more generally, assertions) for many purposes including formal documentation, verification, optimization, guiding the analyses, defining interfaces, etc. As mentioned before, in Ciao the meaning of modes can be defined by users and they act as ‘property macros’ that expand to Ciao’s assertions. Because of the different definitions used in the community for modes, the Ciao system library has traditionally included a number of different ‘modes packages’ so that that a user can choose to use ‘ISO modes’, ‘classical modes’, etc. This allows choosing the mode definitions to be used, if any, in a given module. We show some examples. In these we also illustrate the formal mode description used by Ciao to define modes, to which we will return later.

As a first example, the Ciao isomodes package defines the following (we only deal for now with the simple argument modes, i.e., not including types, etc.):

+ : the argument should be nonvar/1 on calls.
  :- modedef +(A) : nonvar(A).
? : no conditions on the argument.
  :- modedef ?(_).
@ : the argument is not further instantiated on success.
  :- modedef @(A) : nonvar(A) + not_further_inst(A).
- : the argument is var/1on calls and nonvar/1 on success.
  :- modedef -(A) : var(A) => nonvar(A).

The standard seems to imply that @ implies nonvar on calls?

Another issue is that for - is that the standard says that on success the argument will be instantiated if the goal succeeds, i.e.:

:- modedef -(A) : var(A) => nonvar(A).

but then it says that the only error possible is for not meeting the var/1 condition on calls, so it is not really clear what should happen on success.

As another example, the Ciao modes package defines the following:

+ : the argument is nonvar/1 on calls.
  :- modedef +(A) : nonvar(A).
- : the argument is nonvar/1 on success.
  :- modedef  -(A) => nonvar(A).
? : no conditions on the argument.
  :- modedef ?(_).
@ : the argument is not further instantiated on success.
  :- modedef @(A) : nonvar(A) + not_further_inst(A).
Other potentially Useful input-output modes

in : the argument is ground/1 on calls and on success.
 :- modedef in(A)  : ground(A) => ground(A).
++ : alias for in.
 :- modedef in(A)  : ground(A) => ground(A).
out : the argument is var/1 on calls and ground/1 on success.
 :- modedef out(A) : var(A)    => ground(A).
go : the argument is ground/1 on success.
 :- modedef go(A)              => ground(A). 

The Ciao approach provides a solution to the problem of multiple meanings for modes but it is clear that it would be very convenient to have at least one set of modes that all the different Prolog systems agree on.

Eclipse

The Eclipse manual defines in the chapter “Terminology” the following modes:

+X : This denotes an input argument. Such an argument must be instantiated before a predicate is called.

++X : This denotes a ground argument. Such an argument can be complex, but must be fully instantiated, i.e., not contain any variables.

–X : This denotes an output argument. Such an argument is allowed to be uninstantiated at call time. When this mode is used in the description of a built-in or library predicate, it is only descriptive. This means that the predicate can be called with an instantated argument, but it will behave as if were called with an uninstantiated variable which is then unified with the actual argument after returning from the call (e.g. atom_length(abc,3) behaves the same as atom_length(abc,L),L=3). If this mode is used in a mode/1 declaration, it is prescriptive, i.e. it is taken as a promise that the predicate will always be called with an uninstantiated variable, and that the compiler is allowed to make corresponding optimizations. Violating this promise will lead to unexpected failures.

?X : This denotes an input or an output argument. Such an argument may be either instantiated or not when the predicate is called.

It also further specifies the prescriptive use of modes in mode declarations as follows:

The ECLiPSe compiler makes use of the mode information mainly to improve indexing and to reduce code size.

Mode declarations are optional. They specify the argument instantiation patterns that a predicate will be called with at runtime, for example:
:- mode p(+), q(-), r(++, ?).
The possible argument modes and their meaning are:

+ : the argument is instantiated, i.e., it is not a variable;

++ : the argument is ground;

- : the argument is not instantiated, it must be a free variable without any constraints, especially it must not occur in any other argument and it cannot be a suspending variable;

? : the mode is not known or it is neither of the above ones.

Note that, if the actual instantiation of a predicate call violates its mode declaration, the behaviour is undefined. Usually, an unexpected failure occurs in this case.

GNU

From the GNU manual:

The mode specifies whether or not the argument must be instantiated when the built-in predicate is called. … Possible modes are:

+ : the argument must be instantiated.

- : the argument must be a variable (will be instantiated if the built-in predicate succeeds).

? : the argument can be instantiated or a variable.

LogTalk

: Argument must be instantiated (but not necessarily ground).

: Argument should be a free (non-instantiated) variable. When bound, the call will unify the computed term with the given argument.

? : Argument can either be instantiated or free.

@ : Argument will not be further instantiated (modified).

++ : Argument must be ground.

– : Argument must be unbound. Used mainly when returning an opaque term (e.g., a stream handle).

SICStus

In SICStus modes are mainly used for documentation in the manuals. The system accepts traditional (Dec10/Quintus-style) declarations, but they are ignored. The stated meaning of modes has evolved from SICStus 3 to SICStus 4:

SICStus 3

1.2 Mode Spec

When introducing a built-in predicate, we shall present its usage with a mode spec, which has the form name(arg, . . ., arg), where each arg denotes how that argument should be instantiated in goals, and has one of the following forms:

:ArgName : This argument should be instantiated to a term denoting a goal or a clause or a predicate name, or that otherwise needs special handling of module prefixes. The argument is subject to module name expansion.

+ArgName : This argument should be instantiated to a non-variable term.

-ArgName : This argument should be uninstantiated.

?ArgName : This argument may or may not be instantiated.

and, in block declarations:

A block condition evaluates to true if and only if all arguments specified as ‘-’ are uninstantiated, in which case the goal is blocked until at least one of those variables is instantiated.

SICStus 4

1.2 Mode Spec

When describing a predicate, we present its usage with a mode spec, which has the form name(arg, . . . , arg), where each arg denotes how that argument is used by the predicate, and has one of the following forms:

:ArgName : The argument is used as a term denoting a goal or a clause or a predicate name, or that otherwise needs special handling of module prefixes. It is subject to module name expansion

+ArgName : The argument is an input argument. Usually, but not always, this implies that the argument should be instantiated.

-ArgName : The argument is an output argument. Usually, but not always, P> this implies that the argument should be uninstantiated.

?ArgName : The argument may be used for both input and output. Please note: The reference pages for built-in predicate use slightly different mode specs.

SWI

The SWI manual refers to argument mode indicators, and states that they are not a formal part of the language. They are intended to help in explaining intended semantics to the programmer. It uses the following definitions in its documentation (abridged):

++ : At call time, the argument must be ground, i.e., the argument may not contain any variables that are still unbound.

+ : At call time, the argument must be instantiated to a term satisfying some (informal) type specification. The argument need not necessarily be ground.

- : Argument is an output argument. It may or may not be bound at call-time. If the argument is bound at call time, the goal behaves as if the argument were unbound, and then unified with that term after the goal succeeds.

-- : At call time, the argument must be unbound. This is typically used by predicates that create ‘something’ and return a handle to the created object, such as open/3, which creates a stream.

?: At call time, the argument must be bound to a partial term (a term which may or may not be ground) satisfying some (informal) type specification. Note that an unbound variable is a partial term. Think of the argument as either providing input or accepting output or being used for both input and output.

@ : Argument will not be further instantiated than it is at call-time.

XSB

XSB distinguishes between ‘call modes’ and ‘success modes’. The traditional declarations, such as:

:- mode append(+,?.?).

indicate what needs to hold when a predicate is called, and a separate declaration, such as:

:- mode_on_success append(+,?,+).

declares what needs to hold when a predicate succeeds. The allowed mode designations for arguments are + for ground, and ? for nonground (or unknown).

Objectives

The need for a precise definition is specially relevant in systems like Eclipse, where they are used in optimization, or like Ciao Prolog, where modes are checked both at compile-time and at run-time (the latter if static checking cannot discharge the proof obligations). However, an agreed-upon set of modes should arguably be of general advantage to all Prologs, at the very least to make the meaning of documentation more uniform and precise.

A first set of objectives for this PIP is thus as follows:

Adopt, for the purposes of the PIP, a compact notation for describing the meaning of modes.
Agree on the meaning of each of the argument modes in common use, and express it precisely.

Other objectives which may be addressed later:

Adopt a common syntax for expressing predicate modes in comments, mode declarations, etc.
Capture also determinacy and (non)failure characteristics.
Describe the meaning of a combination of modes and how to express them.

A notation for modes

For conciseness and precision, we propose to use in this PIP the Ciao notation for argument modes:

Simple modes

An argument mode implies that a set of call and success properties must hold at call or success time for the head argument of the predicate that it is applied to. Argument modes are defined in a compact way by means of modedef declarations, with syntax:

:- modedef <argument mode symbol>(<variable>)
   [   : <call properties>    ]
   [  => <success properties> ]
   [   # "<comment>".         ] .

<argument mode symbol> is, e.g.,+,-,@`, etc. (any Prolog atom can be used).
<call properties> is either a property or a conjunction of properties that must hold for that argument at call time.
<success properties> is either a property or a conjunction of properties that must hold for that argument at success time.
<comment> is a string in markdown (md dialect unspecified).

All fields within […] are optional (this syntax is derived from the Ciao assertion syntax).

Once defined, such modes can be applied to predicate arguments in comments, declarations, assertions, etc. The meaning of this application is that the call and success properties defined by the mode hold for the argument to which the mode is applied at predicate call or success time. Thus, a mode is conceptually a “macro of properties.”

Properties used in mode definitions

As properties that can be used in modedef declarations we can consider:

nonvar/1: the argument is not a variable.
var/1: the argument is a variable.
ground/1: the argument is ground.
etc.

This list is to be completed, i.e., we may wan to define a set of these properties and what they mean. This is a given of course if the property is a Prolog builtin.

For example, given the following mode definitions:

:- modedef +A : nonvar(A) # "`A` is bound upon predicate entry.".
:- modedef ?A # "No conditions are placed on `A`.".

and, e.g., the declaration:

:- mode length(+,?). % Computes the length of a list.

or the comment:

% length(+,?): Computes the length of a list.

The implication is that the first argument of length/2 should be instantiated at call time.

We can define properties using a prop declaration, e.g.:

:- prop var(X) # "`X` is a free variable.".

Modes indicating global properties

There are some properties traditionally expressed with modes that do not refer to the state of computation at call or success time, but rather to more complex properties across the execution of the predicate. These properties are stated in an additional field of the modedefdeclaration for ‘global properties’:

:- modedef <argument mode symbol>(<variable>)
   [   : <call properties>    ]
   [  => <success properties> ]
   [   + <gloabl properties>  ]
   [   # "<comment>".         ] .

For example:

:- prop not_further_inst(A) # "`A` is not further instantiated by
the execution

:- modedef  @(A) +  not_further_inst(A).

Examples

The following is an example of a set of simple modes:

:- modedef  +(A) :  nonvar(A).
:- modedef  -(A) => nonvar(A).
:- modedef --(A) :  var(A).
:- modedef ++(A) : ground(A) => ground(A).
:- modedef  ?(_).
:- modedef  @(A) +  not_further_inst(A).

(note that the meaning of - given above is not the one in the ISO standard). And these are some possible definitions of some less standard modes:

:- modedef in(A)  : ground(A) => ground(A).
:- modedef out(A) : var(A)    => ground(A). 
:- modedef go(A)              => ground(A).

Modes indicating also types (compound/parametric modes)

Modes are often also used to indicate types and other properties in addition to instantiation state. E.g., using:

+list

+A :: list

to indicate that an argument should be instantiated to a list. The modedef and prop notations can also be used in this case.

For example, to define + <type>, with <type> any type or property, meaning that on calls the argument should be instantiated to a term of , we can write:

:- modedef  +(A,P) : P(A). % Implies nonvar(A)

(or, if one wants to avoid the ho notation, we can agree to write call(P,A), type(P,a), etc.).

Proposal (WIP!)

The following is an (evolving) proposal for the meaning of the basic argument modes, in order to reflect the current state of discussions. The philosophy is for now: to stay as close as possible to the standard, clarifying where it may be ambiguous, and adding new modes as needed to cover other desired modes.