1. Type uniqueness
The simply-typed lambda-calculus as we have defined above has the property that every lambda-term has a unique type. This property is called type uniqueness and can be stated as follows:
Theorem: If Γ ⊢ type_of E T and Γ ⊢ type_of E T' then ⊢ equal T T'.
We explain here how to implement the type uniqueness proof for the simply-typed lambda-calculus. If you'd like to run this example using Beluga, please download unique.bel, which contains all the data-type definitions and the implementation of the proof as a recursive function.
Equality reasoning is not built-in in the logical framework LF, but we can easily specify it.
datatype equal : tp → tp → type =
| e_ref : equal T T
;
This statement of type uniqueness makes explicit the context Γ containing
typing assumptions about variables. Note that while terms E can depend on variables
declared in Γ, no variables can occur in the types T and T',
though this is not captured informally.
The theorem corresponds to a type of a recursive function in
Beluga. Before showing how to implement it, we describe more precisely
the shape of contexts Γ, using a context schema declaration:
schema tctx = some [t:tp] block x:exp. type_of x t;
The schema tctx
describes a context containing assumptions x:exp, each
associated with a typing assumption type_of x t for some type
t. In other words, concrete declarations in a context of schema tctx may instantiate the type t with some concrete type. Formally, we are using a dependent product type or Σ-type to tie x to type_of x t. We thus do not need to establish separately that for every variable there is a unique typing assumption: this is inherent in the definition of tctx.
We can now state the Beluga type corresponding to the statement above:
(g:tctx) [g. type_of (E ..) T] → [g. type_of (E ..) T')] → [ . eq T T']
We can read it as follows: for all contexts g of schema
tctx,
given derivations of
[g. type_of (E ..) T] and of
[g. type_of (E ..) T'] we can construct a derivation
of [ . eq T T'].
Quantification over the context variable g is
written using curly brackets in {g:tctx}. We treat the context variable g as an implicit argmument, i.e., we do not have to pass g explicitely but the correct context will be inferred. To mark that context variables are explicitely passeed, we annotate the context schema name with * and write {g:(tctx)*} instead.
The [ ] means the result is closed.
As we remarked, only the term
E can contain variables; the type
T
is closed. Although we did not state this dependency in the on-paper statement, Beluga
distinguishes closed objects from objects depending on assumptions. To
describe the dependency of terms on the context, we write
(E ..)
associating .. with the variable E. (Technically, ..
is an identity substitution mapping variables from
g to themselves.) In
contrast, T by itself denotes a closed
tp that cannot
depend on hypotheses in g.
Implementation of the proof for type uniqueness as a recursive function
In Beluga, inductive proofs are written as recursive programs. Case analysis and inversion in the on-paper proof correspond to case analysis and pattern matching in Beluga. Inversion is often represented using a let expression in Beluga, and is treated as a special instance of a case expression,
i.e., a case expression with only one branch.
rec unique:(g:tctx) [g. type_of (E ..) T] → [g. type_of (E ..) T']
→ [ . equal T T'] =
fn d ⇒ fn f ⇒ case d of
| [g. t_app (D1 ..) (D2 ..)] ⇒ % Application Case
let [g. t_app (F1 ..) (F2 ..)] = f in
let [ . e_ref] = unique [g. D1 ..] [g. F1 ..] in
[ . e_ref]
| [g. t_lam (\x.(\u. D .. x u)] ⇒ % Abstraction Case
let [g. t_lam (\x.(\u. F .. x u)] = f in
let [ . e_ref] = unique [g,b: block x:exp. type_of x _ . D .. b.1 b.2]
[g,b. F .. b.1 b.2] in
[ . e_ref]
| [g. #q.2] .. ⇒ % d : type_of #p.1 T % Assumption Case
let [g. #r.2] .. = f in % f : type_of #p.1 T'
[ . e_ref]
;
Application case: If d concludes with t_app, it matches
the pattern [g. t_app (D1 ..) (D2 ..)], and is
a contextual object of type
type_of (app (E1 ..) (E2 ..)) T in the
context g. We therefore know that
E .. = app (E1 ..) (E2 ..).
Pattern matching also serves to invert the second argument, the derivation f which
must have type [g. type_of (app (E1 ..) (E2 ..)) T')]. This is achieved
through a let-binding.
The appeal to the induction hypothesis using D1 and F1 in a paper proof
corresponds to the recursive call
unique [g. D1 ..] [g. F1 ..].
Note that we pass three arguments: the context g and contextual objects
[g. D1 ..] and
[g. F1 ..] describing the derivations of
[g. type_of (E1 ..) (arr T2 T)] and
[g. (type_of (E1 ..) (arr T2' T')]. The result is a contextual object of type
[ . eq (arr T2 T) (arr T2' T')]. The only rule that
could derive such an object is e_ref, and pattern matching
establishes that arr T2 T = arr T2' T'. Since we know
that T = T', there is a proof of [ . eq T T'].
Abstraction case:
If the first derivation d concludes with t_lam, it matches
the pattern [g. t_lam (\x.\u. D .. x u)], and is
a contextual object in the context g of type
[g. type_of (lam T1 (\x. E0 .. x)) (arr T1 T2)].
Thus, E .. = lam T1 (\x. E0 .. x)
and T = arr T1 T2.
Pattern matching—through a let-binding—serves to invert the second derivation
f, which
must have been by t_lam with a subderivation
F1 .. x u of type_of (E0 .. x) T2' that
can use x,
u:type_of x T1, and assumptions from g.
Hence, after pattern matching on d and f, we have
E = lam T1 (\x. E0 .. x) and
T = arr T1 T2 and
T' = arr T1 T2'.
The use of the induction hypothesis on D and F in a paper proof
corresponds to the recursive call to unique. To appeal to the
induction hypothesis, we need to extend the context by pairing up x and
its typing assumption: g,b:block x:exp.type_of x T1. In the
code, we wrote an underscore _ instead of
T1, which tells Beluga to reconstruct it.
To retrieve x we take the first projection b.1, and to retrieve
its typing assumption we write b.2.
Now we can appeal to the induction hypothesis using
D1 .. b.1 b.2 and F1 .. b.1 b.2 in the context
g,b:block x:exp. type_of x T1. We pass three arguments: the
context g and two contextual objects. From the i.h. we get a
contextual object, a closed derivation of
[ . eq (arr T1 T2) (arr T1 T2')]. The only rule that could
derive this is e_ref, and pattern matching establishes that T2
must equal T2', and hence arr T1 T2 = arr T1 T2',
i.e. T = T'. Hence, there is a proof of [ . eq T T'],
and we can finish the case with the reflexivity rule e_ref.
Assumption case Here, we must have used an assumption from the
context g to construct the derivation d. Parameter variables
#q allow a generic case that matches a declaration block
x:exp.type_of x S for any S in g. Since our pattern match
proceeds on typing derivations, we want the second component, written
#q.2. The pattern match on d also establishes that
E = #q.1
and S = T. Next, we pattern match on f, which has type
type_of (#q.1 ..) T' in the context g. Clearly, the only
possible way to derive f is by using an assumption from g. We call
this assumption #r, standing for a declaration block
y:exp.type_of y S', so #r.2 refers to the second component
type_of (#r.1 ..) S'. Pattern matching between #r.2 and
f
also establishes that both types are equal and that S' = T' and
#r.1 = #q.1. Finally, we observe that #r.1 = #q.1 only if
#r is equal to #q. Consequently, both parameters have equal
types, and S = S' = T = T'. (In general, unification in the presence
of Σ-types does not yield a unique unifier, but in Beluga only
variables from the context and parameter variables can have Σ-types,
yielding a unique solution.)
