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⌉     = λabc.ax
⌈λ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.