Code == Data: The Basics
There have been a lot of blog entries lately about code versus data: which is more valuable, are they the same, or maybe different, and so on. Most recently, here. That blog entry argues that code is data, and points out Turing’s work on universal Turing machines as an example. The dual argument, that data is code, can be attributed to Church, thereby completing the pair of early computer science figureheads. This won’t be new to most advanced computer science students, but I was unable to find a single place where it’s written down.
To start, two special cases will be helpful. I will be assuming that the reader knows the basic evaluation rules of lambda calculus. The technique here will be the same: use an appropriate function to represent data.
Special Case 1: Finite Enumerated Types
Suppose I want to write lambda calculus expressions to represent the four cardinal directions (north, south, east, and west), and left and right turns. Here’s what I’m shooting for, in Haskell.
data Dir = East | West | North | South left East = North left West = South left North = West left South = East right East = South right West = North right North = East right South = West
To do this in lambda calculus, I need four “data” values, and as promised they will be defined as functions.
East := λabcd.a West := λabcd.b North := λabcd.c South := λabcd.d
(Note that I’m using
:= to denote definition of short-hand names; it is not, of course, part of the lambda calculus itself. In particular, you have the right to complain loudly if I try to give circular definitions; there is no such thing as direct general recursion.)
These are functions that take four parameters and return, respectively, the first, second, third, and fourth ones. Now defining functions case-wise on these values is trivial:
left := λd.d (North) (South) (West) (East) right := λd.d (South) (North) (East) (West)
left function take a parameter
d, which is itself a function, and operates by calling that function and passing it four arguments. Now if the function happens to be
East, then it will return its first result, thereby correctly concluding that north is a left turn from east.
Special Case 2: Church Numerals
A slightly more involved data type is natural numbers. Alonzo Church defined natural numbers in terms of Church numerals. The idea is that a natural number n is a function which iterates another function n times on some initial value. For example, using the functions above, we can say that:
0 left North = North 1 left North = West 2 left North = South 3 left North = East 4 left North = North
So the first few natural numbers are:
0 := λfx.x 1 := λfx.fx 2 := λfx.f(fx) 3 := λfx.f(f(fx)) 4 := λfx.f(f(f(fx)))
And here are a few operations on these natural numbers. It can take some hard work with a pencil and paper to see why some of them work.
inc := λp.(λfx.f(pfx)) add := λpq.(λfx.pf(qfx)) mul := λpq.(λfx.p(qf)x)
General Case: Algebraic Data Types
Algebraic data types are a general approach to defining data types in a programming language. A type may have several different forms, each of which may have several fields. Another way of saying this is that an ADT is a sum of products of other types. Here’s an example in Haskell:
data Discount = FixedAmount Double | Percent Double | Rebate Date Double
In other words, a discount is either a fixed amount of money at purchase, or a percent off the purchase price, or a rebate of some amount that happens at some future date.
data Tree = Leaf Char | Branch Tree Tree
So a tree is either a leaf, or a branch node whose left and right children are trees in their own right.
Both of the special cases above are also algebraic data types. Directions have four forms, each of which is an empty product:
data Dir = East | West | North | South
Church numerals implement natural numbers defined as:
data Nat = Succ Nat | Zero
As you may guess, we’re going to write functions to represent any kind of data of any algebraic data type as a function in the lambda calculus. The idea will be this: we will ask the person using the data to write a handler for each form that the data may take. Then they’ll give us all of these handler functions, and we’ll use the one that applies. So a value of some algebraic data type will be a function that takes a bunch of handlers, and produces the result of one of them. Examples follow:
Discount data type, the value
FixedAmount $2.75 looks like this:
FixedAmount $2.75 := λfpr . f ($2.75)
In other words, this is a function that takes three handlers f, p, and r (one for fixed amounts, one for percentages, and another for rebates). It then calls the first handler, passing it the amount of the fixed discount.
To calculate the amount of money to hand someone as they are buying an item at a price p with a discount d, one may write:
d (λa.a) (λp.(p*a)) (λda.0)
The first handler says that if the discount is for a constant amount, you give back that amount. The second says that if the discount is for some percent, you multiply it by the price and give that back. The third handler says that if the discount is a rebate to be filled later, you don’t give them anything right now. This is all done by calling the data as a function.
To use a Church numeral, you pass it two handlers. The first says what you want back if it’s the successor of another number. The next handler says what to do if it’s zero. Using this, we can write a slightly wordier version of the
inc function from before:
inc := λp.p (λfx.f(pfx)) (λfx.fx)
The second handler is just a value, since there are no fields in that case.
So there you have it, not only is code a type of data (Turing’s approach), but also data is a type of code (Church’s approach).