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 Vector
is a list of size n
whose elements belong to a type α
.
inductive Vector: Type u → Nat → Type u
Vector (α: Type u
α : Type u: Type (u + 1)
Type u) : Nat: Type
Nat → Type u: Type (u + 1)
Type u
| nil: {α : Type u} → Vector α 0
nil : Vector: Type u → Nat → Type u
Vector α: Type u
α 0: Nat
0
| cons: {α : Type u} → {n : Nat} → α → Vector α n → Vector α (n + 1)
cons : α: Type u
α → Vector: Type u → Nat → Type u
Vector α: Type u
α n: Nat
n → Vector: Type u → Nat → Type u
Vector α: Type u
α (n: Nat
n+1: Nat
1)
We can overload the List.cons
notation ::
and use it to create Vector
s.
infix:67 " :: " => Vector.cons: {α : Type u} → {n : Nat} → α → Vector α n → Vector α (n + 1)
Vector.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 → Vector Ty n → Ty → Type
HasType : Fin: Nat → Type
Fin n: Nat
n → Vector: Type → Nat → Type
Vector Ty: Type
Ty n: Nat
n → Ty: Type
Ty → Type: Type 1
Type where
| stop: {ty : Ty} → {x : Nat} → {ctx : Vector Ty x} → HasType 0 (ty :: ctx) ty
stop : HasType: {n : Nat} → Fin n → Vector Ty n → Ty → Type
HasType 0: Fin (?m.2831 + 1)
0 (ty: Ty
ty :: ctx: Vector Ty ?m.2831
ctx) ty: Ty
ty
| pop: {x : Nat} → {k : Fin x} → {ctx : Vector Ty x} → {ty u : Ty} → HasType k ctx ty → HasType k.succ (u :: ctx) ty
pop : HasType: {n : Nat} → Fin n → Vector Ty n → Ty → Type
HasType k: Fin ?m.3021
k ctx: Vector Ty ?m.3021
ctx ty: Ty
ty → HasType: {n : Nat} → Fin n → Vector Ty n → Ty → Type
HasType k: Fin ?m.3021
k.succ: {n : Nat} → Fin n → Fin (n + 1)
succ (u: Ty
u :: ctx: Vector Ty ?m.3021
ctx) ty: Ty
ty
inductive Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr : Vector: Type → Nat → Type
Vector Ty: Type
Ty n: Nat
n → Ty: Type
Ty → Type: Type 1
Type where
| var: {n : Nat} → {i : Fin n} → {ctx : Vector Ty n} → {ty : Ty} → HasType i ctx ty → Expr ctx ty
var : HasType: {n : Nat} → Fin n → Vector Ty n → Ty → Type
HasType i: Fin ?m.3901
i ctx: Vector Ty ?m.3901
ctx ty: Ty
ty → Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr ctx: Vector Ty ?m.3901
ctx ty: Ty
ty
| val: {n : Nat} → {ctx : Vector Ty n} → Int → Expr ctx Ty.int
val : Int: Type
Int → Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr ctx: Vector Ty ?m.3922
ctx Ty.int: Ty
Ty.int
| lam: {n : Nat} → {a : Ty} → {ctx : Vector Ty n} → {ty : Ty} → Expr (a :: ctx) ty → Expr ctx (a.fn ty)
lam : Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr (a: Ty
a :: ctx: Vector Ty ?m.4086
ctx) ty: Ty
ty → Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr ctx: Vector Ty ?m.4086
ctx (Ty.fn: Ty → Ty → Ty
Ty.fn a: Ty
a ty: Ty
ty)
| app: {n : Nat} → {ctx : Vector Ty n} → {a ty : Ty} → Expr ctx (a.fn ty) → Expr ctx a → Expr ctx ty
app : Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr ctx: Vector Ty ?m.4241
ctx (Ty.fn: Ty → Ty → Ty
Ty.fn a: Ty
a ty: Ty
ty) → Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr ctx: Vector Ty ?m.4241
ctx a: Ty
a → Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr ctx: Vector Ty ?m.4241
ctx ty: Ty
ty
| op: {n : Nat} → {ctx : Vector 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} → Vector Ty n → Ty → Type
Expr ctx: Vector Ty ?m.4331
ctx a: Ty
a → Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr ctx: Vector Ty ?m.4331
ctx b: Ty
b → Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr ctx: Vector Ty ?m.4331
ctx c: Ty
c
| ife: {n : Nat} → {ctx : Vector Ty n} → {a : Ty} → Expr ctx Ty.bool → Expr ctx a → Expr ctx a → Expr ctx a
ife : Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr ctx: Vector Ty ?m.4452
ctx Ty.bool: Ty
Ty.bool → Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr ctx: Vector Ty ?m.4452
ctx a: Ty
a → Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr ctx: Vector Ty ?m.4452
ctx a: Ty
a → Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr ctx: Vector Ty ?m.4452
ctx a: Ty
a
| delay: {n : Nat} → {ctx : Vector Ty n} → {a : Ty} → (Unit → Expr ctx a) → Expr ctx a
delay : (Unit: Type
Unit → Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr ctx: Vector Ty ?m.4495
ctx a: Ty
a) → Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr ctx: Vector Ty ?m.4495
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 : Vector Ty x} → HasType 0 (ty :: ctx) ty
stop pop: {x : Nat} → {k : Fin x} → {ctx : Vector 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 n
th most recently defined variable is well-typed, so is the n+1
th.
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} → Vector Ty n → Type
Env : Vector: Type → Nat → Type
Vector Ty: Type
Ty n: Nat
n → Type: Type 1
Type where
| nil: Env Vector.nil
nil : Env: {n : Nat} → Vector Ty n → Type
Env Vector.nil: {α : Type} → Vector α 0
Vector.nil
| cons: {a : Ty} → {x : Nat} → {ctx : Vector Ty x} → a.interp → Env ctx → Env (a :: ctx)
cons : Ty.interp: Ty → Type
Ty.interp a: Ty
a → Env: {n : Nat} → Vector Ty n → Type
Env ctx: Vector Ty ?m.9291
ctx → Env: {n : Nat} → Vector Ty n → Type
Env (a: Ty
a :: ctx: Vector Ty ?m.9291
ctx)
infix:67 " :: " => Env.cons: {a : Ty} → {x : Nat} → {ctx : Vector Ty x} → a.interp → Env ctx → Env (a :: ctx)
Env.cons
def Env.lookup: {n : Nat} → {i : Fin n} → {ctx : Vector Ty n} → {ty : Ty} → HasType i ctx ty → Env ctx → ty.interp
Env.lookup : HasType: {n : Nat} → Fin n → Vector Ty n → Ty → Type
HasType i: Fin ?m.11901
i ctx: Vector Ty ?m.11901
ctx ty: Ty
ty → Env: {n : Nat} → Vector Ty n → Type
Env ctx: Vector Ty ?m.11901
ctx → ty: Ty
ty.interp: Ty → Type
interp
| stop: {ty : Ty} → {x : Nat} → {ctx : Vector 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 : Vector 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 : Vector 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 : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → ty.interp
Expr.interp (env: Env ctx
env : Env: {n : Nat} → Vector Ty n → Type
Env ctx: Vector Ty ?m.14768
ctx) : Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr ctx: Vector Ty ?m.14768
ctx ty: Ty
ty → ty: Ty
ty.interp: Ty → Type
interp
| var: {n : Nat} → {i : Fin n} → {ctx : Vector 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 : Vector Ty n} → {ty : Ty} → HasType i ctx ty → Env ctx → ty.interp
lookup i: HasType i✝ ctx ty
i
| val: {n : Nat} → {ctx : Vector Ty n} → Int → Expr ctx Ty.int
val x: Int
x => x: Int
x
| lam: {n : Nat} → {a : Ty} → {ctx : Vector 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 : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → ty.interp
interp (Env.cons: {a : Ty} → {x : Nat} → {ctx : Vector Ty x} → a.interp → Env ctx → Env (a :: ctx)
Env.cons x: a✝.interp
x env: Env ctx
env)
| app: {n : Nat} → {ctx : Vector 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 : Vector 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 : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → ty.interp
interp env: Env ctx
env)
| op: {n : Nat} → {ctx : Vector 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 : Vector 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 : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → ty.interp
interp env: Env ctx
env)
| ife: {n : Nat} → {ctx : Vector 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 : Vector 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 : Vector 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 : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → ty.interp
interp env: Env ctx
env
| delay: {n : Nat} → {ctx : Vector 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 : Vector 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.
defadd :add: {a : Nat} → {ctx : Vector Ty a} → Expr ctx (Ty.int.fn (Ty.int.fn Ty.int))ExprExpr: {n : Nat} → Vector Ty n → Ty → Typectx (ctx: Vector Ty ?m.18862Ty.fnTy.fn: Ty → Ty → TyTy.int (Ty.int: TyTy.fnTy.fn: Ty → Ty → TyTy.intTy.int: TyTy.int)) :=Ty.int: Tylam (lam: {n : Nat} → {a : Ty} → {ctx : Vector Ty n} → {ty : Ty} → Expr (a :: ctx) ty → Expr ctx (a.fn ty)lam (lam: {n : Nat} → {a : Ty} → {ctx : Vector Ty n} → {ty : Ty} → Expr (a :: ctx) ty → Expr ctx (a.fn ty)opop: {n : Nat} → {ctx : Vector Ty n} → {a b c : Ty} → (a.interp → b.interp → c.interp) → Expr ctx a → Expr ctx b → Expr ctx c(·+·) ((·+·): Ty.int.interp → Ty.int.interp → Ty.int.interpvarvar: {n : Nat} → {i : Fin n} → {ctx : Vector Ty n} → {ty : Ty} → HasType i ctx ty → Expr ctx tystop) (stop: {ty : Ty} → {x : Nat} → {ctx : Vector Ty x} → HasType 0 (ty :: ctx) tyvar (var: {n : Nat} → {i : Fin n} → {ctx : Vector Ty n} → {ty : Ty} → HasType i ctx ty → Expr ctx typoppop: {x : Nat} → {k : Fin x} → {ctx : Vector Ty x} → {ty u : Ty} → HasType k ctx ty → HasType k.succ (u :: ctx) tystop))))stop: {ty : Ty} → {x : Nat} → {ctx : Vector Ty x} → HasType 0 (ty :: ctx) tyadd.add: {a : Nat} → {ctx : Vector Ty a} → Expr ctx (Ty.int.fn (Ty.int.fn Ty.int))interpinterp: {a : Nat} → {ctx : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → ty.interpEnv.nilEnv.nil: Env Vector.nil1010: Ty.int.interp2020: Ty.int.interp
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:ExprExpr: {n : Nat} → Vector Ty n → Ty → Typectx (ctx: Vector Ty ?m.19272Ty.fnTy.fn: Ty → Ty → TyTy.intTy.int: TyTy.int) :=Ty.int: Tylam (lam: {n : Nat} → {a : Ty} → {ctx : Vector Ty n} → {ty : Ty} → Expr (a :: ctx) ty → Expr ctx (a.fn ty)ife (ife: {n : Nat} → {ctx : Vector Ty n} → {a : Ty} → Expr ctx Ty.bool → Expr ctx a → Expr ctx a → Expr ctx aopop: {n : Nat} → {ctx : Vector Ty n} → {a b c : Ty} → (a.interp → b.interp → c.interp) → Expr ctx a → Expr ctx b → Expr ctx c(·==·) ((·==·): Ty.int.interp → Ty.int.interp → Boolvarvar: {n : Nat} → {i : Fin n} → {ctx : Vector Ty n} → {ty : Ty} → HasType i ctx ty → Expr ctx tystop) (stop: {ty : Ty} → {x : Nat} → {ctx : Vector Ty x} → HasType 0 (ty :: ctx) tyvalval: {n : Nat} → {ctx : Vector Ty n} → Int → Expr ctx Ty.int0)) (0: Intvalval: {n : Nat} → {ctx : Vector Ty n} → Int → Expr ctx Ty.int1) (1: Intopop: {n : Nat} → {ctx : Vector Ty n} → {a b c : Ty} → (a.interp → b.interp → c.interp) → Expr ctx a → Expr ctx b → Expr ctx c(·*·) ((·*·): Ty.int.interp → Ty.int.interp → Ty.int.interpdelay fundelay: {n : Nat} → {ctx : Vector Ty n} → {a : Ty} → (Unit → Expr ctx a) → Expr ctx a_ =>_: Unitappapp: {n : Nat} → {ctx : Vector Ty n} → {a ty : Ty} → Expr ctx (a.fn ty) → Expr ctx a → Expr ctx tyfact (fact: {a : Nat} → {ctx : Vector Ty a} → Expr ctx (Ty.int.fn Ty.int)opop: {n : Nat} → {ctx : Vector Ty n} → {a b c : Ty} → (a.interp → b.interp → c.interp) → Expr ctx a → Expr ctx b → Expr ctx c(·-·) ((·-·): Ty.int.interp → Ty.int.interp → Ty.int.interpvarvar: {n : Nat} → {i : Fin n} → {ctx : Vector Ty n} → {ty : Ty} → HasType i ctx ty → Expr ctx tystop) (stop: {ty : Ty} → {x : Nat} → {ctx : Vector Ty x} → HasType 0 (ty :: ctx) tyvalval: {n : Nat} → {ctx : Vector Ty n} → Int → Expr ctx Ty.int1))) (1: Intvarvar: {n : Nat} → {i : Fin n} → {ctx : Vector Ty n} → {ty : Ty} → HasType i ctx ty → Expr ctx tystop)))stop: {ty : Ty} → {x : Nat} → {ctx : Vector Ty x} → HasType 0 (ty :: ctx) tya✝: Nat
ctx: Vector Ty a✝a✝ + 1 < a✝Goals accomplished! 🐙fact.fact: {a : Nat} → {ctx : Vector Ty a} → Expr ctx (Ty.int.fn Ty.int)interpinterp: {a : Nat} → {ctx : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → ty.interpEnv.nilEnv.nil: Env Vector.nil1010: Ty.int.interp