Tag Archives: λ calculus

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.

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

Ref.

Oleg Kiselyov, Predecessor and lists are not representable in simply typed lambda-calculus.