Saturday, May 07, 2005

Lambda-encoded lambda terms

In The Theory of Fexprs is Trivial, Mitch encodes a datatype in the lambda calculus that itself represents the abstract syntax of lambda calculus terms. The encoding trick involves both higher-order abstract syntax and some cute type equivalences.

Here's a data definition of the abstract syntax terms:
data Term α = Var α
| Abs (α → Term α)
| App (Term α) (Term α)
Notice that the variant representing abstractions is itself encoded using a (meta-language) abstraction. So we can represent the program λx.(x x) as:
Abs (λx.(App (Var x) (Var x)))
This is already a useful hack, because we don't have to come up with a datatype to represent variables, and if we wanted to deal with substitution it would be handled automatically by the substitution mechanisms of the meta-language.

But we need to have some way of representing algebraic datatypes. For this we use the following equivalences:
  α + β → ο
≈ (α → ο) × (β → ο)
≈ (α → ο) → (β → ο)
So to reduce the implementation of a k-variant disjoint union to pure lambda calculus, we CPS the values and split out their continuations into k separate partial continuations. Thus we get our final encoding of the abstract syntax of lambda terms:
⌈x⌉     = λ
⌈λx.M⌉ = λabc.b(λx.⌈M⌉)
⌈(M N)⌉ = λabc.c(⌈M⌉ ⌈N⌉)
Update: I hadn't made the Term datatype polymorphic in its variable type. I think this is right now.


Fritz Ruehr said...

I think the second of your type equivalences is wrong.

I believe this:

α + β → ο
≈ (α → ο) × (β → ο)

But I think the second one should be:

((α → ο) × β) → ο
≈ (α → ο) → (β → ο)

I.e., two paired arguments are iso to two successive arguments, but not a pair of functions is iso to two successive arguments. (I usually think about this in terms of mediating curries and uncurries, etc., but the exponential laws for arithmetic also help.)

Dave Herman said...

Yes -- see this later post for the correction. :)