types

Two big questions:
1 What can we say about a term without running it? (Static Analysis)
2 Can we tell a term will get stuck without running it? (Types)
A type is a means of classifying terms. We will want these to “play well” with the reduction relation.
J. Carette (McMaster University) Types Fall 2023 1 / 17

Typing Rules for Booleans
Like our operational semantics, the typing relation is defined using a set of inference rules.
J. Carette (McMaster University) Types Fall 2023 2 / 17

Note the form of the rule T-If.
If both t2 and t3 have the same type T, then complete expression has
Otherwise, the expression has no type
A term which can be typed is called typable, or well-typed. A term which
can’t be typed is called untypable.
Another way to say it: the type relation is not total on terms.
J. Carette (McMaster University) Types Fall 2023 3 / 17
Code Help, Add WeChat: cstutorcs
Note the form of the rule T-If.
If both t2 and t3 have the same type T, then complete expression has
Otherwise, the expression has no type
A term which can be typed is called typable, or well-typed. A term which
can’t be typed is called untypable.
Another way to say it: the type relation is not total on terms.
The following evaluates to a value, but is untypeable:
if true then false else 0 (1)
J. Carette (McMaster University) Types Fall 2023 3 / 17

Natural Numbers
J. Carette (McMaster University) Types Fall 2023 4 / 17

Programming Help
Definition of the Typing Relation
The typing relation for arithmetic expressions is the smallest binary relation between terms and types satisfying all the typing rules given in the last two figures.
A term t is well-typed if there is some T such that t : T When talking about types, we will often make statements like:
If a term of the form succ t1 has any type at all, then it has type Nat. There is a sort of information flow, up and down the AST, of typing
information.
J. Carette (McMaster University) Types Fall 2023 5 / 17

Inversion of the Typing Relation
The following inversion rules are immediately derivable from our typing rules:
LEMMA: [Inversion of the Typing Relation]
true : R =⇒ R = Bool (2)
false : R =⇒ R = Bool (3) if t1 then t2 else t3 :R =⇒ t1 :Bool∧t2 :R∧t3 :R (4)
0 : R =⇒ R = Nat
succ t1 : R =⇒ R = Nat ∧ t1 : Nat pred t1 : R =⇒ R = Nat ∧ t1 : Nat iszero t1 : R =⇒ R = Bool ∧ t1 : Nat
(5) (6) (7) (8)
J. Carette (McMaster University) Types
Fall 2023 6/17

Typing Derivations
Consider the term if iszero 0 then 0 else pred 0 Let’s draw (on board) a typing derivation for it.
J. Carette (McMaster University) Types Fall 2023 7 / 17

Uniqueness of Types
THEOREM [Uniqueness of Types]
Each term t has at most one type. That is, if t is well-typed, then its type is unique. Additionally, there is only one derivation of this type, based on our inference rules.
Proof is by structural induction on t, and uses inversion.
Note that induction over typing derivations is also a valid means to prove
certain properties.
J. Carette (McMaster University) Types Fall 2023 8 / 17

Type Safety
The most important property of any type system: safety. Slogan: Well-typed terms can’t go wrong
i.e., if a term is well typed, it can’t get stuck.
We break safety down into two pieces:
Safety = Progress + Preservation
J. Carette (McMaster University) Types Fall 2023 9 / 17
Programming Help, Add QQ: 749389476
Progress + Preservation
THEOREM [Progress of Typed Arithmetic Expressions]
A well-typed term is not stuck. That is, either it is a value, or one of our evaluation rules can be applied.
THEOREM [Preservation of Typed Arithmetic Expressions]
If a well-typed term takes a step of evaluation, then the resulting term is also well-typed.
Taken together, we can say that any well-typed term will eventually evaluate to a well-typed value without getting stuck.
We can argue this inductively over evaluation derivations.
J. Carette (McMaster University) Types Fall 2023 10 / 17

Canonical Forms
The canonical forms of a type are the values which have that type.
LEMMA [Canonical Forms]
1 If v is a value of type Bool, then v is either true or false
2 If v is a value of type Nat, then v is a numeric value.
▶ That is, v is either 0, or succ nv, where nv is also a numeric value.
J. Carette (McMaster University) Types Fall 2023 11 / 17

Canonical Form of Bool, Nat
If v is a value of type Bool, then v is either true or false
By analysis of all values forms: true, false, 0, and succ nv.
For true and false, get Bool from inversion.
For 0, get Nat from inversion.
For succ nv inversion gives that term must have type Nat, not Bool.
If v is a value of type Nat, then v is either 0 or succ(nv) where nv is a value of type Nat.
Argument is very similar to above.
J. Carette (McMaster University) Types Fall 2023 12 / 17

Proof of Progress I
THEOREM : [Progress]
Suppose t : T. Then t is either a value, or else there is some t′ such that t → t′.
By Induction on typing derivations:
T-True, T-False, and T-Zero, all apply if t is a value.
J. Carette (McMaster University) Types Fall 2023 13 / 17

Proof of Progress II
By inversion:
t =if t1 then t2 else t3 (9)
t1 :Bool t2 :T t3 :T
▶ By the induction hypothesis, t1 is either a value, or there is some t1′ such that t1 → t1′
⋆ If a value, t1 must be true or false, via the canonical forms lemma. In these cases either E-IfTrue or E-IfFalse apply to t respectively.
⋆ If t1 → t1′ , then E-If is applicable to t.
J. Carette (McMaster University) Types Fall 2023 14 / 17

Proof of Progress III
T-Succ. Inversion gives t = succ t1 ∧ t1 : Nat ▶ IH: either t1 value, or ∃ t1′ such that t1 → t1′
⋆ If t1 is a value, must be numeric value (cannonical forms lemma).
⋆ If t1 → t1′ , Then E-Succ is applicable.
T-Pred. Inversion gives t = pred t1 ∧ t1 : Nat
▶ IH:t1 iseitheravalue,or∃t1′ suchthatt1 →t1′
⋆ If t1 is a value, it must be a numeric value via the canonical forms lemma. – If t1 = 0, E-PredZero applies to t.
– If t1 = succ t2, E-PredSucc applies to t.
⋆ If t1 → t1′ , the congruency rule E-Pred applies to t . T-IsZero. Inverse gives t = isZero t1 ∧ t1 : Nat
▶ IH:t1 iseitheravalue,or∃t1′ suchthatt1 →t1′
⋆ If t1 is a value, must be NV by canonical from lemma.
– If t1 = 0, E-IsZeroZero applies to t.
– If t1 = succ t2, E-IsZeroSucc applies to t.
⋆ If t1 → t1′ , the congruency rule E-IsZero applies to t .
J. Carette (McMaster University) Types

Proof of Preservation I
THEOREM [Preservation of Typed Arithmetic Expressions]
t:T∧t→t′ =⇒t′:T
Induction on typing derivations; if last step was: T-True: t = true ∧ T = Bool, so t ↛ t′. T-False, T-Zero: same.
T-Succ: t = succ t1 ∧ T = Nat ∧ t1 : Nat
only one rule, E-Succ:, thus t1 → t1′ .
Plus t1 : Nat implies t1′ : Nat.
From t′ = succ t1′ and t1′ : Nat, typing says t′ : Nat
J. Carette (McMaster University) Types

Proof of Preservation II
T-If: t=if t1 then t2 else t3,t1 :Bool∧t2 :T∧t3 :T Now case analysis on evaluation rules for if:
E-IfTrue: t1 =trueandt′ =t2 =⇒t′ :T.
E-IfFalse: t2 = false and t′ = t3 =⇒ t′ : T.
E-If: t1 →t1′ andif t1 then t2 else t3 →if t1′ then t2 else t3.
▶ IH:t1:T∧t1→t1′ =⇒t1′:T.
⋆ t1 : Bool (via typing relation case analysis)
⋆ t1 → t1′ (via evaluation relation case analysis) ⋆ Thus t1′ : Bool by IH
▶ Ast1′ :Bool,t2 :T andt3 :T,typinggivesif t1′ then t2 else t3 :T. (and so on; T-Pred does require more care)
J. Carette (McMaster University) Types Fall 2023 17 / 17