# Typed NB

Read Chapter 8.

## Syntax and typing rules

TAPL uses T to stand for a type. Most papers use τ.

Typing rules are syntax-directed, that is, typing derivations always have the same shape as syntax trees. It may be helpful to think about the type-checking procedure that the typing rules imply. It’s a recursive function with one case for each typing rule:

``````function typecheck(t)
if t ∈ {true, false}
return Bool
else if t = (if t1 then t2 else t3)
if typecheck(t1) ≠ Bool then fail
T2 = typecheck(t2)
T3 = typecheck(t3)
if T2 ≠ T3 then fail
return T2
else if t = 0
return Nat
else if t = succ t1 or t = pred t1
if typecheck(t1) ≠ Nat then fail
return Nat
else if t = iszero t1
if typecheck(t1) ≠ Nat then fail
return Bool``````

## Type safety

Type safety means that “well-typed programs don’t get stuck” (or “go wrong”). Typically type safety is proven by proving two properties, progress and preservation. In general, it’s probably simpler to work with evaluation rules that write out the congruence rules without using evaluation contexts.

Progress means: If `t:T` for some `T`, then either `t` is a value or `t ⟶ t'` for some `t'`. It is proven by induction on typing derivations.

We illustrate one case of the proof here, case T-If. In this case, the root (bottom) of the typing derivation looks like this:

``````     ⋮        ⋮      ⋮
―――――――   ――――   ――――
t1:Bool   t2:T   t3:T
――――――――――――――――――――――――― T-If
if t1 then t2 else t3 : T``````

By the induction hypothesis, we can assume that either `t1` is a value or `t1 ⟶ t1'` for some `t1'`. So we have two subcases:

• If `t1` is a value, then it must be either `true` or `false`, so either E-IfTrue or E-IfFalse can be used to reduce `t`.

• If `t1 ⟶ t1'` for some `t1'`, then E-If can be used to reduce `t`.

Preservation means: If `t:T` and `t⟶t'`, then `t':T`. (The book’s definition on page 95 allows for the possibility that `t'` is well-typed but has a different type. We won’t encounter any such type systems in this class.) It can be proven either by induction on typing derivations (Proof 8.3.3) or on evaluation derivations (Exercise 8.3.4).

We again illustrate the T-If case of the proof. The typing derivation is as depicted above. We assume that `t⟶t'`, whose evaluation derivation could have one of three forms.

• Subcase E-IfTrue

``````―――――――――――――――――――――――――――――― E-IfTrue
if true then t2 else t3 ⟶ t2``````

And we know from the typing derivation that `t2:T`.

• Subcase E-IfFalse: Just like E-IfTrue.

• Subcase E-If:

``````                       ⋮
――――――――――
t1 ⟶ t1'
―――――――――――――――――――――――――――――――――――――――――――――――― E-If
if t1 then t2 else t3 ⟶ if t1' then t2 else t3``````

We know from the typing derivation that `t1:Bool`, and by the induction hypothesis that `t1':Bool`. So we can build a new typing derivation for `t':T`:

``````      ⋮        ⋮      ⋮
――――――――   ――――   ――――
t1':Bool   t2:T   t3:T
―――――――――――――――――――――――――― T-If
if t1' then t2 else t3 : T``````