# A catamorphic lambda-calculus interpreter

I was playing around with recursion-schemes, which is pretty cool. It’s very nice to be able to define interpreters like this, so my immediate thought was: can we do this for the lambda-calculus?

Strangely, I couldn’t find any examples online of lambda-calculus interpreters written as catamorphisms, and it actually turns out to be a little bit tricky. So here’s what I came up with.

```
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module Lambda where
import Data.Functor.Foldable
import Control.Monad.Reader
```

Let’s kick off by defining our term functor and the fixpoint type. We’ll use de-Bruijn indices for simplicity.

```
data LambdaF e = Index Int | Abs e | Apply e e
deriving (Functor)
type Lambda = Fix LambdaF
```

Now, what are we going to evaluate terms *into*? This is an important decision,
because our algebra will take a `LambdaF`

with all the subterms evaluated. So
the value needs to contain everything we need to know about that subterm.

This is a bit awkward for function values. The
traditional
thing to do is to
evaluate a function term into a “closure”, which includes the original *term* as
well as the captured environment. But we don’t want to be carting around terms
if we can help it, and evaluating a whole term later will require calling the
*recursive* evaluation function, not our one-layer algebra.

Well, what *is* a closure? It’s a kind of suspended computation, so what if we
just evaluated it *into* a suspended computation?

```
data Value m where
Num :: Int -> Value m
Clos :: Monad m => [Value m] -> m (Value m) -> Value m
instance Show (Value m) where
show (Num i) = show i
show (Clos _ _) = "closure"
```

Our `Clos`

value constructs a closure out of a captured environment (just a list
of values, since we’re using de-Bruijn indices), and a suspended computation
which will eventually produce another `Value`

.

The rather unsatisfactory `Show`

instance highlights one problem with this
approach - because we’re representing computation values with actual *Haskell*
computations, they’re difficult to introspect.

Okay, we can now write our algebra:

```
type Algebra f a = f a -> a
-- specialisation of the real signature
-- cata :: Algebra f a -> Fix f -> a
-- note the weird contstraint
evalAlgebra :: (MonadReader [Value m] m) => Algebra LambdaF (m (Value m))
evalAlgebra term = case term of
Index i -> do
e <- ask
pure $ e !! i
Abs t -> do
-- capture the environment
e <- ask
-- store the environment and the un-evaluated body
-- computation in a closure
pure $ Clos e t
Apply f x -> do
-- this will cause pattern match failures if the term
-- isn't well-typed
Clos ctx t <- f
c <- x
-- current env doesn't matter, prepend argument to
-- captured env and evaluate stored computation in that context
local (\_ -> (c:ctx)) t
```

This is pretty neat - the body of an abstraction has been evaluated to a `m (Value m)`

,
which we can just put into the closure value. Later, when evaluating an
application we can just fish out the monadic computation and evaluate it in the
expanded environment.

Initially I thought that I would want to write this as a monadic
catamorphism. However,
with monadic catamorphisms the idea is that the `Traversable`

constraint allows
us to automatically evaluate all the monadic computations for sub-terms before evaluating the
next level of the algebra. But this is *not* what we want, because we want to
take the *un*-evaluated computation for the body of an abstraction and save it to evaluate later in a different
environment. So we just want a normal catamorphism which computes monadic values.

We’ve ended up with a *weird* constraint on our `m`

, though: `(MonadReader [Value m] m)`

.
This is a bit tricky to satisfy, but we can just define our own recursive type:

```
newtype EnvM t = EnvM { unEnv :: Reader ([Value EnvM]) t }
deriving (Functor, Applicative, Monad)
instance (MonadReader [Value EnvM] EnvM) where
ask = EnvM $ ask
local f = EnvM . local f . unEnv
eval :: Lambda -> [Value EnvM] -> Value EnvM
eval t initial = runReader (unEnv (cata evalAlgebra t)) initial
```

Aside: this is pretty unpleasant, especially having to write instances for the new type rather than just using a generic monad transformer stack. I’d be interested if anyone has a nicer way of doing this.

And that’s more or less it, let’s give it a spin.

```
-- convenience constructors
index :: Int -> Lambda
index i = Fix $ Index i
abst :: Lambda -> Lambda
abst e = Fix $ Abs $ e
app :: Lambda -> Lambda -> Lambda
app e1 e2 = Fix $ Apply e1 e2
-- SKI combinators
i :: Lambda
i = abst $ index 0
k :: Lambda
k = abst $ abst $ index 1
s :: Lambda
s = abst $ abst $ abst $
((index 2) `app` (index 0)) `app` ((index 1) `app` (index 0))
```

Checking that `k`

and reverse-`k`

work as expected:

```
> eval (k `app` (index 1) `app` (index 0)) [Num 1, Num 2]
2
> eval (s `app` k `app` (index 1) `app` (index 0)) [Num 1, Num 2]
1
```

Overall this seems like a pretty nice approach and I’m surprised I can’t find any examples of people doing it before. There are some resemblances to HOAS, but I think this version works more nicely with a monadic interpreter (e.g. it would be easy to insert logging).