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