.png)
4 months ago
4
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.
Let’s kick off by defining our term functor and the fixpoint type. We’ll use de-Bruijn indices for simplicity.
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?
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:
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:
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.
Checking that k and reverse-k work as expected:
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).
