In most cases, the correctness of the algorithmic interpretation of a signature as a logic program depends on a restriction to queries of a certain form. Often, this is a restriction of some arguments to inputs which must be given as ground objects, that is, objects not containing any existential variables. In return, one often obtains outputs which will also be ground. In the logic programming terminology, the information about which arguments to a predicate should be considered input and output is called mode information.
Twelf supports a simple system of modes. It checks explicit mode declarations by the programmer against the signature and signals errors if the prescribed information flow is violated. Currently, queries are not checked against the mode declaration.
Mode checking is useful to uncover certain types of errors which elude the type-checker. It can also be used to generate more efficient code, although the compiler currently does not take advantage of mode information.
There are two forms of mode declarations: a short form which is adequate and appropriate most of the time, and a long form which is sometimes necessary to ascribe the right modes to implicit arguments
mdecl ::= smdecl % short mode declaration
| fmdecl % full mode declaration
decl ::= ...
| %mode mdecl.
There are two forms of mode declarations: a short and a full form. The short form is an abbreviation which is expanded into the full form when it is unambiguous.
mode ::= + % input
| * % unrestricted
| - % output
mid ::= mode id % named mode identifier, one token
smdecl ::= id % type family a
| smdecl mid % argument mode
Mode declarations for a predicate a must come before any clauses
defining a. Note that the mode followed with the identifier must
be one token, such as `+L' and not `+ L'. The short form is
most convenient in typical situations. For example, we can declare that
the append program (see section 5.4 Sample Trace) takes the first two
arguments as input and produces the the third as output.
append : list -> list -> list -> type. %mode append +L +K -M.
If we wanted to use append to split a list into two
sublists, we would instead declare
append : list -> list -> list -> type. %mode append -L -K +M.
where the clauses appNil and appCons remain
unchanged.
In the lambda-calculus type checker (see section 5.6 Sample Program), the type must be an unrestricted argument.
of : exp -> tp -> type. %mode of +E *T.
If we declare it as an input argument, %mode of +E +T,
we obtain an error pointing to the first occurrence of T2
in the clause tp_app reproduced below.
examples/nd/lam.elf:27.20-27.22 Error:
Occurrence of variable T2 in input (+) argument not necessarily ground
tp_app : of (app E1 E2) T1
<- of E1 (arrow T2 T1)
<- of E2 T2.
If we declare it as an output argument, %mode of +E -T,
we obtain an error pointing to the second occurrence of T1
in the clause tp_lam reproduced below.
examples/nd/lam.elf:25.8-25.10 Error:
Occurrence of variable T1 in output (-) argument not necessarily ground
tp_lam : of (lam E) (arrow T1 T2)
<- ({x:exp}
of x T1 -> of (E x) T2).
In general, for a mode declaration in short form the arguments are specified exactly as they would look in the program. This means one cannot specify the modes of implicit arguments which are filled in by term reconstruction. These modes are reconstructed as follows: each implicit argument which appears in the type of an input argument is considered input `+', those among the remaining which appear in an output argument are considered output `-', the rest are unrestricted. The mode declaration is echoed in full form, so the user can verify the correctness of the modes assigned to implicit arguments. If the inferred full mode declaration is incorrect, or if one wants to be explicit about modes, one should use full mode declarations (see section 7.2 Full Mode Declaration).
To specify modes for implicit arguments one must use the full form of
mode declaration. A mode can be one of `+',
`*', or `-' (see section 7.1 Short Mode Declaration).
fmdecl ::= mode {id : term} fmdecl
| mode {id} fmdecl
| term
The term following the mode prefix in a full mode declaration must
always have the form a x1 ... xn where
x1 through xn are variables declared in the mode prefix.
As an example, we give an alternative specification of the append
predicate.
append : list -> list -> list -> type.
%mode +{L:list} +{K:list} -{M:list} append L K M.
Mode checking for input, output, and unrestricted arguments examines each clause as it is encountered. The algorithm performs a kind of abstract interpretation of the clause, keeping track of a list of the existential variables for which it knows that they will be ground.
Arguments whose mode is unrestricted are ignored: they do no need to be checked, and they do not contribute any information about the instantiations of existential variables.
Go to the first, previous, next, last section, table of contents.