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.3817
a (a: ?m.3817
a::as: List ?m.3817
as)
| tail: {α : Type} → {a : α} → {bs : List α} → {b : α} → Member a bs → Member a (b :: bs)
tail : Member: {α : Type} → α → List α → Type
Member a: ?m.3989
a bs: List ?m.3989
bs → Member: {α : Type} → α → List α → Type
Member a: ?m.3989
a (b: ?m.3989
b::bs: List ?m.3989
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.
defHList.get :HList.get: {α : Type} → {β : α → Type u_1} → {is : List α} → {i : α} → HList β is → Member i is → β iHListHList: {α : Type} → (α → Type u_1) → List α → Type u_1ββ: ?m.4593 → Type u_1is →is: List ?m.4593MemberMember: {α : Type} → α → List α → Typeii: ?m.4593is →is: List ?m.4593ββ: ?m.4593 → Type u_1i |i: ?m.4593a::a: β ias,as: HList β is✝.head =>.head: Member i (i :: is✝)a |a: β i::as,as: HList β is✝.tail.tail: {α : Type} → {a : α} → {bs : List α} → {b : α} → Member a bs → Member a (b :: bs)h =>h: Member i is✝as.as: HList β is✝getget: {α : Type} → {β : α → Type u_1} → {is : List α} → {i : α} → HList β is → Member i is → β ihh: Member i is✝
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 (dom.fn 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 (dom.fn 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 [] (nat.fn (nat.fn 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 (dom.fn ran)
lam (lam: {dom : Ty} → {ctx : List Ty} → {ran : Ty} → Term (dom :: ctx) ran → Term ctx (dom.fn 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 (dom.fn ran) → Term ctx dom → Term ctx ran
app (app: {ctx : List Ty} → {dom ran : Ty} → Term ctx (dom.fn ran) → Term ctx dom → Term ctx ran
app add: Term [] (nat.fn (nat.fn 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
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
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
denote env: HList Ty.denote ctx
env
| app: {ctx : List Ty} → {dom ran : Ty} → Term ctx (dom.fn ran) → Term ctx dom → Term ctx ran
app f: Term ctx (dom✝.fn ty)
f a: Term ctx dom✝
a, env: HList Ty.denote ctx
env => f: Term ctx (dom✝.fn ty)
f.denote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → ty.denote
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
denote env: HList Ty.denote ctx
env)
| lam: {dom : Ty} → {ctx : List Ty} → {ran : Ty} → Term (dom :: ctx) ran → Term ctx (dom.fn ran)
lam b: Term (dom✝ :: ctx) ran✝
b, env: HList Ty.denote ctx
env => fun x: dom✝.denote
x => b: Term (dom✝ :: ctx) ran✝
b.denote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → ty.denote
denote (x: dom✝.denote
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
denote (a: Term ctx ty₁✝
a.denote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → ty.denote
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: three_the_hard_way.denote [] = 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
denote []: HList Ty.denote []
[] = 3: nat.denote
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 (dom.fn ran) → Term ctx dom → Term ctx ran
app f: Term ctx (dom✝.fn ty)
f a: Term ctx dom✝
a => app: {ctx : List Ty} → {dom ran : Ty} → Term ctx (dom.fn ran) → Term ctx dom → Term ctx ran
app f: Term ctx (dom✝.fn 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 (dom.fn ran)
lam b: Term (dom✝ :: ctx) ran✝
b => lam: {dom : Ty} → {ctx : List Ty} → {ran : Ty} → Term (dom :: ctx) ran → Term ctx (dom.fn 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/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
.
theoremTerm.constFold_sound (Term.constFold_sound: ∀ {ctx : List Ty} {ty : Ty} {env : HList Ty.denote ctx} (e : Term ctx ty), e.constFold.denote env = e.denote enve :e: Term ctx tyTermTerm: List Ty → Ty → Typectxctx: List Tyty) :ty: Tye.e: Term ctx tyconstFold.constFold: {ctx : List Ty} → {ty : Ty} → Term ctx ty → Term ctx tydenotedenote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → ty.denoteenv =env: HList Ty.denote ctxe.e: Term ctx tydenotedenote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → ty.denoteenv :=env: HList Ty.denote ctxGoals accomplished! 🐙ctx: List Ty
ty: Ty
env: HList Ty.denote ctx
e: Term ctx tye.constFold.denote env = e.denote envctx: List Ty
ty: Ty
ctx✝: List Ty
a, b: Term ctx✝ nat
iha: ∀ {env : HList Ty.denote ctx✝}, a.constFold.denote env = a.denote env
ihb: ∀ {env : HList Ty.denote ctx✝}, b.constFold.denote env = b.denote env
env: HList Ty.denote ctx✝
plus(match a.constFold, b.constFold with | const n, const m => const (n + m) | a', b' => a'.plus b').denote env = a.denote env + b.denote envctx: List Ty
ty: Ty
ctx✝: List Ty
a, b: Term ctx✝ nat
iha: ∀ {env : HList Ty.denote ctx✝}, a.constFold.denote env = a.denote env
ihb: ∀ {env : HList Ty.denote ctx✝}, b.constFold.denote env = b.denote env
env: HList Ty.denote ctx✝
plus(match a.constFold, b.constFold with | const n, const m => const (n + m) | a', b' => a'.plus b').denote env = a.denote env + b.denote envctx: List Ty
ty: Ty
ctx✝: List Ty
a, b: Term ctx✝ nat
iha: ∀ {env : HList Ty.denote ctx✝}, a.constFold.denote env = a.denote env
ihb: ∀ {env : HList Ty.denote ctx✝}, b.constFold.denote env = b.denote env
env: HList Ty.denote ctx✝
x✝¹, x✝: Term ctx✝ nat
n✝, m✝: Nat
heq✝¹: a.constFold = const n✝
heq✝: b.constFold = const m✝
plus.h_1(const (n✝ + m✝)).denote env = a.denote env + b.denote envctx: List Ty
ty: Ty
ctx✝: List Ty
a, b: Term ctx✝ nat
iha: ∀ {env : HList Ty.denote ctx✝}, a.constFold.denote env = a.denote env
ihb: ∀ {env : HList Ty.denote ctx✝}, b.constFold.denote env = b.denote env
env: HList Ty.denote ctx✝
x✝², x✝¹: Term ctx✝ nat
x✝: ∀ (n m : Nat), a.constFold = const n → b.constFold = const m → False(a.constFold.plus b.constFold).denote env = a.denote env + b.denote envctx: List Ty
ty: Ty
ctx✝: List Ty
a, b: Term ctx✝ nat
iha: ∀ {env : HList Ty.denote ctx✝}, a.constFold.denote env = a.denote env
ihb: ∀ {env : HList Ty.denote ctx✝}, b.constFold.denote env = b.denote env
env: HList Ty.denote ctx✝
x✝¹, x✝: Term ctx✝ nat
n✝, m✝: Nat
heq✝¹: a.constFold = const n✝
heq✝: b.constFold = const m✝
plus.h_1(const (n✝ + m✝)).denote env = a.denote env + b.denote envctx: List Ty
ty: Ty
ctx✝: List Ty
a, b: Term ctx✝ nat
iha: ∀ {env : HList Ty.denote ctx✝}, a.constFold.denote env = a.denote env
ihb: ∀ {env : HList Ty.denote ctx✝}, b.constFold.denote env = b.denote env
env: HList Ty.denote ctx✝
x✝², x✝¹: Term ctx✝ nat
x✝: ∀ (n m : Nat), a.constFold = const n → b.constFold = const m → False(a.constFold.plus b.constFold).denote env = a.denote env + b.denote envGoals accomplished! 🐙ctx: List Ty
ty: Ty
ctx✝: List Ty
a, b: Term ctx✝ nat
iha: ∀ {env : HList Ty.denote ctx✝}, a.constFold.denote env = a.denote env
ihb: ∀ {env : HList Ty.denote ctx✝}, b.constFold.denote env = b.denote env
env: HList Ty.denote ctx✝
x✝², x✝¹: Term ctx✝ nat
x✝: ∀ (n m : Nat), a.constFold = const n → b.constFold = const m → False
plus.h_2(a.constFold.plus b.constFold).denote env = a.denote env + b.denote envGoals accomplished! 🐙