# Simply-typed lambda calculus

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