Typed λ with Booleans
⟨t⟩ ::= ⟨x⟩
| λ⟨x⟩.⟨t⟩
| if ⟨t⟩ then ⟨t⟩ else ⟨t⟩
Where x is a variable in the λ-Calculus sense. Exclude numbers to keep things simple for now.
⟨T⟩ ::= ⟨T⟩ ⇒ ⟨T⟩ | Bool
J. Carette (McMaster University) Types Fall 2023 1 / 18
Programming Help
Expanding the definition
This grammar allows us to construct some really interesting types!
Bool ⇒ Bool
▶ A function mapping a Boolean argument to a Boolean result.
Bool ⇒ Bool ⇒ Bool
▶ A function mapping a Boolean argument to a function mapping a
Boolean argument to a Boolean result.
▶ ⇒ is right associative, so the above is Bool ⇒ (Bool ⇒ Bool)
(Bool ⇒ Bool) ⇒ (Bool ⇒ Bool)
▶ An operator on Boolean functions.
Plus an infinite number of similar variations!
J. Carette (McMaster University) Types Fall 2023 2 / 18
浙大学霸代写 加微信 cstutorcs
The Typing Relation
How do we type inputs? In general there are two approaches: Explicit Typing (Used in this course).
▶ Typing annotations in the syntax functions: λx : T.t
Implicit Typing (Advanced topic in type theory). ▶ aka via inference.
J. Carette (McMaster University) Types Fall 2023 3 / 18
Programming Help, Add QQ: 749389476
Bad Inference Rule
But consider:
(λx :T1.t2):T1 ⇒T2
λx :Bool. if x then s2 else s3
J. Carette (McMaster University) Types Fall 2023 4 / 18
Enter the Context
x :Bool ⊢t2 :T2
Typing relation becomes a three-place relation, i.e.
context ⊢ term : type
J. Carette (McMaster University) Types Fall 2023 5 / 18
Context in general
In general, need things that look like
{w :T1,x :T2,y :T3}⊢z :T4 (1)
where z can mention w, x, y. General form
Γ⊢t:T (2) where Γ is a set of variable type relations.
Called either the typing context or the typing environment.
J. Carette (McMaster University) Types Fall 2023 6 / 18
Well-formed contexts and variables
Formally we have a well-formed context relation:
· ctx (C-Empty)
Γ, x : T ctx
(C-Extend)
Well-formedness is implicitly assumed. Rather than using · for the empty context, we instead leave it blank:
⊢ t1 : T1 This typing rule is now possible:
x:T∈Γ Γ⊢x:T
Q: what happens if we try to “insert” the same x twice?
J. Carette (McMaster University) Types Fall 2023 7 / 18
Function Typing, Correctly
Let’s try (see board):
Γ,x :T1 ⊢t2 :T2 Γ⊢(λx :T1.t2):T1 ⇒T2
⊢ λx : Bool.λy : Bool.λz : Bool.y
Γ⊢t1 :T1 ⇒T2 Γ⊢t2 :T1 Γ ⊢ t1 t2 : T2
J. Carette (McMaster University) Types Fall 2023 8 / 18
Remark: as is, degenerate.
J. Carette (McMaster University) Types Fall 2023 9 / 18
Inversion Lemma
LEMMA [Inversion of the Typing Relation]
Γ ⊢ x : R =⇒ x : R ∈ Γ Γ⊢(λx :T1.t2):R
=⇒ ∃ R 2 | R = ( T 1 ⇒ R 2 ) ∧ Γ , x : T 1 ⊢ t 2 : R 2 Γ⊢t1t2 :R =⇒ ∃T11 |Γ⊢t1 :T11 ⇒R∧Γ⊢t2 :T11
(I-Abs) (I-App)
J. Carette (McMaster University) Types Fall 2023
Uniqueness still holds
THEOREM [Uniqueness of Types] In a given typing context Γ, if all the free variables of a term t are in the domain of Γ, t has at most one type. Proof Sketch: By induction on term grammar. Crucially relies that each typing rule applies to a single term formation rule.
In this case, we say that the typing relation is syntax directed.
J. Carette (McMaster University) Types Fall 2023 11 / 18
Canonical Forms
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 T1 ⇒ T2, then v has shape λx : T1.t2.
Note that type T1 ⇒ T2 may have infinitely many values as inhabitants.
J. Carette (McMaster University) Types Fall 2023 12 / 18
THEOREM [Progress for the Simply Typed λ-Calculus]
Suppose · ⊢ t : T. Either t is a value, or else there is some t′ such that t → t′.
A later theorem will let us generalize from the empty context. Terms typeable in the empty context are called closed.
Proof by Induction on Typing Derivations. Each evaluation rule is examined in term. Details use use inversion and, for the one tricky case of T-AppAbs, canonical forms are needed.
J. Carette (McMaster University) Types Fall 2023 13 / 18
More about contexts
LEMMA [Permutation invariance]
IfΓ⊢t:T and∆isapermutationofΓ,then∆⊢t:T. Moreover,the latter derivation has the same depth as the former.
Proof Sketch: induction on typing derivations.
We add extra “facts” without changing conclusions: LEMMA [Weakening] IfΓ⊢t:T andx∈/dom(Γ),thenΓ,x:S⊢t:T. Moreover,thelatter derivation has the same depth as the former.
Proof Sketch: Induction on typing derivations.
Points of variations show up here, i.e. linear types, union types, dependent
types, etc.
J. Carette (McMaster University) Types Fall 2023 14 / 18
Substitution Lemma I
LEMMA [Preservation of Types Under Substitution]
Γ,x :S ⊢t :T ∧Γ⊢s :S =⇒ Γ⊢[x 7→s]t :T (3) Proof will proceed by induction over typing derivations, and using a case
analysis over typing rules. As a reminder:
J. Carette (McMaster University) Types Fall 2023 15 / 18
Substitution Lemma II
T-True, T-False, T-If, T-App straightforward. T-Var: t = z ∧ z : T ∈ (Γ, x : S )
Case x = z
▶ [x 7→ s ]z would then evaluate to s .
▶ x = z ∧ z = t =⇒ x = t
▶ Viatheuniquenessoftypes,x:S∧t:T =⇒ S=T
▶ Substituting into lemma statement:
Γ,x:S⊢x:S∧Γ⊢s:S =⇒ Γ⊢s:S
Now consider x ̸= z
▶ [x 7→ s]z would then evaluate to z (and from there to t).
Γ,x:S⊢t:T∧Γ⊢s:S =⇒ Γ⊢t:T We can now conclude by weakening.
J. Carette (McMaster University) Types Fall 2023 16 / 18
Substitution Lemma III
T-Abs: t =λy :T3.t1 ∧ T =T3 ⇒T4 ∧ Γ,x :S,y :T3 ⊢t1 :T4 By our meta-rule of substitutions in λ expressions, we derive:
x ̸= y y ∈/ FV(s)
Using the the permutation lemma on the rightmost equation:
Γ,y : T3,x : S ⊢ t1 : T4 Using the weakening lemma on Γ ⊢ s : S:
Γ, y : T3 ⊢ s : S
By the induction hypothesis:
Γ,y :T3 ⊢[x 7→s]t1 :T4.
J. Carette (McMaster University) Types Fall 2023 17 / 18
Substitution Lemma IV
Recall T-Abs:
Γ,x :T1 ⊢t2 :T2 Γ⊢λx :T1.t2 :T1 ⇒T2
Applying this to last equation Γ, y : T3 ⊢ [x 7→ s]t1 : T4, get Γ⊢λy :T3.[x 7→s]t1 :T3 ⇒T4
The definition of substitution is:
[x 7→ s](λy : T3.t1) = λy : T3.[x 7→ s]t1
The LHS has type T3 ⇒ T4 from our original case analysis. The RHS has the same type from above.
J. Carette (McMaster University) Types Fall 2023 18 / 18