Simply-typed lambda calculus

Read TAPL 9 and 11.1-5.

The simply-typed lambda calculus (λ→ for short) adds a type system to the untyped lambda calculus.

Syntax

The initial definition of λ→ (p. 103) only has one syntax rule for types, namely T ::= T → T. In order for there to be any finite types, we need some base types (cf. Exercise 9.2.1).

T ::= Nat
      Bool
      T → T

Type checking

The typing rules are similar in structure to big-step operational semantics, and typing contexts (Γ) are similar to environments. The way that they map onto an algorithm is that the typing contexts are computed top-down on the syntax tree (bottom-up on the proof tree), but the types are computed bottom-up on the syntax tree (top-down on the proof tree). The pseudocode for type checking looks like this:

function typecheck(t, Γ)
    if t = x
        return Γ(x), {}
    else if t = λx:T1.t2
        T2 = typecheck(t2, Γ ∪ {x:T1})
        return T1→T2
    else if t = t1 t2
        T11→T12 = typecheck(t1, Γ)
        T2 = typecheck(t2, Γ)
        if T11 ≠ T2 then fail
        return T12

Notice how the typing context is passed as an argument and the type is returned.

Properties

Section 9.3 proves various properties of the simply-typed lambda-calculus leading up to type safety. One important property is strong normalization (every term halts), whose proof is deferred to Chapter 12 (which you are not expected to read).

One consequence of this is that the simply-typed lambda calculus is not Turing complete – there are some programs (even programs that always halt) that can’t be written in it. There are two things missing that keep it from being Turing complete, described below.

No recursion

No fixed-point combinator can be defined in the simply-typed lambda calculus (because the fixed-point combinator could be used to write a non-halting term, and that would contradict normalization). There are various ways of adding it back in, including:

• adding it as a primitive (p. 142-145)
• mutable state (Exercise 13.5.8)
• recursive types (p. 273)

But even adding the fixed-point combinator still isn’t enough to restore Turing completeness. With a fixed-point combinator, not every term halts, but it remains decidable whether a given term halts [2]. That’s not true for Turing machines (the halting problem is undecidable), so there must still be a computable function that is not definable in λ→ with fix.

No numbers

Another casualty of adding types is Church numerals. If we assume some type A, we can define them as:

   c0 ≡ λs:A→A. λz:A. z
   c1 ≡ λs:A→A. λz:A. s z
   c2 ≡ λs:A→A. λz:A. s (s z)

and so on, so that each has type (A→A)→A→A. For brevity, let’s write this as CN A. A seemingly minor trouble is that if you want to use Church numerals to iterate a function, you can only do this for functions of type A→A. If you want to iterate a function of another type, then you must define a new set of Church numerals for that type.

But this seemingly minor trouble will become a big one. Let’s keep going:

  scc ≡ λn:CN A. λs:A→A. λz:A. s (n s z)
 plus ≡ λm:CN A. λn:CN A. m scc n          # wrong

This definition of plus is wrong, because m wants a function of type A→A, but scc doesn’t have that type! The definition in the book works:

 plus ≡ λm:CN A. λn:CN A. λs:A→A. λz:A. m s (n s z)

Again, the book’s definition of times, but the alternative definition on page 500 works:

times ≡ λm:CN A. λn:CN A. λs:A→A. λz:A. m (n s) z

But it turns out that the set of functions that can be defined on Church numerals is extremely limited [1] and doesn’t even include the predecessor function. For example, the predecessor function prd given in the book, given cn:CN A, starts with a pair zz ≡ pair c0 c0 and applies the function

   ss ≡ λp. pair (snd p) (scc (snd p))

to it n times to give pair cn-1 cn. Then the first member of this pair is the predecessor.

The problem is that we want prd to have type CN A → CN A, which means that zz must be a pair of CN A’s (let’s write this as CN A × CN A). But in order to apply ss to it n times, we need a representation of n that is of type CN (CN A × CN A), and it’s not clear how to convert our cn of type CN A to type CN (CN A × CN A).

More generally, this means that if we define, say, linked lists, we won’t be able to define cdr, or if we define binary trees, we won’t be able to find the left or right child of a node.

PCF

Combining the simply-typed lambda calculus with numbers and Booleans (Chapter 8) and fix (11.11) forms a language known as PCF (Programming Computable Functions), which is Turing-complete.

The new rules for fix are:

t ::= ...
      fix t

fix (λx:T1. t2) ⟶ [x↦fix (λx:T1. t2)]t2

Γ ⊢ t : T→T
—————————————   (T-Fix)
Γ ⊢ fix t : T

We showed how to simulate a Turing machine in the untyped lambda calculus using two lists to represent the tape. In PCF, we can use numbers to represent lists.

Pierce (p. 143) defines an iseven function; here, we define an isodd function:

isodd ≡ fix (λh:Nat→Bool. λn:Nat.
               if iszero n then false
               else if iszero (pred n) then true
               else h (pred (pred n)))

Similarly, define a half function that divides by two, discarding the remainder:

half ≡ fix (λt:Nat→Nat. λn:Nat.
              if iszero n then 0
              else if iszero (pred n) then 0
              else succ (t (pred (pred n))))

We can then represent a list of Booleans using numbers:

 nil ≡ 0
head ≡ isodd
tail ≡ half

References