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


4 Term Reconstruction

Representations of deductions in LF typically contain a lot of redundant information. In order to make LF practical, Twelf gives the user the opportunity to omit redundant information in declarations and reconstructs it from context. Unlike for functional languages, this requires recovering objects as well as types, so we refer to this phase as term reconstruction.

There are criteria which guarantee that the term reconstruction problem is decidable, but unfortunately these criteria are either very complicated or still force much redundant information to be supplied. Therefore, the Twelf implementation employs a reconstruction algorithm which always terminates and gives one of three answers:

  1. yes, and here is the most general reconstruction;
  2. no, and here is the problem; or
  3. maybe.

The last characterizes the situations where there is insufficient information to guarantee a most general solution to the term reconstruction problem. Because of the decidable nature of type-checking in LF, the user can always annotate the term further until it falls into one of the definitive categories.

4.1 Implicit Quantifiers

The model of term reconstruction employed by Twelf is straightforward, although it employs a relatively complex algorithm. The basic principle is a duality between quantifiers omitted in a constant declaration and implicit arguments where the constant is used. Recall some definitions in the signature defining natural deductions (see section 3.6 Sample Signature).

o : type.
and : o -> o -> o.   %infix right 10 and
nd : o -> type.
andi : nd A -> nd B -> nd (A and B).

The last declaration contains A and B as free variables. Type reconstruction infers most general types for the free variables in a constant declaration and adds implicit quantifiers. In the example above, A and B must both be of type o. The internal form of the constant thus has one of the following two forms.

andi : {A:o} {B:o} nd A -> nd B -> nd (A and B).
andi : {B:o} {A:o} nd A -> nd B -> nd (A and B).

These forms are printed during type reconstruction, so the user can examine if the result of reconstruction matches his expectations.

4.2 Implicit Arguments

The quantifiers on A and B in the declaration

andi : nd A -> nd B -> nd (A and B).

were implicit. The corresponding arguments to andi are also implicit. In fact, since the order of the reconstructed quantifiers is arbitrary, we cannot know in which order to supply the arguments, so they must always be omitted. Thus a constant with n implicit quantifiers is supplied with n implicit arguments wherever it is seen. These implicit arguments are existential variables whose value may be determined from context by unification.

For example, using also

true : o.
truei: nd (true).

we have

(andi truei truei) : nd (true and true).

During parsing, the expression (andi truei truei) is interpreted as

(andi _ _ truei truei)

where the two underscores stand for the implicit A and B arguments to andi. They are replaced by existential variables whose value will be determined during type reconstruction. We call them A1 and A2 and reason as follows.

|- andi : {A:o} {B:o} nd A -> nd B -> nd (A and B)
|- andi A1 : {B:o} nd A1 -> nd B -> nd (A1 and B)
|- andi A1 A2 : nd A1 -> nd A2 -> nd (A1 and A2)

At this point, we need a to infer the type of the application (andi A1 A2) truei. This equates the actual type of the argument with the expected type of the argument.

|- andi A1 A2 : nd A1 -> nd A2 -> nd (A1 and A2)
|- truei : nd true
------------------------------------------------
|- andi A1 A2 truei : nd A2 -> nd (A1 and A2)
   where nd true = nd A1

The equation can be solved by instantiating A1 to true and we continue:

|- andi true A2 truei : nd A2 -> nd (true and A2)
|- truei : nd true
------------------------------------------------
|- andi true A2 truei truei : nd (true and A2)
   where nd true = nd A2
|- andi true true truei truei : nd (true and true)

The last line is the expected result. In this way, term reconstruction can always be reduced to solving equations such that every solution to the set of equations leads to a valid typing and vice versa.

4.3 Strict Occurrences

Both for type reconstruction and the operational semantics, Twelf must solve equations between objects and types. Unfortunately, it is undecidable if a set of equations in the LF type theory has a solution. Worse yet, even if it has solutions, it may not have a most general solution. Therefore, Twelf postpones difficult equations as constraints and solves only those within the pattern fragment (see Miller 1991, Journal of Logic and Computation and Pfenning 1991, Logical Frameworks). In this fragment, principal solutions always exist and can be computed efficiently. If constraints remain after term reconstruction, the constant declaration is rejected as ambiguous which indicates that the user must supply more type information. We illustrate this phenomenon and a typical solution in our natural deduction example.

A central concept useful for understanding the finer details of type reconstruction is the notion of a strict occurrence of a free variable. We call a position in a term rigid if it is not in the argument of a free variable. We then call an occurrence of a free variable strict if the occurrence is in a rigid position and all its arguments (possibly none) are distinct bound variables.

If all free variable occurrences in all declarations in a signature are strict, then term reconstruction will always either fail or succeed with a principal solution, provided no further terms are omitted (that is, replaced by an underscore).

If a free variable in a declaration of a constant c has no strict occurrence at all, then its type can almost never be inferred and most uses of c will lead to a constraint.

If a free variable has strict and non-strict occurrences then in most cases term reconstruction will provide a definitive answer, but there is no guarantee. Mostly this is because most general answers simply do not exist, but sometimes because the algorithm generates, but cannot solve constraints with unique solutions.

We use some advanced examples from the natural deduction signature to illustrate these concepts and ideas. In the declarations

foralli : ({x:i} nd (A x)) -> nd (forall A).
foralle : nd (forall A) -> {T:i} nd (A T).

all free variables have a strict occurrence. However, if we had decided to leave T as an implicit argument,

foralle : nd (forall A) -> nd (A T).

then T has no strict occurrence. While this declaration is accepted as unambiguous (with A:i -> o and T:i), any future use of foralle most likely leads to constraints on T which cannot be solved.

4.4 Strict Definitions

Definitions are currently restricted so that each argument to the defined constant, may it be implicit or explicit, must have at least one strict occurrence in the right-hand side. For example, the definition of not in the signature for natural deduction (see section 3.6 Sample Signature)

not : o -> o = [A:o] A imp false.

is strict since the only argument A has a strict occurrence in A imp false. On the other hand, the definition

noti : ({p:o} nd A -> nd p) -> nd (not A)
     = [D] impi ([u:nd A] D false u).

which gives a possible derived introduction rule for negation is not strict: the argument D has only one occurrence, and this occurrence is not strict since the argument false is not a variable bound in the body, but a constant.

However, the definitions

noti : (nd A -> nd false) -> nd (not A)
     = [D:nd A -> nd false] impi D.
note : nd (not A) -> nd A -> nd false
     = [D:nd (not A)] [E:nd A] impe D E.

are both strict since arguments D and E both have strict occurrences. Type-checking these definitions requires that the definition of not A is expanded to A imp false.

Note that free variables in the type and the right-hand side of a definition are shared. In the above example, A occurs both in the types and the right hand side and it should be thought of as the same A. With the implicit quantifiers and abstractions restored, the definitions above have the following form.

noti : {A:o} (nd A -> nd false) -> nd (not A)
   = [A:o] [D:nd A -> nd false] impi D.
note : {A:o} nd (not A) -> nd A -> nd false
   = [A:o] [D:nd (not A)] [E:nd A] impe D E.

4.5 Type Ascription

In some circumstances it is useful to directly ascribe a type in order to disambiguate declarations. For example, the term ori1 truei has principal type nd (true or B) for a free variable B. If we want to constrain this to a derivation of nd (true or false) we can write ori1 truei : nd (true or false).

Explicit type ascription sometimes helps when the source of a type error is particularly hard to discern: we can ascribe an expected type to a subterm, thus verifying our intuition about constituent terms in a declaration.

4.6 Error Messages

When term reconstruction fails, Twelf issues an error message with the location of the declaration in which the problem occurred and the disagreement encountered. A typical message is

examples/nd/nd.elf:37.35-37.41 Error: Type mismatch
Expected: o
Found:    (i -> o) -> o
Expression clash

which points to an error in the file `examples/nd/nd.elf', line 37, characters 35 through 41 where an argument to a function was expected to have type o, but was found to have type (i -> o) -> o.

If constraints remain, the error location is the whole declaration with the message

filename:location Error: Typing ambiguous -- unresolved constraints

The filename and location information can be used by Emacs (see section 13 Emacs Interface) to jump to the specified location in the given file for editing of the incorrect declaration for the constant c. The location has the form line1.column1-line2.column2 and represent Twelf's best guess as to the source of the error. Due to the propagation of non-trivial constraints the source of a type reconstruction failure can sometimes not be pinpointed very precisely.

4.7 Tracing Reconstruction

Sometimes it is quite difficult to determine the real source of a type error. On such occasion there are three standard techniques that sometimes help. The first is to enable the printing of implicit arguments with Twelf.Print.implicit := true and try again. The second is to insert explicit type annotations to limit the flexibility of reconstruction. The third is to trace type reconstruction.

Tracing of term reconstruction is enabled with

Twelf.Recon.trace := true;

It then prints, during reconstruction, the typing and kinding judgments it infers in the form |- M : A or |- A : K.

There are two modes for tracing reconstruction that can be set with

Twelf.Recon.traceMode := Twelf.Recon.Omniscient;
Twelf.Recon.traceMode := Twelf.Recon.Progressive;

where Twelf.Recon.Omnisicient is the default. In omnisicent mode, it first solves all typing constraints, and then prints the typing judgments. In progressive mode, it prints the typing judgments as they are encountered. Both have their uses, depending on the form of the problem with reconstruction.


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