# 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 `i`th element in an environment is the `i`th 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 `i`th 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.

# S Combinator is Injective, with Proofs

By chance, I came upon a blog entry by Masahiro Sakai (酒井政裕) in which he, after reading my short comment on my previous homepage “Do you know that the `S` combinator is injective? I have a simple algebraic proof!”, tried to construct the inverse of `S` and showed that `S⁻¹ ○ S = id` in, guess what, Agda!

Wow, people were actually reading what I wrote! This made me feel that I have to be a bit more responsible and, at least, provide the proof when I claim I have one. So, here it is.

### S is injective

Recall the definition of `S`:

``````
S : (A -> B -> C) -> (A -> B) -> A -> C
S = λ x y a -> x a (y a)
``````

I am assuming a simple semantics of sets and functions, and by `S` being injective I mean that `S x = S x' ⇒ x = x'`, which can be trivially shown below:

``````
S x = S x'
≡       { η expansion, for all y : A -> B, a : A }
(∀ a, y : S x y a = S x' y a)
≡       { definition of S }
(∀ a, y : x a (y a) = x' a (y a))
⇒       { choose y = K b for some b }
(∀ a, b : x a (K b a) = x' a (K b a))
≡       { definition of K: K b a = b }
(∀ a, b : x a b = x' a b)
≡       { pointwise equality }
x = x'
``````

I would usually leave out the `∀`‘s in derivations, but in this case, they are explicitly written to emphasise that `b` is indeed universally quantified.

### So, what is the inverse of S?

Now that we know `S` is injective, there ought to exist some function `S⁻¹` such that `S⁻¹ ○ S = id`. Nakano san claimed that a definition would be:

``````
S⁻¹ : ((A -> B) -> A -> C) -> A -> B -> C
S⁻¹ = λ x a b -> x (K b) a
``````

That `S⁻¹ ○ S = id` is easy to see:

``````
S⁻¹ (S x) a b
=  (S x) (K b) a
=  x a (K b a)
=  x a b
``````

From another direction, we have only `S ○ S⁻¹ ⊆ id` since `S` is not a surjective function. How the range of `S` look like? Inspecting the definition of `S`. Since `y` is applied only once to `a`, the value of `y` on other input does not matter. That is, the range of `S` consists of only functions `e` such that:

``````
e y a = e y' a     for all y, y' such that y a = y' a      ......(1)
``````

We will show that `S (S⁻¹ e) = e` for all `e` satisfying (1):

``````
S (S⁻¹ e) y a
=      { definition of S }
S⁻¹ e a (y a)
=      { definition of S⁻¹ }
e (K (y a)) a
=      { by (1), since K (y a) a = y a }
e y a
``````

### Inverting higher-order functions?

Some endnotes. Once Nakano and I thought we discovered how to invert higher-order functions (and even derive the necessary side conditions, like the one on `e` above) by drawing λ expressions as trees and manipulating them. It turned out that I overlooked something obvious in the very beginning and the result was a disaster.

Does anyone know of some related work on inverting higher order functions? The only one I know is Samson Abramsky’s paper A Structural Approach to Reversible Computation, but I am not sure whether it is about reversibility/invertibility in the same sense.

# Encoding Inductive and Coinductive Types in Polymorphic Lambda Calculus

This was written about two years ago. Mostly inspired by Philip Wadler‘s note Recursive types for free.

### Inductive types

Inductive types are least fixed-points. An indcutive type μF is simulated by

`` forall x . (F x -> x) -> x``

In Haskell, we need a constructor to wrap a “forall” quantifier.

``````> newtype LFix f = LF (forall x. (f x -> x) -> x)
> instance Show (LFix f) where
>   show _ = ""

> foldL :: Functor f => (f x -> x) -> LFix f -> x
> foldL f (LF x) = x f

> inL :: Functor f => f (LFix f) -> LFix f
> inL fx = LF (\\f -> f . fmap (foldL f) \$ fx)

> outL :: Functor f => LFix f -> f (LFix f)
> outL = foldL (fmap inL)
``````

Example: lists.

``````> data F a x = L | R a x deriving Show
> instance Functor (F a) where
>   fmap f L = L
>   fmap f (R a x) = R a (f x)

> type ListL a = LFix (F a)
``````

A `ListL` can only be constructed out of nil and cons.

``````    Main> consL 1 (consL 2 (consL 3 nilL))

``````
``````> nilL = inL L
> consL a x = inL (R a x)
``````

We can convert a ListL to a ‘real’ Haskell list.

``````
Main> lList \$ consL 1 (consL 2 (consL 3 nilL))
[1,2,3]
``````
``````> lList :: LFix (F a) -> [a]
> lList = foldL ll
>   where ll L = []
>         ll (R a x) = a : x
``````

However, a `ListL` has to be explicitly built, so there is no infinite `ListL`.

### Coinductive types

A coinductive type νF is simulatd by

`````` exists x . (x -> F x, x)
``````

We represent it in Haskell using the property `exists x . F x == forall y . (forall x . F x -> y) -> y`:

``````> data GFix f = forall x . GF (x -> f x, x)
> instance Show (GFix f) where
>   show _ = ""

> unfoldG :: Functor f => (x -> f x) -> x -> GFix f
> unfoldG g x = GF (g,x)

> outG :: Functor f => GFix f -> f (GFix f)
> outG (GF (g,x)) = fmap (unfoldG g) . g \$ x

> inG :: Functor f => f (GFix f) -> GFix f
> inG = unfoldG (fmap outG)
``````

Example:

``````> type ListG a = GFix (F a)
``````

`ListG` can be constructed out of `nil` and `cons`, as well as an unfold.

``````> nilG = inG L
> consG a x = inG (R a x)

> fromG :: Int -> ListG Int
> fromG m = unfoldG ft m
>    where ft m = R m (m+1)
``````

However, one can perform only a finite number of outG.

``````  Main> fmap outG . outG . fromG \$ 1
R 1 (R 2 )
``````

### Isomorphism

The function `force` witnesses the isomorphism between `LFix` and `GFix`.

``````> force :: Functor f => GFix f -> LFix f
> force = inL . fmap force . outG     -- recursion!
``````

If `LFix` and `GFix` are isomorphic, we are allowed to build hylomorphisms:

``````> fromTo :: Int -> Int -> LFix (F Int)
> fromTo m n = takeLessThan n . force . fromG \$ m

> takeLessThan :: Int -> LFix (F Int) -> LFix (F Int)
> takeLessThan n = foldL (tlt n)
>   where tlt n L = nilL
>         tlt n (R m x) | n <= m = nilL
>                       | otherwise = consL m x

Main> lList (fromTo 1 10)
[1,2,3,4,5,6,7,8,9]
``````

However, `force` has to be defined using general recursion. The price is that it is now possible to write programs that do not terminate.

# Substraction not Definable in Simply Typed Lambda Calculus

I probably wrote this a couple of years ago when I was studying polymorphic types.

What happens if we have only monomorphic type when we define church numerals? Let us represent church numerals by the type `(a -> a) -> a -> a` for some monomorphic `a`:

``````> import Prelude hiding (succ, pred)

> type N a = (a -> a) -> a -> a``````

Zero and successor can still be defined. Their values do not matter.

``````> zero :: N a
> zero = error ""

> succ :: N a -> N a
> succ = error ""``````

Also assume we have pairs predefined:

``> pair a b = (a,b)``

We can even define primitive recursion, only that it does not have the desired type:

``  primrec :: (N -> b -> b) -> b -> N -> b``

Instead we get the type below:

``````> primrec :: (N a -> b -> b) -> b -> N (N a, b) -> b
> primrec f c n =
>   snd (n (\z -> pair (succ (fst z))
>                      (f (fst z) (snd z)))
>          (pair zero c))``````

Therefore, predecessor does not get the type ```pred :: N a -> N a ``` we want. Instead we have:

``````> pred :: N (N a, N a) -> N a
> pred = primrec (\n m -> n) zero``````

# S Combinator is Injective

Do you know that the S combinator is injective? I have a simple algebraic proof and Nakano actually constructed its inverse.