Modes and their meaning

[Note: This is still a rough draft for discussion (including the mode definitions).]

[Note: We should extend the PIP to cover determinism and non-failure also, but 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]

What do we mean by modes?

In Prolog “modes” refer to the different ways in which a predicate can be called. For example, given the standard definition of length/2, one of the intended uses is normally to provide a list in the first argument and obtain an integer representing its length in the second argument. We refer to this as a “mode”. Modes are useful for many purposes. A traditional one is program documentation.

To specify modes usually some special terms are used that define the expected instantiation state of the arguments of the predicate. This is done using atoms (such as +, -, ?, @, etc.) or more complex terms (such as +list, -list, ?list, @list, etc. etc.).

Predicate modes can be expressed using these terms:

In classical mode declarations such as:

:- mode length(+,-). % Computes the length of a list.
or in comments, such as:

% length(+list,-int): Computes the length of a list.
or in machine readable comments, such as:

%! length(+list,-int): Computes the length of a list.
or, equivalently, in assertions, such as:

:- pred length(+list,-int) # “Computes the length of a list.”.

Etc.

Focus for now

Our focus here (at least initially) is on the special terms used to describe instantiation states (the +, -, +list, etc.) rather than on the declarations in which they appear.

Is there a problem with modes?

The meaning of such terms (and modes in general) has not been traditionally a matter of debate among Prolog developers or programmers, probably because the usual different understandings of modes have been sufficient for the traditional purpose of documentation.

However, a more detailed look can reveal subtle issues that need agreement on, particularly when modes are used for other purposes such as program verification or to guide program optimizations.

For 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?

<Here we could include a discussion of the modes used in ISO or others.>

The need for a precise definition is specially relevant in systems like Ciao Prolog, where modes are checked both at compile-time and at run-time (the latter when static checking cannot discharge the proof obligations), but it is perceived to be useful in general also to, e.g., make the meaning of documentation more precise.

A first purpose of this PIP is then to define precisely the meaning of these terms (+, -, +list, …) used to define modes.

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