Modes and their precise meaning

[Note: This is still a rough draft for discussion (and specially the proposed definitions for each mode).]

[Note: We should eventually extend the PIP to cover determinism and non-failure also, but we are limiting to modes for now to focus discussion. That could also be a separate PIP. Another issue that we leave open for now is the names of the types (list, int, etc.) used as arguments of modes.]

[General note: If you have comments please post them at the Prolog Community Discourse 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.

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 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 - 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.

Ciao

Ciao Prolog uses modes for formal documentation and also for verification. As mentioned before in Ciao the meaning of modes can be defined and they act as ‘property macros’ to Ciao’s assertions. Also, the system library has traditionally included a number of different ‘modes packages’ so that that 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. This solves in part the problem but it is clear that it would be much better to have at least one set of modes that the different systems agree on. We will return below to the method used by Ciao to define modes.

Eclipse

From the Eclipse manual:

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.

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.

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, 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 is a meta-argument, for example a term that can be called as goal. The predicate is thus a meta-predicate. This flag implies +.

@ : 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 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 as follows:

  1. Adopt, for the purposes of the PIP, a compact notation for describing the meaning of modes.

  2. Agree on the meaning of each of the argument modes in common use, and express it precisely.

Other objectives which may be addressed later:

  1. Describe the meaning combination o

  2. Ideally adopting a common syntax for expressing predicate modes in comments, mode declarations, etc.

A notation for modes

For conciseness and precision, we propose to use in this PIP the Ciao notation for argument 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.

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 “property macro.”

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 need 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.

There are some properties traditionally associated 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>".         ] .

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 - here 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).

Proposal (WIP!)

 THE PART BELOW THIS LINE IS NOT UP TO DATE

‘Traditional’ modes

In the previous draft we were referring to ‘unary’ modes, etc. This was referring to the fact that they correspond to unary properties, such as nonvar(Arg1), var(Arg2), etc. when translated to Prolog code, in ‘assertions’, etc. This was inspired by the translation of modes into assertions in Ciao Prolog. For example, modes such as:

:- mode length(+,-).

or

:- pred length(+,-) # "Computes the length of a list.".

are translated to the following assertion:

:- pred length(X,Y) : nonvar(X) => nonvar(Y) # "Computes the length of a list.".

+

The argument should be bound (nonvar/1) when the predicate is called.

For example:

:- pred + > +.

expresses that both arguments of >/2 should be bound when the predicate is called.

+<type>

The argument should be instantiated when the predicate is called to a term that has the indicated type or property. For example +list expresses that the argument should be bound to a list when the predicate is called. Note that this does not mean that the list will be ground, but rather that it will be a complete list but whose elements can be any term, including variables.

-

The argument is an output argument. It may be bound or not at call time. It will be bound (nonvar/1) if the predicate succeeds.

Discussion point: In the ISO documentation, in classic mode declarations, and in some classic texts, - also implies that the argument is a variable at call time.

-<type>

The argument is an output argument. It may be bound or not at call time. It will be instantiated to a term that has the indicated type or property if the predicate succeeds. For example,

foo(-list,-int)

expresses that length/2 can be called in any way, but on output the second argument will be instantiated to a number and the first one will be instantiated to a list. Note that this does not mean that the list will be ground, but rather that it will be a complete list but whose elements can be any term, including variables.

?

No information is given on this argument.

?<type> : On call and success the argument can be a variable or, if it is instantiated, it is to a term that is compatible with the indicated type or property.

@

The argument will not be further instantiated, i.e., will not be more instantiated than when the predicate is called.

_COMMENT: Recall that test builtins (integer/1) are @_

@<type>

The argument will not be further instantiated, i.e., will not be more instantiated than when the predicate is called, and the term is compatible with the indicated type or property.

QUESTION: @list does it refer to not further instantiating the list part or also the argument?

Other modes

Note: some of these are probably not needed and consensus is in any case not needed on all of them

in ++

The argument is ground at call time.

in<type> ++<type>

The argument is ground at call time and is instantiated with the indicated type or property.

out

The argument is a variable when the predicate is called and will be ground if the predicate succeeds.

Discussion point: do we want the var on calls? See go below.

go

(‘Ground output’) The argument is ground by the predicate, if it succeeds.

Discussion point: do we need both out and go?

out<type>

The argument should be a free variable (i.e., unbound) when the predicate is called and will be bound to a ground term that is compatible with the indicated type or property, if the predicate succeeds.

Discussion point: do we want the var on calls? See go<type> below.

go<type>

The argument is bound by the predicate to a ground term that is compatible with the indicated type or property, if the predicate succeeds.

Discussion point: do we need both out<type> and go<type>?

--

The argument should be a free variable (i.e., unbound) when the predicate is called.

Discussion point: nonvar on success for regularity with --<type> below? Consensus seems to be yes?

--<type>

The argument should be a free variable (i.e., unbound) when the predicate is called and will be bound to a term that has the indicated type or property if the predicate succeeds.

!

The argument contains a mutable structure that could be modified.

:

The argument is meta. Must be bound as with +.


The Prolog Implementers Forum is a part of the "All Things Prolog" online Prolog community, an initiative of the Association for Logic Programming stemming from the Year of Prolog activities.