Go to the first, previous, next, last section, table of contents.

7 Modes

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.

7.1 Short Mode Declaration

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

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.

7.3 Mode Checking

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.

  1. We assume each existential variable with a strict occurrence (see section 4.3 Strict Occurrences) in an input argument to the clause head to be ground.
  2. We traverse the subgoals in evaluation order (see section 5.5 Operational Semantics). For each subgoal we first verify that all input arguments will be ground, using the information about the existential variables collected so far. If this check succeeds we add all variables which have a strict occurrence in an output argument of the subgoal to the list of variables with known ground instantiations.
  3. After the last subgoal has been examined, we verify that the output arguments in the clause head are now also 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.