Here's a data definition of the abstract syntax terms:

Notice that the variant representing abstractions is itself encoded using a (meta-language) abstraction. So we can represent the program λx.(x x) as:data Term α = Var α

| Abs (α → Term α)

| App (Term α) (Term α)

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.Abs (λx.(App (Var x) (Var x)))

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.
## 2 comments:

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.)

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

Post a Comment