Type Uniqueness for the Simply-typed Lambda-calculus

We prove that every lambda term has a unique type. Type uniqueness is also a benchmark in ORBI, Open challenge problem Repository for systems reasoning with Binders. For a detailed description of the proof and a discussion regarding other systems see (Felty et al, 2014).

Syntax: Types and Lambda-terms

We first represent the simply-typed lambda-calculus in the logical framework LF: the LF type tp describes the types of our simply typed lambda-calculus, and the LF type tm characterizes the terms of the lambda-calculus.

The LF type tp has two constructors, nat and arr, corresponding to the types nat and arr T S, respectively. Since arr is a constructor which takes in two arguments, its type is tp -> tp -> tp.

The LF type tm also has two constructors. The constructor app takes as input two objects of type tm and allows us to construct an object of type tm. The constructor for lambda-terms also takes two arguments as input; it first takes an object of type tp for the type annotation and the body of the abstraction is second. We use higher-order abstract syntax to represent the object-level binding of the variable x in the body M. Accordingly, the body of the abstraction is represented by the type (tm -> tm). For example, lam x:(arr nat nat) . lam y:nat . app x y is represented by lam (arr nat nat) \x.lam nat \y.app x y. This encoding has several well-known advantages: First, the encoding naturally supports alpha-renaming of bound variables, which is inherited from the logical framework. Second, the encoding elegantly supports substitution for bound variables which reduces to beta-reduction in the logical framework LF.

Typing Rules

We describe typing judgment using the type family has_type which relates terms tm and types tp. The inference rules for lambda-abstraction and application are encoded as h_lam and h_app, respectively.

Equality

Since Beluga does not support equality types, we implement equality by reflexivity using the type family equal.

Schema

The schema txG describes a context containing assumptions x:tm, each associated with a typing assumption hastype x t for some type t. Formally, we are using a dependent product Η (used only in contexts) to tie x to hastype 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 txG. The schema classifies well-formed contexts and checking whether a context satisfies a schema will be part of type checking. As a consequence, type checking will ensure that we are manipulating only well-formed contexts, that later declarations overshadow previous declarations, and that all declarations are of the specified form.

Typing uniqueness proof

Our final proof of type uniqueness rec unique proceeds by case analysis on the first derivation. Accordingly, the recursive function pattern-matches on the first derivation d which has type [g |- hastype M T].

Consider each case individually.

• Application case. If the first derivation d concludes with h_app, it matches the pattern [g |- h_app D1 D2], and forms a contextual object in the context g of type [g |- hastype M T'[]]. D1 corresponds to the first premise of the typing rule for applications with contextual type [g |- hastype M1 (arr T'[] T[])]. Using a let-binding, we invert the second argument, the derivation f which must have type [g |- hastype (app M1 M2) T[]]. F1 corresponds to the first premise of the typing rule for applications and has the contextual type [g |- hastype M1 (arr S'[] S[])]. The appeal to the induction hypothesis using D1 and F1 in the on-paper proof corresponds to the recursive call unique [g |- D1] [g |- F1]. Note that while unique’s type says it takes a context variable (g:xtG), we do not pass it explicitly; Beluga infers it from the context in the first argument passed. The result of the recursive call is a contextual object of type [ |- eq (arr T1 T2) (arr S1 S2)]. The only rule that could derive such an object is e_ref, and pattern matching establishes that arr T T' = arr S S’ and hence T = S and T' = S’.

• Lambda case. If the first derivation d concludes with h_lam, it matches the pattern [g |- h_lam (\x.\u. D u)], and is a contextual object in the context g of type hastype (lam T[] M) (arr T[] T'[]). Pattern matching—through a let-binding—serves to invert the second derivation f, which must have been by h_lam with a subderivation F to reach hastype M S[] that can use x, u:hastype x T[], and assumptions from g.
  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 the typing assumption hastype x T[]. This is accomplished by creating the declaration b: block x:term, u:hastype x T[]. In the code, we wrote an underscore _ instead of T[], which tells Beluga to reconstruct it since we cannot write T[] there without binding it by explicitly giving the type of D. To retrieve x we take the first projection b.x, and to retrieve x’s typing assumption we take the second projection b.u.
  Now we can appeal to the induction hypothesis using D1[.., b.x, b.u] and F1[.., b.x, b.u] in the context g, b: block x:term, u:hastype x S[]. From the i.h. we get a contextual object, a closed derivation of [|- eq (arr T T') (arr S S’)]. The only rule that could derive this is ref, and pattern matching establishes that S must equal S’, since we must have arr T S = arr T1 S’. Therefore, there is a proof of [ |- equal S S’], and we can finish with the reflexivity rule e_ref.

• Variable case. Since our context consists of blocks containing variables of type tm and assumptions hastype x T[], we pattern match on [g |- #p.2], i.e., we project out the second argument of the block. By the given assumptions, we know that [g |- #p.2] has type [g |- hastype #p.1 T[]], because #p has type [g |- block x:tm , u:hastype x T[]]. We also know that the second input, called f, to the function unique has type [g |- hastype #p.1 T'[]]. By inversion on f, we know that the only possible object that can inhabit this type is [g |- #p.2] and therefore T' must be identical to T. Moreover, #r denotes the same block as #p.