5 Type, mode and determinism declaration headers
Many predicates can sensibly be called in different ways, e.g. with a specific argument as input or as output. The header of the documentation of a predicate consists of one or more templates, each representing a specific way of calling the predicate.
A template can contain information about types, argument instantiation patterns, determinism and more. The syntax is informally described below:
| <template> | ::= | <head>['//']’is' <determinism> |
| | | <head>['//'] | |
| <determinism> | ::= | ’det' |
| | | ’semidet' | |
| | | ’failure' | |
| | | ’nondet' | |
| | | ’multi' | |
| | | ’undefined' | |
| <head> | ::= | <functor>’('<argspec> ’,' <argspec>’)' |
| | | <functor> | |
| <argspec> | ::= | [<instantiation>]<argname>[':'<type>] |
| <instantiation> | ::= | ’++' | ’+' | ’-' | ’--' | ’?' | ’:' | ’@' | ’!' |
| <type> | ::= | <term> |
The determinism values originate from Mercury. Their meaning
is explained in the table below. Informally, det is used
for deterministic transformations (e.g. arithmetic), semidet
for tests, nondet and multi for generators.
The
failure indicator is rarely used. It mostly appears in
hooks or the recovery goal of catch/3.
| Determinism | Predicate behaviour |
det | Succeeds exactly once without a choice point |
semidet | Fails or Succeeds exactly once without a choice-point |
failure | Always fails |
nondet | No constraints on the number of times the predicate succeeds and whether or not it leaves choice-points on the last success. |
multi | As nondet, but succeeds
at least one time. |
undefined | Well founded semantics third value. See undefined/0. |
The meanings of the instantiation patterns for individual arguments are:
| ++ | Argument is ground at call-time, i.e., the argument does not contain a variable anywhere. |
| + | Argument is fully instantiated at call-time, to a term
that satisfies the type. This is not necessarily ground, e.g.,
the term
[_] is a list, although its only member is
unbound. |
| - | Argument is an output argument. It may be
unbound at call-time, or it may be bound to a term. In the latter case,
the predicate behaves as if the argument was unbound, and then unified
with that term after the goal succeeds. For example, the goal findall(X,
Goal, [T]) is good style and equivalent to findall(X, Goal,
Xs), Xs = [T]3The ISO
standard dictates that findall(X, Goal, 1) raises a type_error
exception, breaking this semantic relation. SWI-Prolog does not follow
the standard here. Determinism declarations assume that the
argument is a free variable at call-time. For the case where the
argument is bound or involved in constraints,
det effectively becomes semidet, and multi
effectively becomes nondet. |
| -- | Argument is unbound at call-time. Typically used by predicates that create‘something' and return a handle to the created object, such as open/3 which creates a stream. |
| ? | Argument is bound to a partial term of the indicated type at call-time. Note that a variable is a partial term for any type. |
| : | Argument is a meta-argument. Implies |
| @ | Argument will not be further instantiated than it is at call-time. Typically used for type tests. |
| ! | Argument contains a mutable structure that may be modified using setarg/3 or nb_setarg/3. |
Users should be aware that calling a predicate with arguments instantiated in a way other than specified by one of the templates may result in errors or unexpected behavior.
Developers should ensure that predicates are steadfast with respect to output arguments (marked - in the template). This means that instantiation of output arguments at call-time does not change the semantics of the goal (it may be used for optimization, though). If this steadfast behavior cannot be guaranteed, -- should be used instead.
In the current version, argument types are represented by an arbitrary term without formal semantics. In future versions we may adopt a formal type system that allows for runtime verification and static type analysis Hermenegildo, 2000, Mycroft & O'Keefe, 1984, Jeffery et al., 2000
Examples
%! length(+List:list, -Length:int) is det. %! length(?List:list, -Length:int) is nondet. %! length(?List:list, +Length:int) is det. % % True if List is a list of length Length. % % @compat iso