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