# 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 uVector (α: Type uα : Type u: Type (u + 1)Type u) : Nat: TypeNat → Type u: Type (u + 1)Type u
| nil: {α : Type u} → Vector α 0nil : Vector: Type u → Nat → Type uVector α: Type uα 0: Nat0
| cons: {α : Type u} → {n : Nat} → α → Vector α n → Vector α (n + 1)cons : α: Type uα → Vector: Type u → Nat → Type uVector α: Type uα n: Natn → Vector: Type u → Nat → Type uVector α: Type uα (n: Natn+1: Nat1)```

We can overload the `List.cons` notation `::` and use it to create `Vector`s.

`infix:67 " :: " => Vector.cons`

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

```inductive Ty: TypeTy where
| int: Tyint
| bool: Tybool
| fn: Ty → Ty → Tyfn (a: Tya r: Tyr : Ty: TypeTy)```

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 → TypeTy.interp : Ty: TypeTy → Type: Type 1Type
| int: Tyint    => Int: TypeInt
| bool: Tybool   => Bool: TypeBool
| fn: Ty → Ty → Tyfn a: Tya r: Tyr => a: Tya.interp: Ty → Typeinterp → r: Tyr.interp: Ty → Typeinterp```

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 → TypeHasType : Fin: Nat → TypeFin n: Natn → Vector: Type → Nat → TypeVector Ty: TypeTy n: Natn → Ty: TypeTy → Type: Type 1Type where
| stop: {ty : Ty} → {x : Nat} → {ctx : Vector Ty x} → HasType 0 (ty :: ctx) tystop : HasType: {n : Nat} → Fin n → Vector Ty n → Ty → TypeHasType 0: Fin (?m.2009 + 1)0 (ty: Tyty :: ctx: Vector Ty ?m.2009ctx) ty: Tyty
| pop: {x : Nat} → {k : Fin x} → {ctx : Vector Ty x} → {ty u : Ty} → HasType k ctx ty → HasType (Fin.succ k) (u :: ctx) typop  : HasType: {n : Nat} → Fin n → Vector Ty n → Ty → TypeHasType k: Fin ?m.2129k ctx: Vector Ty ?m.2129ctx ty: Tyty → HasType: {n : Nat} → Fin n → Vector Ty n → Ty → TypeHasType k: Fin ?m.2129k.succ: {n : Nat} → Fin n → Fin (Nat.succ n)succ (u: Tyu :: ctx: Vector Ty ?m.2129ctx) ty: Tyty

inductive Expr: {n : Nat} → Vector Ty n → Ty → TypeExpr : Vector: Type → Nat → TypeVector Ty: TypeTy n: Natn → Ty: TypeTy → Type: Type 1Type where
| var: {n : Nat} → {i : Fin n} → {ctx : Vector Ty n} → {ty : Ty} → HasType i ctx ty → Expr ctx tyvar   : HasType: {n : Nat} → Fin n → Vector Ty n → Ty → TypeHasType i: Fin ?m.2969i ctx: Vector Ty ?m.2969ctx ty: Tyty → Expr: {n : Nat} → Vector Ty n → Ty → TypeExpr ctx: Vector Ty ?m.2969ctx ty: Tyty
| val: {n : Nat} → {ctx : Vector Ty n} → Int → Expr ctx Ty.intval   : Int: TypeInt → Expr: {n : Nat} → Vector Ty n → Ty → TypeExpr ctx: Vector Ty ?m.2990ctx Ty.int: TyTy.int
| lam: {n : Nat} → {a : Ty} → {ctx : Vector Ty n} → {ty : Ty} → Expr (a :: ctx) ty → Expr ctx (Ty.fn a ty)lam   : Expr: {n : Nat} → Vector Ty n → Ty → TypeExpr (a: Tya :: ctx: Vector Ty ?m.3087ctx) ty: Tyty → Expr: {n : Nat} → Vector Ty n → Ty → TypeExpr ctx: Vector Ty ?m.3087ctx (Ty.fn: Ty → Ty → TyTy.fn a: Tya ty: Tyty)
| app: {n : Nat} → {ctx : Vector Ty n} → {a ty : Ty} → Expr ctx (Ty.fn a ty) → Expr ctx a → Expr ctx tyapp   : Expr: {n : Nat} → Vector Ty n → Ty → TypeExpr ctx: Vector Ty ?m.3176ctx (Ty.fn: Ty → Ty → TyTy.fn a: Tya ty: Tyty) → Expr: {n : Nat} → Vector Ty n → Ty → TypeExpr ctx: Vector Ty ?m.3176ctx a: Tya → Expr: {n : Nat} → Vector Ty n → Ty → TypeExpr ctx: Vector Ty ?m.3176ctx ty: Tyty
| op: {n : Nat} →
{ctx : Vector Ty n} → {a b c : Ty} → (Ty.interp a → Ty.interp b → Ty.interp c) → Expr ctx a → Expr ctx b → Expr ctx cop    : (a: Tya.interp: Ty → Typeinterp → b: Tyb.interp: Ty → Typeinterp → c: Tyc.interp: Ty → Typeinterp) → Expr: {n : Nat} → Vector Ty n → Ty → TypeExpr ctx: Vector Ty ?m.3266ctx a: Tya → Expr: {n : Nat} → Vector Ty n → Ty → TypeExpr ctx: Vector Ty ?m.3266ctx b: Tyb → Expr: {n : Nat} → Vector Ty n → Ty → TypeExpr ctx: Vector Ty ?m.3266ctx c: Tyc
| ife: {n : Nat} → {ctx : Vector Ty n} → {a : Ty} → Expr ctx Ty.bool → Expr ctx a → Expr ctx a → Expr ctx aife   : Expr: {n : Nat} → Vector Ty n → Ty → TypeExpr ctx: Vector Ty ?m.3387ctx Ty.bool: TyTy.bool → Expr: {n : Nat} → Vector Ty n → Ty → TypeExpr ctx: Vector Ty ?m.3387ctx a: Tya → Expr: {n : Nat} → Vector Ty n → Ty → TypeExpr ctx: Vector Ty ?m.3387ctx a: Tya → Expr: {n : Nat} → Vector Ty n → Ty → TypeExpr ctx: Vector Ty ?m.3387ctx a: Tya
| delay: {n : Nat} → {ctx : Vector Ty n} → {a : Ty} → (Unit → Expr ctx a) → Expr ctx adelay : (Unit: TypeUnit → Expr: {n : Nat} → Vector Ty n → Ty → TypeExpr ctx: Vector Ty ?m.3430ctx a: Tya) → Expr: {n : Nat} → Vector Ty n → Ty → TypeExpr ctx: Vector Ty ?m.3430ctx a: Tya```

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

`open HasType (stop 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 ot 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 → TypeEnv : Vector: Type → Nat → TypeVector Ty: TypeTy n: Natn → Type: Type 1Type where
| nil: Env Vector.nilnil  : Env: {n : Nat} → Vector Ty n → TypeEnv Vector.nil: {α : Type} → Vector α 0Vector.nil
| cons: {a : Ty} → {x : Nat} → {ctx : Vector Ty x} → Ty.interp a → Env ctx → Env (a :: ctx)cons : Ty.interp: Ty → TypeTy.interp a: Tya → Env: {n : Nat} → Vector Ty n → TypeEnv ctx: Vector Ty ?m.7942ctx → Env: {n : Nat} → Vector Ty n → TypeEnv (a: Tya :: ctx: Vector Ty ?m.7942ctx)

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

def Env.lookup: {n : Nat} → {i : Fin n} → {ctx : Vector Ty n} → {ty : Ty} → HasType i ctx ty → Env ctx → Ty.interp tyEnv.lookup : HasType: {n : Nat} → Fin n → Vector Ty n → Ty → TypeHasType i: Fin ?m.9720i ctx: Vector Ty ?m.9720ctx ty: Tyty → Env: {n : Nat} → Vector Ty n → TypeEnv ctx: Vector Ty ?m.9720ctx → ty: Tyty.interp: Ty → Typeinterp
| stop: {ty : Ty} → {x : Nat} → {ctx : Vector Ty x} → HasType 0 (ty :: ctx) tystop,  x: Ty.interp tyx :: xs: Env ctx✝xsWarning: unused variable `xs` => x: Ty.interp tyx
| pop: {x : Nat} → {k : Fin x} → {ctx : Vector Ty x} → {ty u : Ty} → HasType k ctx ty → HasType (Fin.succ k) (u :: ctx) typop k: HasType k✝ ctx✝ tyk, x: Ty.interp u✝xWarning: unused variable `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 tylookup k: HasType k✝ ctx✝ tyk 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 tyExpr.interp (env: Env ctxenv : Env: {n : Nat} → Vector Ty n → TypeEnv ctx: Vector Ty ?m.12558ctx) : Expr: {n : Nat} → Vector Ty n → Ty → TypeExpr ctx: Vector Ty ?m.12558ctx ty: Tyty → ty: Tyty.interp: Ty → Typeinterp
| var: {n : Nat} → {i : Fin n} → {ctx : Vector Ty n} → {ty : Ty} → HasType i ctx ty → Expr ctx tyvar i: HasType i✝ ctx tyi     => env: Env ctxenv.lookup: {n : Nat} → {i : Fin n} → {ctx : Vector Ty n} → {ty : Ty} → HasType i ctx ty → Env ctx → Ty.interp tylookup i: HasType i✝ ctx tyi
| val: {n : Nat} → {ctx : Vector Ty n} → Int → Expr ctx Ty.intval x: Intx     => x: Intx
| lam: {n : Nat} → {a : Ty} → {ctx : Vector Ty n} → {ty : Ty} → Expr (a :: ctx) ty → Expr ctx (Ty.fn a ty)lam b: Expr (a✝ :: ctx) ty✝b     => fun x: Ty.interp a✝x => b: Expr (a✝ :: ctx) ty✝b.interp: {a : Nat} → {ctx : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → Ty.interp tyinterp (Env.cons: {a : Ty} → {x : Nat} → {ctx : Vector Ty x} → Ty.interp a → Env ctx → Env (a :: ctx)Env.cons x: Ty.interp a✝x env: Env ctxenv)
| app: {n : Nat} → {ctx : Vector Ty n} → {a ty : Ty} → Expr ctx (Ty.fn a ty) → Expr ctx a → Expr ctx tyapp f: Expr ctx (Ty.fn a✝ ty)f a: Expr ctx a✝a   => f: Expr ctx (Ty.fn a✝ ty)f.interp: {a : Nat} → {ctx : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → Ty.interp tyinterp env: Env ctxenv (a: Expr ctx a✝a.interp: {a : Nat} → {ctx : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → Ty.interp tyinterp env: Env ctxenv)
| op: {n : Nat} →
{ctx : Vector Ty n} → {a b c : Ty} → (Ty.interp a → Ty.interp b → Ty.interp c) → Expr ctx a → Expr ctx b → Expr ctx cop o: Ty.interp a✝ → Ty.interp b✝ → Ty.interp tyo x: Expr ctx a✝x y: Expr ctx b✝y  => o: Ty.interp a✝ → Ty.interp b✝ → Ty.interp tyo (x: Expr ctx a✝x.interp: {a : Nat} → {ctx : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → Ty.interp tyinterp env: Env ctxenv) (y: Expr ctx b✝y.interp: {a : Nat} → {ctx : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → Ty.interp tyinterp env: Env ctxenv)
| ife: {n : Nat} → {ctx : Vector Ty n} → {a : Ty} → Expr ctx Ty.bool → Expr ctx a → Expr ctx a → Expr ctx aife c: Expr ctx Ty.boolc t: Expr ctx tyt e: Expr ctx tye => if c: Expr ctx Ty.boolc.interp: {a : Nat} → {ctx : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → Ty.interp tyinterp env: Env ctxenv then t: Expr ctx tyt.interp: {a : Nat} → {ctx : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → Ty.interp tyinterp env: Env ctxenv else e: Expr ctx tye.interp: {a : Nat} → {ctx : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → Ty.interp tyinterp env: Env ctxenv
| delay: {n : Nat} → {ctx : Vector Ty n} → {a : Ty} → (Unit → Expr ctx a) → Expr ctx adelay a: Unit → Expr ctx tya   => (a: Unit → Expr ctx tya (): Unit()).interp: {a : Nat} → {ctx : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → Ty.interp tyinterp env: Env ctxenv

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 : Vector Ty a} → Expr ctx (Ty.fn Ty.int (Ty.fn Ty.int Ty.int))add : Expr: {n : Nat} → Vector Ty n → Ty → TypeExpr ctx: Vector Ty ?m.16786ctx (Ty.fn: Ty → Ty → TyTy.fn Ty.int: TyTy.int (Ty.fn: Ty → Ty → TyTy.fn Ty.int: TyTy.int Ty.int: TyTy.int)) :=
lam: {n : Nat} → {a : Ty} → {ctx : Vector Ty n} → {ty : Ty} → Expr (a :: ctx) ty → Expr ctx (Ty.fn a ty)lam (lam: {n : Nat} → {a : Ty} → {ctx : Vector Ty n} → {ty : Ty} → Expr (a :: ctx) ty → Expr ctx (Ty.fn a ty)lam (op: {n : Nat} →
{ctx : Vector Ty n} → {a b c : Ty} → (Ty.interp a → Ty.interp b → Ty.interp c) → Expr ctx a → Expr ctx b → Expr ctx cop (·+·): Ty.interp Ty.int → Ty.interp Ty.int → Ty.interp Ty.int(·+·) (var: {n : Nat} → {i : Fin n} → {ctx : Vector Ty n} → {ty : Ty} → HasType i ctx ty → Expr ctx tyvar stop: {ty : Ty} → {x : Nat} → {ctx : Vector Ty x} → HasType 0 (ty :: ctx) tystop) (var: {n : Nat} → {i : Fin n} → {ctx : Vector Ty n} → {ty : Ty} → HasType i ctx ty → Expr ctx tyvar (pop: {x : Nat} → {k : Fin x} → {ctx : Vector Ty x} → {ty u : Ty} → HasType k ctx ty → HasType (Fin.succ k) (u :: ctx) typop stop: {ty : Ty} → {x : Nat} → {ctx : Vector Ty x} → HasType 0 (ty :: ctx) tystop))))

#eval30
add: {a : Nat} → {ctx : Vector Ty a} → Expr ctx (Ty.fn Ty.int (Ty.fn Ty.int Ty.int))add.interp: {a : Nat} → {ctx : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → Ty.interp tyinterp Env.nil: Env Vector.nilEnv.nil 10: Ty.interp Ty.int10 20: Ty.interp Ty.int20```

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 viwed as "trust me, this recursive definition makes sense". Recall that `sorry` is an unsound axiom in Lean.

```def fact: {a : Nat} → {ctx : Vector Ty a} → Expr ctx (Ty.fn Ty.int Ty.int)factWarning: declaration uses 'sorry' : Expr: {n : Nat} → Vector Ty n → Ty → TypeExpr ctx: Vector Ty ?m.17172ctx (Ty.fn: Ty → Ty → TyTy.fn Ty.int: TyTy.int Ty.int: TyTy.int) :=
lam: {n : Nat} → {a : Ty} → {ctx : Vector Ty n} → {ty : Ty} → Expr (a :: ctx) ty → Expr ctx (Ty.fn a ty)lam (ife: {n : Nat} → {ctx : Vector Ty n} → {a : Ty} → Expr ctx Ty.bool → Expr ctx a → Expr ctx a → Expr ctx aife (op: {n : Nat} →
{ctx : Vector Ty n} → {a b c : Ty} → (Ty.interp a → Ty.interp b → Ty.interp c) → Expr ctx a → Expr ctx b → Expr ctx cop (·==·): Ty.interp Ty.int → Ty.interp Ty.int → Bool(·==·) (var: {n : Nat} → {i : Fin n} → {ctx : Vector Ty n} → {ty : Ty} → HasType i ctx ty → Expr ctx tyvar stop: {ty : Ty} → {x : Nat} → {ctx : Vector Ty x} → HasType 0 (ty :: ctx) tystop) (val: {n : Nat} → {ctx : Vector Ty n} → Int → Expr ctx Ty.intval 0: Int0))
(val: {n : Nat} → {ctx : Vector Ty n} → Int → Expr ctx Ty.intval 1: Int1)
(op: {n : Nat} →
{ctx : Vector Ty n} → {a b c : Ty} → (Ty.interp a → Ty.interp b → Ty.interp c) → Expr ctx a → Expr ctx b → Expr ctx cop (·*·): Ty.interp Ty.int → Ty.interp Ty.int → Ty.interp Ty.int(·*·) (delay: {n : Nat} → {ctx : Vector Ty n} → {a : Ty} → (Unit → Expr ctx a) → Expr ctx adelay fun _: Type_ => app: {n : Nat} → {ctx : Vector Ty n} → {a ty : Ty} → Expr ctx (Ty.fn a ty) → Expr ctx a → Expr ctx tyapp fact: {a : Nat} → {ctx : Vector Ty a} → Expr ctx (Ty.fn Ty.int Ty.int)fact (op: {n : Nat} →
{ctx : Vector Ty n} → {a b c : Ty} → (Ty.interp a → Ty.interp b → Ty.interp c) → Expr ctx a → Expr ctx b → Expr ctx cop (·-·): Ty.interp Ty.int → Ty.interp Ty.int → Ty.interp Ty.int(·-·) (var: {n : Nat} → {i : Fin n} → {ctx : Vector Ty n} → {ty : Ty} → HasType i ctx ty → Expr ctx tyvar stop: {ty : Ty} → {x : Nat} → {ctx : Vector Ty x} → HasType 0 (ty :: ctx) tystop) (val: {n : Nat} → {ctx : Vector Ty n} → Int → Expr ctx Ty.intval 1: Int1))) (var: {n : Nat} → {i : Fin n} → {ctx : Vector Ty n} → {ty : Ty} → HasType i ctx ty → Expr ctx tyvar stop: {ty : Ty} → {x : Nat} → {ctx : Vector Ty x} → HasType 0 (ty :: ctx) tystop)))
decreasing_by sorryGoals accomplished! 🐙

#eval3628800
fact: {a : Nat} → {ctx : Vector Ty a} → Expr ctx (Ty.fn Ty.int Ty.int)fact.interp: {a : Nat} → {ctx : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → Ty.interp tyinterp Env.nil: Env Vector.nilEnv.nil 10: Ty.interp Ty.int10```