Typed λ Calculus Interpreter in Agda

Update (Oct. 5, 2010): updated the code to use the current version of Standard Library (with universe polymorphism); index the environment by typing context.

It has been a typical exercise for beginners to write an evaluator for some variation of λ calculus. In a recent meeting I talked to my assistants about using dependent type to guarantee that, in an evaluator for λ calculus using de Bruin indices, that variable look-up always succeeds. The basic idea is to represent the environment using the Vec datatype, and label each λ terms with the number of enclosing λ’s, which must match the length of the environment.

I thought it could also be an easy exercsie for them to write up such an evaluator. Yet again, things turned out to be just a little bit more harder than I expected, thus I am recording the code here for reference. I do not remember where I have seen similar code before, but I believe the following is more or less standard.

Evaluating Simply-Typed λ Calculus

Take simply-typed λ calculus with natural numbers as the only base type. It is common in Haskell to use such a tagged value type:

data Val = Num Int | Fun (Val -> Val)


However, Val is not a legistimate type in Agda, since recursion occurs in negative position in the case of Fun. Indeed, Val -> Val is a “larger” type than Val, and we would need a more complicated semantics to accommodate the former into the latter.

Oleg Kiselyov suggested defunctionalising Val. For example, represent the value as either

data Val = Num Int | Closure [Val] Term


or

data Val n = Num n Int | Closure [Val m] (Val (n+1))


I may try these alternatives later. At the time when I wrote the code, the right thing to do seemed to be switching to a tagless representation for values and integrate type checking into the term type.

The type Term Γ a represents a term that, in the typing context Γ, evaluates to a value having type a. Since we are about to use the de Bruin notation, the typing context is simply a vector of types:

Cxt : ℕ → Set1
Cxt n = Vec Set n


Note that it is a vector storing types (in Set1) rather than values (in Set). Before Agda introduced universe polymorphism, one would have to use Vec₁, a Set1 variation of Vec.

The type Term Γ a can then be defined by:

data Term {n : ℕ} (Γ : Cxt n) : Set → Set1 where
   lit : ℕ → Term Γ ℕ
   var : (x : Fin n) → Term Γ (lookup x Γ)
   _·_ : ∀ {a b} → Term Γ (a → b) → Term Γ a → Term Γ b
   add : Term Γ ℕ → Term Γ ℕ → Term Γ ℕ
   ƛ : ∀ {a b} → Term (a ∷ Γ) b → Term Γ (a → b)


The type Fin n denotes natural numbers between 0 and n-1. Notice that in a (de Bruin) variable var x, the value of x is bounded by n, the length of the typing context. The lookup function is thus guaranteed to success. The typing context is extended with one more element within each ƛ. The type Vec, its look-up function, and the type Fin for bounded natural numbers, are all defined in the standard library:

data Vec {a} (A : Set a) : ℕ → Set a where
   [] : Vec A zero
   _∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n)

data Fin : ℕ → Set where
   zero : {n : ℕ} → Fin (suc n)
   suc : {n : ℕ} (i : Fin n) → Fin (suc n)

lookup : ∀ {a n} {A : Set a} → Fin n → Vec A n → A
lookup zero (x ∷ xs) = x
lookup (suc i) (x ∷ xs) = lookup i xs


Now the evaluator. We need an environment allowing us to store heterogeneous values. One possibility is to index the environment by typing contexts: given a typing context Γ of length n, Env Γ is essentially a vector of n values whose types match those in Γ:

data Env : {n : ℕ} → Cxt n → Set1 where
   [] : Env []
   _∷_ : ∀ {a n} {Γ : Cxt n} → a → Env Γ → Env (a ∷ Γ)


Agda allows us to reuse the constructors [] and _∷_. For an example, 0 ∷ 1 ∷ (λ v → suc v) ∷ [] may have type Env (ℕ ∷ ℕ ∷ (ℕ → ℕ) ∷ []).

We also need a function that looks up an environment:

envLookup : ∀ {n}{Γ : Cxt n} → (i : Fin n) → Env Γ → lookup i Γ
envLookup zero (v ∷ ρ) = v
envLookup (suc n) (v ∷ ρ) = envLookup n ρ


Notice the resulting type lookup i Γ — the type of the ith element in an environment is the ith type in the typing context.

With the setting up, the evaluator looks rather standard:

eval : ∀ {a n} {Γ : Cxt n} → (ρ : Env Γ) → Term Γ a → a
eval ρ (lit m) = m
eval ρ (var x) = envLookup x ρ
eval ρ (e₁ · e₂) = (eval ρ e₁) (eval ρ e₂)
eval ρ (add e₁ e₂) = (eval ρ e₁) + (eval ρ e₂)
eval ρ (ƛ e) = λ v → eval (v ∷ ρ) e


An Environment as a Vector of Type-Value Pairs

In my earlier attempt I tried to reuse the Vec type for the environment as well. After all, an environment can be seen as a list of (type, value) pairs:

Env : ℕ → Set1
Env n = Vec (Σ Set (λ a → a)) n


where Σ is a pair where the type of its second component may depend on the first. The two projection functions of a pair are respectively proj₁ and proj₂. In Σ Set (λ a → a), the type of the second component is exactly the first, that is, we may have environments like ρ = (ℕ , 0) ∷ (ℕ , 1) ∷ (ℕ → ℕ , (λ v → suc v)) ∷ []. To extract the ith value, we simply apply proj₂ (lookup i ρ), which by the definition of Σ has type proj₁ (lookup i ρ). Applying map proj₁ to ρ gives us the “typing context” Env (ℕ ∷ ℕ ∷ (ℕ → ℕ) ∷ []). The eval function now has type:

eval : ∀ {a n} → (ρ : Env n) → Term (map proj₁ ρ) a → a

In dependently typed programming, however, it is not always easy to reuse general purpose datatypes. In this case, the price for reusing Vec and lookup is an additional proof obligation in the var x case of eval:

eval : ∀ {a n} → (ρ : Env n) → Term (map proj₁ ρ) a → a
eval ρ (lit m) = m
eval ρ (var x) rewrite lookup-proj x ρ = proj₂ (lookup x ρ)
eval ρ (e₁ · e₂) = eval ρ e₁ (eval ρ e₂)
eval ρ (add e₁ e₂) = (eval ρ e₁) + (eval ρ e₂)
eval ρ (ƛ e) = λ v → eval ((_ , v) ∷ ρ) e


The reason is that the right-hand side, proj₂ (lookup x ρ), has type proj₁ (lookup x ρ), while the type checker, having just matched the var constructor, expects something having type lookup x (map proj₁ ρ). We thus have to convince Agda that they are actually the same type:

lookup-proj : ∀ {n} (x : Fin n) (ρ : Env n) →
     lookup x (map proj₁ ρ) ≡ proj₁ (lookup x ρ)
lookup-proj zero (_ ∷ _) = refl
lookup-proj (suc i) (_ ∷ xs) = lookup-proj i xs


Higher-Order Abstract Syntax

My original purpose was to demonstrate the use of vectors to guarantee static properties. If we decide not to use de Bruin notation and switch to higher-order abstract syntax instead, we could have a much simpler evaluator:

data Term : Set → Set1 where
  lit : ℕ → Term ℕ
  var : ∀ {a} → a → Term a
  _·_ : ∀ {a b} → Term (a → b) → Term a → Term b
  add : Term ℕ → Term ℕ → Term ℕ
  ƛ : ∀ {a b} → (a → Term b) → Term (a → b)

eval : ∀ {a} → Term a → a
eval (lit n) = n
eval (var v) = v
eval (e₁ · e₂) = eval e₁ (eval e₂)
eval (add e₁ e₂) = eval e₁ + eval e₂
eval (ƛ e) = λ x → eval (e x)


It is a bit odd to me that var and lit are actually the same thing. Nothing forbids you from writing λ(\x -> lit x) or λ(\x -> var 3).

Further Reading

Oleg Kiselyov has written a lot on typed tagless interpreters. Besides the initial representation above, there is a dual final representation. The purpose is to experiment with staged interpreters. Their paper Finally Tagless, Partial Evaluated: Tagless Staged Interpreters for Simpler Typed Languages is a good read which I would recommend to people.

Code

• Eval.agda: an early version, using Vec for the environment.
• Eval2.agda: using higher-order abstract syntax.
• Eval3.agda: the code presented in the main text of this post.