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:

- yes, and here is the most general reconstruction;
- no, and here is the problem; or
- 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.

- Implicit Quantifiers: Free variables in declarations
- Implicit Arguments: Omitted arguments to constants
- Strict Occurrences: A sufficient condition for principal types
- Strict Definitions: Reconstruction on definitions
- Type Ascription: Disambiguating terms
- Error Messages: When things go wrong
- Tracing Reconstruction: Seeing what happens during reconstruction

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.

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.

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.

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.

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.

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:locationError: 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

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.
`line1`.`column1`-`line2`.`column2`

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.