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)
HList
{
α: Type v
α
:
Type v: Type (v + 1)
Type v
} (
β: α → Type u
β
:
α: Type v
α
Type u: Type (u + 1)
Type u
) :
List: Type v → Type v
List
α: Type v
α
Type (max u v): Type ((max u v) + 1)
Type (max u v)
|
nil: {α : Type v} → {β : α → Type u} → HList β []
nil
:
HList: {α : Type v} → (α → Type u) → List α → Type (max u v)
HList
β: α → Type u
β
[]: List α
[]
|
cons: {α : Type v} → {β : α → Type u} → {i : α} → {is : List α} → β i → HList β is → HList β (i :: is)
cons
:
β: α → Type u
β
i: α
i
HList: {α : Type v} → (α → Type u) → List α → Type (max u v)
HList
β: α → Type u
β
is: List α
is
HList: {α : Type v} → (α → Type u) → List α → Type (max u v)
HList
β: α → Type u
β
(
i: α
i
::
is: List α
is
)

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

infix:67 " :: " => 
HList.cons: {α : Type v} → {β : α → Type u} → {i : α} → {is : List α} → β i → HList β is → HList β (i :: is)
HList.cons

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

notation "[" "]" => 
HList.nil: {α : Type v} → {β : α → Type u} → HList β []
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: {α : Type} → α → List α → Type
Member
:
α: Type
α
List: Type → Type
List
α: Type
α
Type: Type 1
Type
|
head: {α : Type} → {a : α} → {as : List α} → Member a (a :: as)
head
:
Member: {α : Type} → α → List α → Type
Member
a: ?m.15459
a
(
a: ?m.15459
a
::
as: List ?m.15459
as
) |
tail: {α : Type} → {a : α} → {bs : List α} → {b : α} → Member a bs → Member a (b :: bs)
tail
:
Member: {α : Type} → α → List α → Type
Member
a: ?m.15600
a
bs: List ?m.15600
bs
Member: {α : Type} → α → List α → Type
Member
a: ?m.15600
a
(
b: ?m.15600
b
::
bs: List ?m.15600
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: {α : Type} → {β : α → Type u_1} → {is : List α} → {i : α} → HList β is → Member i is → β i
HList.get
:
HList: {α : Type} → (α → Type u_1) → List α → Type u_1
HList
β: ?m.16170 → Type u_1
β
is: List ?m.16170
is
Member: {α : Type} → α → List α → Type
Member
i: ?m.16170
i
is: List ?m.16170
is
β: ?m.16170 → Type u_1
β
i: ?m.16170
i
|
a: β i
a
::
as: HList β is✝
as
,
.head: {α : Type} → {a : α} → {as : List α} → Member a (a :: as)
.head
=>
a: β i
a
|
Warning: unused variable `a` [linter.unusedVariables]
::
as: HList β is✝
as
,
.tail: {α : Type} → {a : α} → {bs : List α} → {b : α} → Member a bs → Member a (b :: bs)
.tail
h: Member i is✝
h
=>
as: HList β is✝
as
.
get: {α : Type} → {β : α → Type u_1} → {is : List α} → {i : α} → HList β is → Member i is → β i
get
h: Member i is✝
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: Type
Ty
where |
nat: Ty
nat
|
fn: Ty → Ty → Ty
fn
:
Ty: Type
Ty
Ty: Type
Ty
Ty: Type
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
Ty.denote
:
Ty: Type
Ty
Type: Type 1
Type
|
nat: Ty
nat
=>
Nat: Type
Nat
|
fn: Ty → Ty → Ty
fn
a: Ty
a
b: Ty
b
=>
a: Ty
a
.
denote: Ty → Type
denote
b: Ty
b
.
denote: Ty → Type
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
Term
:
List: Type → Type
List
Ty: Type
Ty
Ty: Type
Ty
Type: Type 1
Type
|
var: {ty : Ty} → {ctx : List Ty} → Member ty ctx → Term ctx ty
var
:
Member: {α : Type} → α → List α → Type
Member
ty: Ty
ty
ctx: List Ty
ctx
Term: List Ty → Ty → Type
Term
ctx: List Ty
ctx
ty: Ty
ty
|
const: {ctx : List Ty} → Nat → Term ctx Ty.nat
const
:
Nat: Type
Nat
Term: List Ty → Ty → Type
Term
ctx: List Ty
ctx
.nat: Ty
.nat
|
plus: {ctx : List Ty} → Term ctx Ty.nat → Term ctx Ty.nat → Term ctx Ty.nat
plus
:
Term: List Ty → Ty → Type
Term
ctx: List Ty
ctx
.nat: Ty
.nat
Term: List Ty → Ty → Type
Term
ctx: List Ty
ctx
.nat: Ty
.nat
Term: List Ty → Ty → Type
Term
ctx: List Ty
ctx
.nat: Ty
.nat
|
app: {ctx : List Ty} → {dom ran : Ty} → Term ctx (Ty.fn dom ran) → Term ctx dom → Term ctx ran
app
:
Term: List Ty → Ty → Type
Term
ctx: List Ty
ctx
(
.fn: Ty → Ty → Ty
.fn
dom: Ty
dom
ran: Ty
ran
)
Term: List Ty → Ty → Type
Term
ctx: List Ty
ctx
dom: Ty
dom
Term: List Ty → Ty → Type
Term
ctx: List Ty
ctx
ran: Ty
ran
|
lam: {dom : Ty} → {ctx : List Ty} → {ran : Ty} → Term (dom :: ctx) ran → Term ctx (Ty.fn dom ran)
lam
:
Term: List Ty → Ty → Type
Term
(
dom: Ty
dom
::
ctx: List Ty
ctx
)
ran: Ty
ran
Term: List Ty → Ty → Type
Term
ctx: List Ty
ctx
(
.fn: Ty → Ty → Ty
.fn
dom: Ty
dom
ran: Ty
ran
) |
«let»: {ctx : List Ty} → {ty₁ ty₂ : Ty} → Term ctx ty₁ → Term (ty₁ :: ctx) ty₂ → Term ctx ty₂
«let»
:
Term: List Ty → Ty → Type
Term
ctx: List Ty
ctx
ty₁: Ty
ty₁
Term: List Ty → Ty → Type
Term
(
ty₁: Ty
ty₁
::
ctx: List Ty
ctx
)
ty₂: Ty
ty₂
Term: List Ty → Ty → Type
Term
ctx: List Ty
ctx
ty₂: Ty
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))
add
:
Term: List Ty → Ty → Type
Term
[]: List Ty
[]
(
fn: Ty → Ty → Ty
fn
nat: Ty
nat
(
fn: Ty → Ty → Ty
fn
nat: Ty
nat
nat: Ty
nat
)) :=
lam: {dom : Ty} → {ctx : List Ty} → {ran : Ty} → Term (dom :: ctx) ran → Term ctx (fn dom ran)
lam
(
lam: {dom : Ty} → {ctx : List Ty} → {ran : Ty} → Term (dom :: ctx) ran → Term ctx (fn dom ran)
lam
(
plus: {ctx : List Ty} → Term ctx nat → Term ctx nat → Term ctx nat
plus
(
var: {ty : Ty} → {ctx : List Ty} → Member ty ctx → Term ctx ty
var
(
tail: {α : Type} → {a : α} → {bs : List α} → {b : α} → Member a bs → Member a (b :: bs)
tail
head: {α : Type} → {a : α} → {as : List α} → Member a (a :: as)
head
)) (
var: {ty : Ty} → {ctx : List Ty} → Member ty ctx → Term ctx ty
var
head: {α : Type} → {a : α} → {as : List α} → Member a (a :: as)
head
))) def
three_the_hard_way: Term [] nat
three_the_hard_way
:
Term: List Ty → Ty → Type
Term
[]: List Ty
[]
nat: Ty
nat
:=
app: {ctx : List Ty} → {dom ran : Ty} → Term ctx (fn dom ran) → Term ctx dom → Term ctx ran
app
(
app: {ctx : List Ty} → {dom ran : Ty} → Term ctx (fn dom ran) → Term ctx dom → Term ctx ran
app
add: Term [] (fn nat (fn nat nat))
add
(
const: {ctx : List Ty} → Nat → Term ctx nat
const
1: Nat
1
)) (
const: {ctx : List Ty} → Nat → Term ctx nat
const
2: Nat
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: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → Ty.denote ty
Term.denote
:
Term: List Ty → Ty → Type
Term
ctx: List Ty
ctx
ty: Ty
ty
HList: {α : Type} → (α → Type) → List α → Type
HList
Ty.denote: Ty → Type
Ty.denote
ctx: List Ty
ctx
ty: Ty
ty
.
denote: Ty → Type
denote
|
var: {ty : Ty} → {ctx : List Ty} → Member ty ctx → Term ctx ty
var
h: Member ty ctx
h
,
env: HList Ty.denote ctx
env
=>
env: HList Ty.denote ctx
env
.
get: {α : Type} → {β : α → Type} → {is : List α} → {i : α} → HList β is → Member i is → β i
get
h: Member ty ctx
h
|
const: {ctx : List Ty} → Nat → Term ctx nat
const
n: Nat
n
, _ =>
n: Nat
n
|
plus: {ctx : List Ty} → Term ctx nat → Term ctx nat → Term ctx nat
plus
a: Term ctx nat
a
b: Term ctx nat
b
,
env: HList Ty.denote ctx
env
=>
a: Term ctx nat
a
.
denote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → Ty.denote ty
denote
env: HList Ty.denote ctx
env
+
b: Term ctx nat
b
.
denote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → Ty.denote ty
denote
env: HList Ty.denote ctx
env
|
app: {ctx : List Ty} → {dom ran : Ty} → Term ctx (fn dom ran) → Term ctx dom → Term ctx ran
app
f: Term ctx (fn dom✝ ty)
f
a: Term ctx dom✝
a
,
env: HList Ty.denote ctx
env
=>
f: Term ctx (fn dom✝ ty)
f
.
denote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → Ty.denote ty
denote
env: HList Ty.denote ctx
env
(
a: Term ctx dom✝
a
.
denote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → Ty.denote ty
denote
env: HList Ty.denote ctx
env
) |
lam: {dom : Ty} → {ctx : List Ty} → {ran : Ty} → Term (dom :: ctx) ran → Term ctx (fn dom ran)
lam
b: Term (dom✝ :: ctx) ran✝
b
,
env: HList Ty.denote ctx
env
=> fun
x: Ty.denote dom✝
x
=>
b: Term (dom✝ :: ctx) ran✝
b
.
denote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → Ty.denote ty
denote
(
x: Ty.denote dom✝
x
::
env: HList Ty.denote ctx
env
) |
«let»: {ctx : List Ty} → {ty₁ ty₂ : Ty} → Term ctx ty₁ → Term (ty₁ :: ctx) ty₂ → Term ctx ty₂
«let»
a: Term ctx ty₁✝
a
b: Term (ty₁✝ :: ctx) ty
b
,
env: HList Ty.denote ctx
env
=>
b: Term (ty₁✝ :: ctx) ty
b
.
denote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → Ty.denote ty
denote
(
a: Term ctx ty₁✝
a
.
denote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → Ty.denote ty
denote
env: HList Ty.denote ctx
env
::
env: HList Ty.denote ctx
env
)

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

example: Term.denote three_the_hard_way [] = 3
example
:
three_the_hard_way: Term [] nat
three_the_hard_way
.
denote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → Ty.denote ty
denote
[]: HList Ty.denote []
[]
=
3: Ty.denote nat
3
:=
rfl: ∀ {α : Type} {a : α}, a = a
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: {ctx : List Ty} → {ty : Ty} → Term ctx ty → Term ctx ty
Term.constFold
:
Term: List Ty → Ty → Type
Term
ctx: List Ty
ctx
ty: Ty
ty
Term: List Ty → Ty → Type
Term
ctx: List Ty
ctx
ty: Ty
ty
|
const: {ctx : List Ty} → Nat → Term ctx nat
const
n: Nat
n
=>
const: {ctx : List Ty} → Nat → Term ctx nat
const
n: Nat
n
|
var: {ty : Ty} → {ctx : List Ty} → Member ty ctx → Term ctx ty
var
h: Member ty ctx
h
=>
var: {ty : Ty} → {ctx : List Ty} → Member ty ctx → Term ctx ty
var
h: Member ty ctx
h
|
app: {ctx : List Ty} → {dom ran : Ty} → Term ctx (fn dom ran) → Term ctx dom → Term ctx ran
app
f: Term ctx (fn dom✝ ty)
f
a: Term ctx dom✝
a
=>
app: {ctx : List Ty} → {dom ran : Ty} → Term ctx (fn dom ran) → Term ctx dom → Term ctx ran
app
f: Term ctx (fn dom✝ ty)
f
.
constFold: {ctx : List Ty} → {ty : Ty} → Term ctx ty → Term ctx ty
constFold
a: Term ctx dom✝
a
.
constFold: {ctx : List Ty} → {ty : Ty} → Term ctx ty → Term ctx ty
constFold
|
lam: {dom : Ty} → {ctx : List Ty} → {ran : Ty} → Term (dom :: ctx) ran → Term ctx (fn dom ran)
lam
b: Term (dom✝ :: ctx) ran✝
b
=>
lam: {dom : Ty} → {ctx : List Ty} → {ran : Ty} → Term (dom :: ctx) ran → Term ctx (fn dom ran)
lam
b: Term (dom✝ :: ctx) ran✝
b
.
constFold: {ctx : List Ty} → {ty : Ty} → Term ctx ty → Term ctx ty
constFold
|
«let»: {ctx : List Ty} → {ty₁ ty₂ : Ty} → Term ctx ty₁ → Term (ty₁ :: ctx) ty₂ → Term ctx ty₂
«let»
a: Term ctx ty₁✝
a
b: Term (ty₁✝ :: ctx) ty
b
=>
«let»: {ctx : List Ty} → {ty₁ ty₂ : Ty} → Term ctx ty₁ → Term (ty₁ :: ctx) ty₂ → Term ctx ty₂
«let»
a: Term ctx ty₁✝
a
.
constFold: {ctx : List Ty} → {ty : Ty} → Term ctx ty → Term ctx ty
constFold
b: Term (ty₁✝ :: ctx) ty
b
.
constFold: {ctx : List Ty} → {ty : Ty} → Term ctx ty → Term ctx ty
constFold
|
plus: {ctx : List Ty} → Term ctx nat → Term ctx nat → Term ctx nat
plus
a: Term ctx nat
a
b: Term ctx nat
b
=> match
a: Term ctx nat
a
.
constFold: {ctx : List Ty} → {ty : Ty} → Term ctx ty → Term ctx ty
constFold
,
b: Term ctx nat
b
.
constFold: {ctx : List Ty} → {ty : Ty} → Term ctx ty → Term ctx ty
constFold
with |
const: {ctx : List Ty} → Nat → Term ctx nat
const
n: Nat
n
,
const: {ctx : List Ty} → Nat → Term ctx nat
const
m: Nat
m
=>
const: {ctx : List Ty} → Nat → Term ctx nat
const
(
n: Nat
n
+
m: Nat
m
) |
a': Term ctx nat
a'
,
b': Term ctx nat
b'
=>
plus: {ctx : List Ty} → Term ctx nat → Term ctx nat → Term ctx nat
plus
a': Term ctx nat
a'
b': Term ctx nat
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/simplications 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 simplier 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: ∀ {ctx : List Ty} {ty : Ty} {env : HList Ty.denote ctx} (e : Term ctx ty), denote (constFold e) env = denote e env
Term.constFold_sound
(
e: Term ctx ty
e
:
Term: List Ty → Ty → Type
Term
ctx: List Ty
ctx
ty: Ty
ty
) :
e: Term ctx ty
e
.
constFold: {ctx : List Ty} → {ty : Ty} → Term ctx ty → Term ctx ty
constFold
.
denote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → Ty.denote ty
denote
env: HList Ty.denote ctx
env
=
e: Term ctx ty
e
.
denote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → Ty.denote ty
denote
env: HList Ty.denote ctx
env
:=
ctx: List Ty
ty: Ty
env: HList Ty.denote ctx
e: Term ctx ty

denote (constFold e) env = denote e env
ctx: List Ty
ty: Ty
env: HList Ty.denote ctx
e: Term ctx ty

denote (constFold e) env = denote e env

Goals accomplished! 🐙
ctx: List Ty
ty: Ty
ctx✝: List Ty
a, b: Term ctx nat
iha: {env : HList Ty.denote ctx}, denote (constFold a) env = denote a env
ihb: {env : HList Ty.denote ctx}, denote (constFold b) env = denote b env
env: HList Ty.denote ctx

plus
denote (match constFold a, constFold b with | const n, const m => const (n + m) | a', b' => plus a' b') env = denote a env + denote b env
ctx: List Ty
ty: Ty
ctx✝: List Ty
a, b: Term ctx nat
iha: {env : HList Ty.denote ctx}, denote (constFold a) env = denote a env
ihb: {env : HList Ty.denote ctx}, denote (constFold b) env = denote b env
env: HList Ty.denote ctx
x✝¹, x✝: Term ctx nat
n✝, m✝: Nat
heq✝¹: constFold a = const n
heq✝: constFold b = const m

plus.h_1
denote (const (n + m)) env = denote a env + denote b env
ctx: List Ty
ty: Ty
ctx✝: List Ty
a, b: Term ctx nat
iha: {env : HList Ty.denote ctx}, denote (constFold a) env = denote a env
ihb: {env : HList Ty.denote ctx}, denote (constFold b) env = denote b env
env: HList Ty.denote ctx
x✝², x✝¹: Term ctx nat
x✝: (n m : Nat), constFold a = const n constFold b = const m False
denote (plus (constFold a) (constFold b)) env = denote a env + denote b env
ctx: List Ty
ty: Ty
ctx✝: List Ty
a, b: Term ctx nat
iha: {env : HList Ty.denote ctx}, denote (constFold a) env = denote a env
ihb: {env : HList Ty.denote ctx}, denote (constFold b) env = denote b env
env: HList Ty.denote ctx
x✝¹, x✝: Term ctx nat
n✝, m✝: Nat
heq✝¹: constFold a = const n
heq✝: constFold b = const m

plus.h_1
denote (const (n + m)) env = denote a env + denote b env
ctx: List Ty
ty: Ty
ctx✝: List Ty
a, b: Term ctx nat
iha: {env : HList Ty.denote ctx}, denote (constFold a) env = denote a env
ihb: {env : HList Ty.denote ctx}, denote (constFold b) env = denote b env
env: HList Ty.denote ctx
x✝², x✝¹: Term ctx nat
x✝: (n m : Nat), constFold a = const n constFold b = const m False
denote (plus (constFold a) (constFold b)) env = denote a env + denote b env

Goals accomplished! 🐙
ctx: List Ty
ty: Ty
ctx✝: List Ty
a, b: Term ctx nat
iha: {env : HList Ty.denote ctx}, denote (constFold a) env = denote a env
ihb: {env : HList Ty.denote ctx}, denote (constFold b) env = denote b env
env: HList Ty.denote ctx
x✝², x✝¹: Term ctx nat
x✝: (n m : Nat), constFold a = const n constFold b = const m False

plus.h_2
denote (plus (constFold a) (constFold b)) env = denote a env + denote b env

Goals accomplished! 🐙