Dependent de Bruijn Indices

In this example, we represent program syntax terms in a type family parameterized by a list of types, representing the typing context, or information on which free variables are in scope and what their types are.

Remark: this example is based on an example in the book Certified Programming with Dependent Types by Adam Chlipala.

Programmers who move to statically typed functional languages from scripting languages often complain about the requirement that every element of a list have the same type. With fancy type systems, we can partially lift this requirement. We can index a list type with a “type-level” list that explains what type each element of the list should have. This has been done in a variety of ways in Haskell using type classes, and we can do it much more cleanly and directly in Lean.

We parameterize our heterogeneous lists by at type α and an α-indexed type β.

inductive HList {α : Type v} (β : α → Type u) : List α → Type (max u v)
  | nil  : HList β []
  | cons : β i → HList β is → HList β (i::is)

We overload the List.cons notation :: so we can also use it to create heterogeneous lists.

infix:67 " :: " => HList.cons

We similarly overload the List notation [] for the empty heterogeneous list.

notation "[" "]" => HList.nil

Variables are represented in a way isomorphic to the natural numbers, where number 0 represents the first element in the context, number 1 the second element, and so on. Actually, instead of numbers, we use the Member inductive family.

The value of type Member a as can be viewed as a certificate that a is an element of the list as. The constructor Member.head says that a is in the list if the list begins with it. The constructor Member.tail says that if a is in the list bs, it is also in the list b::bs.

inductive Member : α → List α → Type
  | head : Member a (a::as)
  | tail : Member a bs → Member a (b::bs)

Given a heterogeneous list HList β is and value of type Member i is, HList.get retrieves an element of type β i from the list. The pattern .head and .tail h are sugar for Member.head and Member.tail h respectively. Lean can infer the namespace using the expected type.

def HList.get : HList β is → Member i is → β i
  | a::as, .head => a
  | unused variable `a`
note: this linter can be disabled with `set_option linter.unusedVariables false`a::as, .tail h => as.get h

Here is the definition of the simple type system for our programming language, a simply typed lambda calculus with natural numbers as the base type.

inductive Ty where
  | nat
  | fn : Ty → Ty → Ty

We can write a function to translate Ty values to a Lean type — remember that types are first class, so can be calculated just like any other value. We mark Ty.denote as [reducible] to make sure the typeclass resolution procedure can unfold/reduce it. For example, suppose Lean is trying to synthesize a value for the instance Add (Ty.denote Ty.nat). Since Ty.denote is marked as [reducible], the typeclass resolution procedure can reduce Ty.denote Ty.nat to Nat, and use the builtin instance for Add Nat as the solution.

Recall that the term a.denote is sugar for denote a where denote is the function being defined. We call it the "dot notation".

@[reducible] def Ty.denote : Ty → Type
  | nat    => Nat
  | fn a b => a.denote → b.denote

Here is the definition of the Term type, including variables, constants, addition, function application and abstraction, and let binding of local variables. Since let is a keyword in Lean, we use the "escaped identifier" let. You can input the unicode (French double quotes) using \f<< (for «) and \f>> (for »). The term Term ctx .nat is sugar for Term ctx Ty.nat, Lean infers the namespace using the expected type.

inductive Term : List Ty → Ty → Type
  | var   : Member ty ctx → Term ctx ty
  | const : Nat → Term ctx .nat
  | plus  : Term ctx .nat → Term ctx .nat → Term ctx .nat
  | app   : Term ctx (.fn dom ran) → Term ctx dom → Term ctx ran
  | lam   : Term (dom :: ctx) ran → Term ctx (.fn dom ran)
  | let : Term ctx ty₁ → Term (ty₁ :: ctx) ty₂ → Term ctx ty₂

Here are two example terms encoding, the first addition packaged as a two-argument curried function, and the second of a sample application of addition to constants.

The command open Ty Term Member opens the namespaces Ty, Term, and Member. Thus, you can write lam instead of Term.lam.

open Ty Term Member

def add : Term [] (fn nat (fn nat nat)) :=
  lam (lam (plus (var (tail head)) (var head)))

def three_the_hard_way : Term [] nat :=
  app (app add (const 1)) (const 2)

Since dependent typing ensures that any term is well-formed in its context and has a particular type, it is easy to translate syntactic terms into Lean values.

The attribute [simp] instructs Lean to always try to unfold Term.denote applications when one applies the simp tactic. We also say this is a hint for the Lean term simplifier.

@[simp] def Term.denote : Term ctx ty → HList Ty.denote ctx → ty.denote
  | var h,     env => env.get h
  | const n,   _   => n
  | plus a b,  env => a.denote env + b.denote env
  | app f a,   env => f.denote env (a.denote env)
  | lam b,     env => fun x => b.denote (x :: env)
  | let a b, env => b.denote (a.denote env :: env)

You can show that the denotation of three_the_hard_way is indeed 3 using reflexivity.

example : three_the_hard_way.denote [] = 3 :=
  rfl

We now define the constant folding optimization that traverses a term if replaces subterms such as plus (const m) (const n) with const (n+m).

@[simp] def Term.constFold : Term ctx ty → Term ctx ty
  | const n   => const n
  | var h     => var h
  | app f a   => app f.constFold a.constFold
  | lam b     => lam b.constFold
  | let a b => let a.constFold b.constFold
  | plus a b  =>
    match a.constFold, b.constFold with
    | const n, const m => const (n+m)
    | a',      b'      => plus a' b'

The correctness of the Term.constFold is proved using induction, case-analysis, and the term simplifier. We prove all cases but the one for plus using simp [*]. This tactic instructs the term simplifier to use hypotheses such as a = b as rewriting/simplifications rules. We use the split to break the nested match expression in the plus case into two cases. The local variables iha and ihb are the induction hypotheses for a and b. The modifier ← in a term simplifier argument instructs the term simplifier to use the equation as a rewriting rule in the "reverse direction". That is, given h : a = b, ← h instructs the term simplifier to rewrite b subterms to a.

theorem Term.constFold_sound (e : Term ctx ty) : e.constFold.denote env = e.denote env := byctx:List Tyty:Tyenv:HList Ty.denote ctxe:Term ctx ty⊢ e.constFold.denote env = e.denote env
  induction e with simp [*]All goals completed! 🐙
  | plus a b iha ihb =>
    splitplus.h_1ctx:List Tyty:Tyctx✝:List Tya:Term ctx✝ natb:Term ctx✝ natiha:∀ {env : HList Ty.denote ctx✝}, a.constFold.denote env = a.denote envihb:∀ {env : HList Ty.denote ctx✝}, b.constFold.denote env = b.denote envenv:HList Ty.denote ctx✝x✝¹:Term ctx✝ natx✝:Term ctx✝ natn✝:Natm✝:Natheq✝¹:a.constFold = const n✝heq✝:b.constFold = const m✝⊢ (const (n✝ + m✝)).denote env = a.denote env + b.denote envplus.h_2ctx:List Tyty:Tyctx✝:List Tya:Term ctx✝ natb:Term ctx✝ natiha:∀ {env : HList Ty.denote ctx✝}, a.constFold.denote env = a.denote envihb:∀ {env : HList Ty.denote ctx✝}, b.constFold.denote env = b.denote envenv:HList Ty.denote ctx✝x✝²:Term ctx✝ natx✝¹:Term ctx✝ natx✝:∀ (n m : Nat), a.constFold = const n → b.constFold = const m → False⊢ (a.constFold.plus b.constFold).denote env = a.denote env + b.denote env
    next he₁ he₂ =>ctx:List Tyty:Tyctx✝:List Tya:Term ctx✝ natb:Term ctx✝ natiha:∀ {env : HList Ty.denote ctx✝}, a.constFold.denote env = a.denote envihb:∀ {env : HList Ty.denote ctx✝}, b.constFold.denote env = b.denote envenv:HList Ty.denote ctx✝x✝¹:Term ctx✝ natx✝:Term ctx✝ natn✝:Natm✝:Nathe₁:a.constFold = const n✝he₂:b.constFold = const m✝⊢ (const (n✝ + m✝)).denote env = a.denote env + b.denote env simp [← iha, ← ihb, he₁, he₂]All goals completed! 🐙
    next =>ctx:List Tyty:Tyctx✝:List Tya:Term ctx✝ natb:Term ctx✝ natiha:∀ {env : HList Ty.denote ctx✝}, a.constFold.denote env = a.denote envihb:∀ {env : HList Ty.denote ctx✝}, b.constFold.denote env = b.denote envenv:HList Ty.denote ctx✝x✝²:Term ctx✝ natx✝¹:Term ctx✝ natx✝:∀ (n m : Nat), a.constFold = const n → b.constFold = const m → False⊢ (a.constFold.plus b.constFold).denote env = a.denote env + b.denote env simp [iha, ihb]All goals completed! 🐙