The Well-Typed Interpreter

In this example, we build an interpreter for a simple functional programming language, with variables, function application, binary operators and an if...then...else construct. We will use the dependent type system to ensure that any programs which can be represented are well-typed.

Remark: this example is based on an example found in the Idris manual.

Vectors

A Vec is a list of size n whose elements belong to a type α.

inductive 
Vec: Type u → Nat → Type u
Vec (
α: Type u
α : 
Type u: Type (u + 1)
Type u) : 
Nat: Type
Nat → 
Type u: Type (u + 1)
Type u
  | 
nil: {α : Type u} → Vec α 0
nil : 
Vec: Type u → Nat → Type u
Vec 
α: Type u
α 
0: Nat
0
  | 
cons: {α : Type u} → {n : Nat} → α → Vec α n → Vec α (n + 1)
cons : 
α: Type u
α → 
Vec: Type u → Nat → Type u
Vec 
α: Type u
α 
n: Nat
n → 
Vec: Type u → Nat → Type u
Vec 
α: Type u
α (
n: Nat
n+
1: Nat
1)

We can overload the List.cons notation :: and use it to create Vecs.

infix:67 " :: " => 
Vec.cons: {α : Type u} → {n : Nat} → α → Vec α n → Vec α (n + 1)
Vec.cons

Now, we define the types of our simple functional language. We have integers, booleans, and functions, represented by Ty.

inductive 
Ty: Type
Ty where
  | 
int: Ty
int
  | 
bool: Ty
bool
  | 
fn: Ty → Ty → Ty
fn (
a: Ty
a 
r: Ty
r : 
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.interp 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.interp Ty.int). Since Ty.interp is marked as [reducible], the typeclass resolution procedure can reduce Ty.interp Ty.int to Int, and use the builtin instance for Add Int as the solution.

@[reducible] def 
Ty.interp: Ty → Type
Ty.interp : 
Ty: Type
Ty → 
Type: Type 1
Type
  | 
int: Ty
int    => 
Int: Type
Int
  | 
bool: Ty
bool   => 
Bool: Type
Bool
  | 
fn: Ty → Ty → Ty
fn 
a: Ty
a 
r: Ty
r => 
a: Ty
a.
interp: Ty → Type
interp → 
r: Ty
r.
interp: Ty → Type
interp

Expressions are indexed by the types of the local variables, and the type of the expression itself.

inductive 
HasType: {n : Nat} → Fin n → Vec Ty n → Ty → Type
HasType : 
Fin: Nat → Type
Fin 
n: Nat
n → 
Vec: Type → Nat → Type
Vec 
Ty: Type
Ty 
n: Nat
n → 
Ty: Type
Ty → 
Type: Type 1
Type where
  | 
stop: {ty : Ty} → {x : Nat} → {ctx : Vec Ty x} → HasType 0 (ty :: ctx) ty
stop : 
HasType: {n : Nat} → Fin n → Vec Ty n → Ty → Type
HasType 
0: Fin (?m.2875 + 1)
0 (
ty: Ty
ty :: 
ctx: Vec Ty ?m.2875
ctx) 
ty: Ty
ty
  | 
pop: {x : Nat} → {k : Fin x} → {ctx : Vec Ty x} → {ty u : Ty} → HasType k ctx ty → HasType k.succ (u :: ctx) ty
pop  : 
HasType: {n : Nat} → Fin n → Vec Ty n → Ty → Type
HasType 
k: Fin ?m.3065
k 
ctx: Vec Ty ?m.3065
ctx 
ty: Ty
ty → 
HasType: {n : Nat} → Fin n → Vec Ty n → Ty → Type
HasType 
k: Fin ?m.3065
k.
succ: {n : Nat} → Fin n → Fin (n + 1)
succ (
u: Ty
u :: 
ctx: Vec Ty ?m.3065
ctx) 
ty: Ty
ty

inductive 
Expr: {n : Nat} → Vec Ty n → Ty → Type
Expr : 
Vec: Type → Nat → Type
Vec 
Ty: Type
Ty 
n: Nat
n → 
Ty: Type
Ty → 
Type: Type 1
Type where
  | 
var: {n : Nat} → {i : Fin n} → {ctx : Vec Ty n} → {ty : Ty} → HasType i ctx ty → Expr ctx ty
var   : 
HasType: {n : Nat} → Fin n → Vec Ty n → Ty → Type
HasType 
i: Fin ?m.3961
i 
ctx: Vec Ty ?m.3961
ctx 
ty: Ty
ty → 
Expr: {n : Nat} → Vec Ty n → Ty → Type
Expr 
ctx: Vec Ty ?m.3961
ctx 
ty: Ty
ty
  | 
val: {n : Nat} → {ctx : Vec Ty n} → Int → Expr ctx Ty.int
val   : 
Int: Type
Int → 
Expr: {n : Nat} → Vec Ty n → Ty → Type
Expr 
ctx: Vec Ty ?m.3982
ctx 
Ty.int: Ty
Ty.int
  | 
lam: {n : Nat} → {a : Ty} → {ctx : Vec Ty n} → {ty : Ty} → Expr (a :: ctx) ty → Expr ctx (a.fn ty)
lam   : 
Expr: {n : Nat} → Vec Ty n → Ty → Type
Expr (
a: Ty
a :: 
ctx: Vec Ty ?m.4146
ctx) 
ty: Ty
ty → 
Expr: {n : Nat} → Vec Ty n → Ty → Type
Expr 
ctx: Vec Ty ?m.4146
ctx (
Ty.fn: Ty → Ty → Ty
Ty.fn 
a: Ty
a 
ty: Ty
ty)
  | 
app: {n : Nat} → {ctx : Vec Ty n} → {a ty : Ty} → Expr ctx (a.fn ty) → Expr ctx a → Expr ctx ty
app   : 
Expr: {n : Nat} → Vec Ty n → Ty → Type
Expr 
ctx: Vec Ty ?m.4301
ctx (
Ty.fn: Ty → Ty → Ty
Ty.fn 
a: Ty
a 
ty: Ty
ty) → 
Expr: {n : Nat} → Vec Ty n → Ty → Type
Expr 
ctx: Vec Ty ?m.4301
ctx 
a: Ty
a → 
Expr: {n : Nat} → Vec Ty n → Ty → Type
Expr 
ctx: Vec Ty ?m.4301
ctx 
ty: Ty
ty
  | 
op: {n : Nat} → {ctx : Vec Ty n} → {a b c : Ty} → (a.interp → b.interp → c.interp) → Expr ctx a → Expr ctx b → Expr ctx c
op    : (
a: Ty
a.
interp: Ty → Type
interp → 
b: Ty
b.
interp: Ty → Type
interp → 
c: Ty
c.
interp: Ty → Type
interp) → 
Expr: {n : Nat} → Vec Ty n → Ty → Type
Expr 
ctx: Vec Ty ?m.4391
ctx 
a: Ty
a → 
Expr: {n : Nat} → Vec Ty n → Ty → Type
Expr 
ctx: Vec Ty ?m.4391
ctx 
b: Ty
b → 
Expr: {n : Nat} → Vec Ty n → Ty → Type
Expr 
ctx: Vec Ty ?m.4391
ctx 
c: Ty
c
  | 
ife: {n : Nat} → {ctx : Vec Ty n} → {a : Ty} → Expr ctx Ty.bool → Expr ctx a → Expr ctx a → Expr ctx a
ife   : 
Expr: {n : Nat} → Vec Ty n → Ty → Type
Expr 
ctx: Vec Ty ?m.4512
ctx 
Ty.bool: Ty
Ty.bool → 
Expr: {n : Nat} → Vec Ty n → Ty → Type
Expr 
ctx: Vec Ty ?m.4512
ctx 
a: Ty
a → 
Expr: {n : Nat} → Vec Ty n → Ty → Type
Expr 
ctx: Vec Ty ?m.4512
ctx 
a: Ty
a → 
Expr: {n : Nat} → Vec Ty n → Ty → Type
Expr 
ctx: Vec Ty ?m.4512
ctx 
a: Ty
a
  | 
delay: {n : Nat} → {ctx : Vec Ty n} → {a : Ty} → (Unit → Expr ctx a) → Expr ctx a
delay : (
Unit: Type
Unit → 
Expr: {n : Nat} → Vec Ty n → Ty → Type
Expr 
ctx: Vec Ty ?m.4555
ctx 
a: Ty
a) → 
Expr: {n : Nat} → Vec Ty n → Ty → Type
Expr 
ctx: Vec Ty ?m.4555
ctx 
a: Ty
a

We use the command open to create the aliases stop and pop for HasType.stop and HasType.pop respectively.

open HasType (
stop: {ty : Ty} → {x : Nat} → {ctx : Vec Ty x} → HasType 0 (ty :: ctx) ty
stop 
pop: {x : Nat} → {k : Fin x} → {ctx : Vec Ty x} → {ty u : Ty} → HasType k ctx ty → HasType k.succ (u :: ctx) ty
pop)

Since expressions are indexed by their type, we can read the typing rules of the language from the definitions of the constructors. Let us look at each constructor in turn.

We use a nameless representation for variables — they are de Bruijn indexed. Variables are represented by a proof of their membership in the context, HasType i ctx ty, which is a proof that variable i in context ctx has type ty.

We can treat stop as a proof that the most recently defined variable is well-typed, and pop n as a proof that, if the nth most recently defined variable is well-typed, so is the n+1th. In practice, this means we use stop to refer to the most recently defined variable, pop stop to refer to the next, and so on, via the Expr.var constructor.

A value Expr.val carries a concrete representation of an integer.

A lambda Expr.lam creates a function. In the scope of a function of type Ty.fn a ty, there is a new local variable of type a.

A function application Expr.app produces a value of type ty given a function from a to ty and a value of type a.

The constructor Expr.op allows us to use arbitrary binary operators, where the type of the operator informs what the types of the arguments must be.

Finally, the constructor Exp.ife represents a if-then-else expression. The condition is a Boolean, and each branch must have the same type.

The auxiliary constructor Expr.delay is used to delay evaluation.

When we evaluate an Expr, we’ll need to know the values in scope, as well as their types. Env is an environment, indexed over the types in scope. Since an environment is just another form of list, albeit with a strongly specified connection to the vector of local variable types, we overload again the notation :: so that we can use the usual list syntax. Given a proof that a variable is defined in the context, we can then produce a value from the environment.

inductive 
Env: {n : Nat} → Vec Ty n → Type
Env : 
Vec: Type → Nat → Type
Vec 
Ty: Type
Ty 
n: Nat
n → 
Type: Type 1
Type where
  | 
nil: Env Vec.nil
nil  : 
Env: {n : Nat} → Vec Ty n → Type
Env 
Vec.nil: {α : Type} → Vec α 0
Vec.nil
  | 
cons: {a : Ty} → {x : Nat} → {ctx : Vec Ty x} → a.interp → Env ctx → Env (a :: ctx)
cons : 
Ty.interp: Ty → Type
Ty.interp 
a: Ty
a → 
Env: {n : Nat} → Vec Ty n → Type
Env 
ctx: Vec Ty ?m.9447
ctx → 
Env: {n : Nat} → Vec Ty n → Type
Env (
a: Ty
a :: 
ctx: Vec Ty ?m.9447
ctx)

infix:67 " :: " => 
Env.cons: {a : Ty} → {x : Nat} → {ctx : Vec Ty x} → a.interp → Env ctx → Env (a :: ctx)
Env.cons

def 
Env.lookup: {n : Nat} → {i : Fin n} → {ctx : Vec Ty n} → {ty : Ty} → HasType i ctx ty → Env ctx → ty.interp
Env.lookup : 
HasType: {n : Nat} → Fin n → Vec Ty n → Ty → Type
HasType 
i: Fin ?m.12089
i 
ctx: Vec Ty ?m.12089
ctx 
ty: Ty
ty → 
Env: {n : Nat} → Vec Ty n → Type
Env 
ctx: Vec Ty ?m.12089
ctx → 
ty: Ty
ty.
interp: Ty → Type
interp
  | 
stop: {ty : Ty} → {x : Nat} → {ctx : Vec Ty x} → HasType 0 (ty :: ctx) ty
stop,  
x: ty.interp
x :: 
xs: Env ctx✝
xs => 
x: ty.interp
x
  | 
pop: {x : Nat} → {k : Fin x} → {ctx : Vec Ty x} → {ty u : Ty} → HasType k ctx ty → HasType k.succ (u :: ctx) ty
pop 
k: HasType k✝ ctx✝ ty
k, 
x: u✝.interp
x :: 
xs: Env ctx✝
xs => 
lookup: {n : Nat} → {i : Fin n} → {ctx : Vec Ty n} → {ty : Ty} → HasType i ctx ty → Env ctx → ty.interp
lookup 
k: HasType k✝ ctx✝ ty
k 
xs: Env ctx✝
xs

Given this, an interpreter is a function which translates an Expr into a Lean value with respect to a specific environment.

def 
Expr.interp: {a : Nat} → {ctx : Vec Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → ty.interp
Expr.interp (
env: Env ctx
env : 
Env: {n : Nat} → Vec Ty n → Type
Env 
ctx: Vec Ty ?m.14954
ctx) : 
Expr: {n : Nat} → Vec Ty n → Ty → Type
Expr 
ctx: Vec Ty ?m.14954
ctx 
ty: Ty
ty → 
ty: Ty
ty.
interp: Ty → Type
interp
  | 
var: {n : Nat} → {i : Fin n} → {ctx : Vec Ty n} → {ty : Ty} → HasType i ctx ty → Expr ctx ty
var 
i: HasType i✝ ctx ty
i     => 
env: Env ctx
env.
lookup: {n : Nat} → {i : Fin n} → {ctx : Vec Ty n} → {ty : Ty} → HasType i ctx ty → Env ctx → ty.interp
lookup 
i: HasType i✝ ctx ty
i
  | 
val: {n : Nat} → {ctx : Vec Ty n} → Int → Expr ctx Ty.int
val 
x: Int
x     => 
x: Int
x
  | 
lam: {n : Nat} → {a : Ty} → {ctx : Vec Ty n} → {ty : Ty} → Expr (a :: ctx) ty → Expr ctx (a.fn ty)
lam 
b: Expr (a✝ :: ctx) ty✝
b     => fun 
x: a✝.interp
x => 
b: Expr (a✝ :: ctx) ty✝
b.
interp: {a : Nat} → {ctx : Vec Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → ty.interp
interp (
Env.cons: {a : Ty} → {x : Nat} → {ctx : Vec Ty x} → a.interp → Env ctx → Env (a :: ctx)
Env.cons 
x: a✝.interp
x 
env: Env ctx
env)
  | 
app: {n : Nat} → {ctx : Vec Ty n} → {a ty : Ty} → Expr ctx (a.fn ty) → Expr ctx a → Expr ctx ty
app 
f: Expr ctx (a✝.fn ty)
f 
a: Expr ctx a✝
a   => 
f: Expr ctx (a✝.fn ty)
f.
interp: {a : Nat} → {ctx : Vec Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → ty.interp
interp 
env: Env ctx
env (
a: Expr ctx a✝
a.
interp: {a : Nat} → {ctx : Vec Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → ty.interp
interp 
env: Env ctx
env)
  | 
op: {n : Nat} → {ctx : Vec Ty n} → {a b c : Ty} → (a.interp → b.interp → c.interp) → Expr ctx a → Expr ctx b → Expr ctx c
op 
o: a✝.interp → b✝.interp → ty.interp
o 
x: Expr ctx a✝
x 
y: Expr ctx b✝
y  => 
o: a✝.interp → b✝.interp → ty.interp
o (
x: Expr ctx a✝
x.
interp: {a : Nat} → {ctx : Vec Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → ty.interp
interp 
env: Env ctx
env) (
y: Expr ctx b✝
y.
interp: {a : Nat} → {ctx : Vec Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → ty.interp
interp 
env: Env ctx
env)
  | 
ife: {n : Nat} → {ctx : Vec Ty n} → {a : Ty} → Expr ctx Ty.bool → Expr ctx a → Expr ctx a → Expr ctx a
ife 
c: Expr ctx Ty.bool
c 
t: Expr ctx ty
t 
e: Expr ctx ty
e => if 
c: Expr ctx Ty.bool
c.
interp: {a : Nat} → {ctx : Vec Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → ty.interp
interp 
env: Env ctx
env then 
t: Expr ctx ty
t.
interp: {a : Nat} → {ctx : Vec Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → ty.interp
interp 
env: Env ctx
env else 
e: Expr ctx ty
e.
interp: {a : Nat} → {ctx : Vec Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → ty.interp
interp 
env: Env ctx
env
  | 
delay: {n : Nat} → {ctx : Vec Ty n} → {a : Ty} → (Unit → Expr ctx a) → Expr ctx a
delay 
a: Unit → Expr ctx ty
a   => (
a: Unit → Expr ctx ty
a 
(): Unit
()).
interp: {a : Nat} → {ctx : Vec Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → ty.interp
interp 
env: Env ctx
env

open Expr

We can make some simple test functions. Firstly, adding two inputs fun x y => y + x is written as follows.

def 
add: {a : Nat} → {ctx : Vec Ty a} → Expr ctx (Ty.int.fn (Ty.int.fn Ty.int))
add : 
Expr: {n : Nat} → Vec Ty n → Ty → Type
Expr 
ctx: Vec Ty ?m.18964
ctx (
Ty.fn: Ty → Ty → Ty
Ty.fn 
Ty.int: Ty
Ty.int (
Ty.fn: Ty → Ty → Ty
Ty.fn 
Ty.int: Ty
Ty.int 
Ty.int: Ty
Ty.int)) :=
  
lam: {n : Nat} → {a : Ty} → {ctx : Vec Ty n} → {ty : Ty} → Expr (a :: ctx) ty → Expr ctx (a.fn ty)
lam (
lam: {n : Nat} → {a : Ty} → {ctx : Vec Ty n} → {ty : Ty} → Expr (a :: ctx) ty → Expr ctx (a.fn ty)
lam (
op: {n : Nat} → {ctx : Vec Ty n} → {a b c : Ty} → (a.interp → b.interp → c.interp) → Expr ctx a → Expr ctx b → Expr ctx c
op 
(·+·): Ty.int.interp → Ty.int.interp → Ty.int.interp
(·+·) (
var: {n : Nat} → {i : Fin n} → {ctx : Vec Ty n} → {ty : Ty} → HasType i ctx ty → Expr ctx ty
var 
stop: {ty : Ty} → {x : Nat} → {ctx : Vec Ty x} → HasType 0 (ty :: ctx) ty
stop) (
var: {n : Nat} → {i : Fin n} → {ctx : Vec Ty n} → {ty : Ty} → HasType i ctx ty → Expr ctx ty
var (
pop: {x : Nat} → {k : Fin x} → {ctx : Vec Ty x} → {ty u : Ty} → HasType k ctx ty → HasType k.succ (u :: ctx) ty
pop 
stop: {ty : Ty} → {x : Nat} → {ctx : Vec Ty x} → HasType 0 (ty :: ctx) ty
stop))))

#eval
30 
add: {a : Nat} → {ctx : Vec Ty a} → Expr ctx (Ty.int.fn (Ty.int.fn Ty.int))
add.
interp: {a : Nat} → {ctx : Vec Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → ty.interp
interp 
Env.nil: Env Vec.nil
Env.nil 
10: Ty.int.interp
10 
20: Ty.int.interp
20

More interestingly, a factorial function fact (e.g. fun x => if (x == 0) then 1 else (fact (x-1) * x)), can be written as. Note that this is a recursive (non-terminating) definition. For every input value, the interpreter terminates, but the definition itself is non-terminating. We use two tricks to make sure Lean accepts it. First, we use the auxiliary constructor Expr.delay to delay its unfolding. Second, we add the annotation decreasing_by sorry which can be viewed as "trust me, this recursive definition makes sense". Recall that sorry is an unsound axiom in Lean.

def 
fact: {a : Nat} → {ctx : Vec Ty a} → Expr ctx (Ty.int.fn Ty.int)
fact
Warning: declaration uses 'sorry' : 
Expr: {n : Nat} → Vec Ty n → Ty → Type
Expr 
ctx: Vec Ty ?m.19347
ctx (
Ty.fn: Ty → Ty → Ty
Ty.fn 
Ty.int: Ty
Ty.int 
Ty.int: Ty
Ty.int) :=
  
lam: {n : Nat} → {a : Ty} → {ctx : Vec Ty n} → {ty : Ty} → Expr (a :: ctx) ty → Expr ctx (a.fn ty)
lam (
ife: {n : Nat} → {ctx : Vec Ty n} → {a : Ty} → Expr ctx Ty.bool → Expr ctx a → Expr ctx a → Expr ctx a
ife (
op: {n : Nat} → {ctx : Vec Ty n} → {a b c : Ty} → (a.interp → b.interp → c.interp) → Expr ctx a → Expr ctx b → Expr ctx c
op 
(·==·): Ty.int.interp → Ty.int.interp → Bool
(·==·) (
var: {n : Nat} → {i : Fin n} → {ctx : Vec Ty n} → {ty : Ty} → HasType i ctx ty → Expr ctx ty
var 
stop: {ty : Ty} → {x : Nat} → {ctx : Vec Ty x} → HasType 0 (ty :: ctx) ty
stop) (
val: {n : Nat} → {ctx : Vec Ty n} → Int → Expr ctx Ty.int
val 
0: Int
0))
           (
val: {n : Nat} → {ctx : Vec Ty n} → Int → Expr ctx Ty.int
val 
1: Int
1)
           (
op: {n : Nat} → {ctx : Vec Ty n} → {a b c : Ty} → (a.interp → b.interp → c.interp) → Expr ctx a → Expr ctx b → Expr ctx c
op 
(·*·): Ty.int.interp → Ty.int.interp → Ty.int.interp
(·*·) (
delay: {n : Nat} → {ctx : Vec Ty n} → {a : Ty} → (Unit → Expr ctx a) → Expr ctx a
delay fun 
_: Unit
_ => 
app: {n : Nat} → {ctx : Vec Ty n} → {a ty : Ty} → Expr ctx (a.fn ty) → Expr ctx a → Expr ctx ty
app 
fact: {a : Nat} → {ctx : Vec Ty a} → Expr ctx (Ty.int.fn Ty.int)
fact (
op: {n : Nat} → {ctx : Vec Ty n} → {a b c : Ty} → (a.interp → b.interp → c.interp) → Expr ctx a → Expr ctx b → Expr ctx c
op 
(·-·): Ty.int.interp → Ty.int.interp → Ty.int.interp
(·-·) (
var: {n : Nat} → {i : Fin n} → {ctx : Vec Ty n} → {ty : Ty} → HasType i ctx ty → Expr ctx ty
var 
stop: {ty : Ty} → {x : Nat} → {ctx : Vec Ty x} → HasType 0 (ty :: ctx) ty
stop) (
val: {n : Nat} → {ctx : Vec Ty n} → Int → Expr ctx Ty.int
val 
1: Int
1))) (
var: {n : Nat} → {i : Fin n} → {ctx : Vec Ty n} → {ty : Ty} → HasType i ctx ty → Expr ctx ty
var 
stop: {ty : Ty} → {x : Nat} → {ctx : Vec Ty x} → HasType 0 (ty :: ctx) ty
stop)))
  decreasing_by
a✝: Nat
ctx: Vec Ty a✝
a✝ + 1 < a✝ sorry
Goals accomplished! 🐙

#eval!
3628800 
fact: {a : Nat} → {ctx : Vec Ty a} → Expr ctx (Ty.int.fn Ty.int)
fact.
interp: {a : Nat} → {ctx : Vec Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → ty.interp
interp 
Env.nil: Env Vec.nil
Env.nil 
10: Ty.int.interp
10