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.

LF tp : type = 
| arr : tptptp
| nat : 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.

LF term : type = 
| lam : tp → (termterm) → term
| app : termtermterm;

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.

LF hastype : termtptype = 
| h_lam : ({x : term} (hastype x T1 → hastype (M x) T2)) → hastype (lam T1 M) (arr T1 T2)
| h_app : hastype M1 (arr T2 T) → hastype M2 T2 → hastype (app M1 M2) T;


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

LF equal : tptptype = 
| e_ref : equal T T;


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 &Eta (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.

schema xtG = some [t : tp] block (x:term, _t:hastype x t);

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

rec unique : (g:xtG) [g ⊢ hastype M T[]] → [g ⊢ hastype M T'[]] → [ ⊢ equal T T']  =
fn d ⇒ fn f ⇒ case d of 
  | [g ⊢ h_app D1 D2] ⇒
    let  [g ⊢ h_app F1 F2] = f in 
    let  [ ⊢ e_ref] = unique [g ⊢ D1] [g ⊢ F1] in [ ⊢ e_ref]
  | [g ⊢ h_lam (λx. λu. D)] ⇒
    let  [g ⊢ h_lam (λx. λu. F)] = f in 
    let  [ ⊢ e_ref] =
    unique [g, b : block (x:term, u:hastype x _) ⊢ D[…, b.x, b.u]] [g, b ⊢ F[…, b.x, b.u]] in
    [ ⊢ e_ref]
  | [g ⊢ #q.2] ⇒ let  [g ⊢ #r.2] = f in [ ⊢ e_ref];

Consider each case individually.

To download the code: Type_Uniqueness.bel