Types and Type Theory (part 2)

August 24th, 2009

0

In my previous post I mentioned different ways in which programming languages (and programmers) make use of types and type theory. In my next post I would like to describe the formal system which underlies almost all typed programming languages, the “simply-typed lambda calculus.” But before I get to that, I need to explain the (untyped) lambda calculus, its history, motivation, and functionality.

In the 1930s many people were researching formal models of computation. They were looking for precise ways to describe the sorts of things a computer could do, and thus gain an understanding of the power and limitations of computers.

One famous model of a computer was the Turing Machine, created by Alan Turing in 1936. A Turing Machine is simply a long strip of paper, divided into cells, with a ‘head’ that can move left or right along the paper and read and write into the cells. A program for a Turing Machine is a sequence of statements that move the head, read and write values to the tape, and a single control statement ’if … then … ’. Turing hypothesized that any function that could in principle be calculated could be computed by a Turing Machine.

At the same time that the Turing Machine was proposed, Alonzo Church was working on another model of computation which on the surface looks very different from Turing Machines, but turns out to be equivalent. Church called his model of computation the “lambda calculus”.

(Typographical aside: “Lambda” is a letter in the Greek alphabet that looks like an upside-down ‘Y’. It is commonly represented in ASCII text by either the backslash ‘\’ or simply the word ‘lambda’. I will use the latter convention here.)

Like the Turing Machine, the lambda calculus is deceptively simple to describe, but extraordinarily powerful. Expressions in the lambda calculus have only three forms: they can be variables: x y z …; they can be applications: (e1 e2) where ‘e1’ and ‘e2’ are other expressions; or they can be ‘lambda-abstractions’, which look like (lambda x . e), where ‘x’ is a variable and ‘e’ is another expression.

Lambda-abstractions may seem new and strange, but they just provide a uniform way of writing functions. Consider the function that squares its argument. In standard mathematical notation, this function ‘f’ would be defined as in (1) below.

(1) f(x) = x^2

This equation establishes a relationship between the function being defined (f), the argument the function takes (x), and what the function does (squares x). This function can be written in the lambda-calculus as the expression in (2).

(2) (lambda x . x^2)

This can be read as “the function which takes an x and returns x squared”.

Defining a function with an equation as in (1) requires that we give the function a name (in this case, ‘f’). Lambda abstractions encapsulate all the information about the function (what arguments it takes, and what it does with them), without having to actually name the function. This might seem trivial, but because most complex software contains hundreds or thousands of small functions, not having to name each of them is crucial.

That completes the syntax of the lambda calculus; variables, applications, lambda-abstractions, and nothing more. Although in practice we usually include natural numbers and booleans in the set of expressions, they are not actually needed because we can define lambda-abstractions which behave exactly like numbers and booleans.

Now let’s move on to the semantics of the lambda calculus, which is where the actual ‘computation’ takes place. Happily, the semantics is just as simple as the syntax. There is one main rule, called “beta-reduction”, and it looks like this:

(3) (lambda x . e1) (e2) ==> e1 with all instances of x replaced with e2.

Let’s apply the squared function in (2) with the number 5.

(4) (lambda x . x^2) (5)

This is an application of two lambda expressions, so it is a lambda expression itself. We use beta-reduction to compute its value.

(5) (lambda x . x^2) (5) ==> (5^2) ==> 25

Here we have applied a function to a number, and the result is a number. The lambda-calculus derives its power from the fact that functions can take other functions as arguments, and can return other functions. Consider the function in (6).

(6) (lambda f . (f 5))

This function takes a function as an argument and applies it to the number 5. Let’s apply this function to the squaring function.

(7) (lambda f . (f 5)) (lambda x . x^2)
==> (lambda x . x^2) (5)
==> 5^2 ==> 25

We can nest lambda expressions to create arbitrarily complex and useful functions very easily. The function in (8) takes two other functions as arguments and composes them.

(8) compose = (lambda f . (lambda g . (lambda z . (g (f (z))))))

Let’s compose the square function with the successor function (lambda y . y+1).

(9) (lambda f . (lambda g . (lambda x . (g (f (x)))))) (lambda x . x^2) (lambda y . y+1)
==> (lambda g . (lambda z . (g (lambda x . x^2) (z)))) (lambda x . x^2)
==> (lambda z . ((lambda y . y+1) ((lambda x . x^2) (z))))
==> (lambda z . ((lambda y . y+1) (z^2)))
==> (lambda z . (z^2 + 1))

The result is a function which takes an argument, squares it and adds one, just as we would expect.

There is one other essential reduction rule, called “alpha-reduction”, but it is much less interesting than beta-reduction. Briefly, alpha-reduction allows us to rename bound variables, so two functions that differ only in which variables they use are equivalent. For example, the pair of function in (10) are alpha-equivalent.

(10) (lambda x . x^2) < ===> (lambda y . y^2)

Church and Turing proved that the lambda calculus is just as powerful as a Turing Machine. That is, any function which can be computed in the lambda-calculus can also be computed by a Turing Machine, and vice versa. Furthermore, many other models of computation that have been explored since them also turn out to be equally powerful.

Because it is possible to write a Turing Machine program that runs forever (one that moves the read head left at every step is such a program), it follows that it is possible to write a lambda calculus expression which can never be fully reduced. The function omega defined in (11) is such a function.

(11) omega = (lambda x . x) (lambda x . x)
==> (lambda x . x) (lambda x . x)
==> (lambda x . x) (lambda x . x)
…

This expression has no final value. When we try to reduce it, it returns itself, and no amount of reduction will break this cycle. Once we have infinite computations with no return value, paradoxes arise. Indeed, Russell’s paradox can easily be coded in a lambda-expression.

Further problems arise when we extend the lambda calculus with other useful primitive constants and functions. For example, in the lambda calculus extended with booleans and natural numbers, the following expressions are nonsensical.

(12) (true + 12)

(13) (12 * (lambda x . x + 10))

Both of these expressions are syntactically valid, yet semantically they are nonsense. Intuitively, (12) is nonsensical because there is no way to apply ‘+’ to a boolean value, and (13) is similarly nonsensical because there is no way to apply ‘*’ to a function. (We could define special cases for these functions, but the problem is to general to be solved through this approach.)

It seems we need some way to ensure than functions are only applied to arguments that they know how to handle. Moreover, it would be nice if we could determine whether an expression is nonsensical or not without having to evaluate it. This last part is important because the nonsensical part of a computation could be at the very last step of a very long program, and we would be wasting our time if we tried to evaluate it only to find an error at the very end.

All of these issues were uncovered very soon after the debut of the lambda calculus. The solution is to augment the lambda calculus with types, yielding what’s called “the simply-typed lambda calculus”.

The simply-typed lambda calculus assigns each expression a type, and provides a way to analyze a program for errors without ever running it. The simply-typed lambda calculus is at the core of many modern programming languages, and is still an essential tool in programming language research. Even more amazing is the fact that the simply typed lambda calculus is not just a model of computation, but it is also a model of proofs and logical reasoning. But this will have to wait for a later post.

Tagged with: computation, lambda, Calculus, turing machine, type theory, types

Related Posts

• Types and Type Theory
• The Many Flavors of Curry

Author