for the few of us.

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 complicated than I expected. I do not remember where I have seen similar code before, but I believe the following code is more or less standard. It is recorded here for reference.

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 n Γ a represents a term enclosed in n surrrounding λ binders which, in the type context Γ, evaluates to a value having type a. Since we are about to use the de Bruin notation, the type context is simply a vector of types:

Cxt : ℕ -> Set1
Cxt n = Vec₁ Set n


It is a vector storing types, so I used Vec₁, a Set1 variation of Vec.

The typed term can then be defined by:

data Term (n : ℕ) (Γ : Cxt n) : Set -> Set1 where
   lit : ℕ -> Term n Γ ℕ
   var : (x : Fin n) -> Term n Γ (lookup x Γ)
   _·_ : forall {a b} -> Term n Γ (a -> b) -> Term n Γ a -> Term n Γ b
   add : Term n Γ ℕ -> Term n Γ ℕ -> Term n Γ ℕ
   λ : forall {a b} -> Term (suc n) (a ∷ Γ) b -> Term n Γ (a -> b)


The count of λ binders increments after each λ, while a (de Bruin) variable occuring in a term with n enclosing λ binders must be bounded by n. 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 : Set1) : ℕ -> Set1 where
   [] : Vec₁ a zero
   _∷_ : forall {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 : forall {a n} -> 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. Therefore, an environment is represented by a vector of type-value pairs:

Env : ℕ -> Set1
Env n = Vec₁ (Σ₁₀ Set (\a -> a)) n


where Σ₁₀ is a dependent pair whose first component is in Set1 while the second in Set. The two projection functions are proj₁₀₁ and proj₁₀₂.

Here is the evaluator:

eval : forall {a n} -> (ρ : Env n) -> Term n (map proj₁₀₁ ρ) a -> a
eval ρ (lit m) = m
eval ρ (var x) =
    ≡₁-subst (lookup-proj {_}{x}{ρ}) (proj₁₀₂ (lookup x ρ))
eval ρ (e₁ · e₂) = eval ρ e₁ (eval ρ e₂)
eval ρ (add e₁ e₂) = Data.Nat._+_ (eval ρ e₁) (eval ρ e₂)
eval ρ (λ e) = \v -> eval ((_ , v) ∷ ρ) e


The function evaluates a term having type a under the type context extracted from the environment ρ to a value of type a. In the case for var x we need a proof that the value extracted from the environment does have the expected type. For the proof we need such a lemma:

lookup-proj : forall {n} {x : Fin n} {ρ : Env n} ->
     proj₁₀₁ (lookup x ρ) ≡₁ lookup x (map proj₁₀₁ ρ)
lookup-proj {zero} {()} {_}
lookup-proj {suc n} {zero} {y ∷ _} = ≡₁-refl
lookup-proj {suc n} {suc fn} {_ ∷ xs} = lookup-proj {n} {fn} {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 : forall {a} -> a -> Term a
  _·_ : forall {a b} -> Term (a -> b) -> Term a -> Term b
  add : Term ℕ -> Term ℕ -> Term ℕ
  λ : forall {a b} -> (a -> Term b) -> Term (a -> b)

eval : forall {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.