Learning the Lambda Calculus, simple types

The simply typed lambda calculus adds a notion of type to the terms of the LC. Each term is given a type, and terms that cannot be assigned a type are forbidden. This restriction gives us a system with a couple of particularly nice properties. Perhaps the most important property is called strong normalization. In previous posts we saw that we could turn terms into other terms using the three rules, alpha, beta, and eta. If a term has no parts that can be reduced with beta and eta reduction than the term is said to be in (beta eta) normal form. When trying to determine if two terms are equal we would like to be able to reduce them to a single form and then just check if they look the same. The problem, however, is that not all terms in the untyped lambda calculus have a normal form, as we saw when we tried to use the Y combinator. Restricting terms to those with types we can get a system where every term has a unique normal form. For completeness sake I want to mention that when I say unique I mean unique up to alpha conversion, so the terms (\x.x) and (\y.y) are the same because they can be converted into each other with just renaming of bound variables.

If a system has a unique normal form for every term then every computation completes in that system, as the notion of computation in the LC is finding the normal form. Even better, when we talk about "strong" normalization we mean that it doesn't matter which sequence of reduction we do, we will always end up with the same form. Doing the steps in different orders has important consequences in practice, and is the essential idea of laziness in programming language. I hope to talk about laziness and non-strictness in a later post.

So, on to the actual types. To give a type to a term, we must have a type context. I'm not going to go much into this concept, and I will informally assign types variable names like a, b, c, ... and variables names like x, y, z, ... to help distinguish between them. Notice that types are just like assumption in logic, and a type context is just a set of assumptions.

Lets look at a simple term- (\x.x). This term takes an argument and returns that argument. If we knew that the variable x had to be of type "a" then we would say that (\x.x) : a -> a where ":" is pronounced "has type" or "is in" (if we think of types as sets). We shouldn't use variables without giving them types anymore, so really that term would be written (\x:a.x) : a -> a. The type of the input is "a" and the result is also of type "a" so the result is a function of a to a. The arrow is a connective in that it takes two types and creates a new type out of them- the type of function from the first type to the second. If we assume that we have integers and booleans then the type integer -> boolean might be the type of a function called "even" or "odd" or "equalsZero" or anything that takes an integer and results in a boolean value.

Notice that I said that we assume that we have a type "a" before giving the type of (\x.x). This is because that term, the identity function, doesn't just have one type, but rather there are an infinite number of terms of the same form with different types. In other words, for each type there is an identity function that takes a value of that type and just returns it unchanged. This is a little bit unfortunate as we would like that the term's type reflect that it is essentially the same for every type. In the simply typed lambda calculus we simply don't have the ability to state such a thing, and we would have to add something (universal quantification) to gain this ability.

We have seen that a term can have the type a -> a, but what other types are there? Well, each type variable (a, b, c, ...) is a type, and for any two types a and b, a -> b is a type, and there are no types besides these. If we take "a" to be (d -> c) and b to be "e" then (d -> c) -> e (given a function from d to c return a value of type e) and e -> (d -> c) (given a value of type e, return a function from d to c) are certainly types.

In addition to these rules specifying which types exist, there are rules for giving types to terms. Given that x : a (x has type a) and y : b we can deduce that (\y. x) : b -> a, as the input is of type b and the output (the variable x) is of type x. Just so we are clear here, there is some subtly going on here with type contexts and substitution that I am completely ignoring.

Given a function (\x:a. y) where y : b, and a value z : a, the type of (\x:a.y)z is of course b. Applying an argument of the correct type as the input to a function gets a result of the same type as the result of the function.

In the Y combinator post I gave Y the type (a -> a) -> a. I was being very informal, as Y cannot be given a type in the simply type lambda calculus, which avoids the associated contradiction.

Unfortunately the simply typed lambda calculus is not very expressive, and I think we will just move on to the polymorphic lambda calculus aka the second order lambda calculus aka System F. This brings us to just about the type system of Haskell and introduces a huge amount of interesting material. Because this series is pretty informal I think we will just cover these topics very lightly, as it gets harder and harder to go on without needing some more rigorous discussion to talk about interesting things.