Simple types Explicit types Fixpoint operators
Typing Lambda terms
Draft April 16, 2013
Slides by Matthew Hennessy
Typing Lambda Draft April 16, 2013
Simple types Explicit types Fixpoint operators
Things go wrong
M ∈ Lambda ::= v | x | if M1 then M2 else M3
| (M1 + M2 ) | M1 = M2
| M1 M2
v ∈ Val ::= n | tt | ff | λx .M
I tt λx .0
I if λx .x = 1 then 0 else ff
Typing:
A static analysis to avoid runtime errors
Typing Lambda Draft April 16, 2013
Simple types Explicit types Fixpoint operators
Simple types
σ ∈ STypes ::= base | σ1 → σ2
base ::= int | bool
Every value is either:
I an integer
I a Boolean
I or a function
Note: every type has the form
σ1 → σ2 → . . . . . . σk → base k ≥0
where base is either int or bool
Typing Lambda Draft April 16, 2013
Simple types Explicit types Fixpoint operators
Typing judgements
Γ`M:σ
Type environment Γ:
Γ ::= | Γ, x : σ
Type environment: x1 : σ1 , . . . xn : σn variables may be repeated
Environment lookup:
(ty-look1) (ty-look2)
Γ ` x 2 : σ1
x1 6= x2
Γ, x : σ ` x : σ Γ, x1 : σ1 ` x2 : σ2
Intuition: scan from right-to-left looking for variable
Typing Lambda Draft April 16, 2013
Simple types Explicit types Fixpoint operators
Standard typing rules
(ty-int)
Γ ` n : int
(ty-bool) (ty-bool)
Γ ` tt : bool Γ ` ff : bool
(ty-i−op) (ty-b−op)
Γ ` F1 : int Γ ` F2 : int Γ ` F1 : bool Γ ` F1 : bool
Γ ` F1 op F2 : int Γ ` F1 bop F2 : bool
(ty-le)
Γ ` F1 : int Γ ` F2 : int
Γ ` F1 < F2 : bool
Typing Lambda Draft April 16, 2013
Simple types Explicit types Fixpoint operators
More standard typing rules
(ty-eq)
Γ ` F1 : base Γ ` F2 : base
Γ ` F1 = F2 : bool
(ty-if)
Γ ` B : bool
Γ ` F1 : σ Γ ` F2 : σ
Γ ` if B then F1 else F2 : σ
I Only base types can be compared int and bool
Typing Lambda Draft April 16, 2013
Simple types Explicit types Fixpoint operators
Typing functions
(ty-abs)
Γ, x : σ1 ` M : σ2
Γ ` λx .M : σ1 → σ2
(ty-app)
Γ ` M : σ1 → σ2 , Γ ` N : σ1
Γ ` M N : σ2
Typing Lambda Draft April 16, 2013
Simple types Explicit types Fixpoint operators
Example typing
(ty-look) (ty-look)
Γxf ` f : int → int Γxf ` x : int
(ty-app) (ty-int)
Γxf ` f (x) : int Γxf ` 1 : int
(ty-add)
x : int, f : int → int ` f (x) + 1 : int
(ty-abs)
x : int ` λf .f (x) + 1 : (int → int) → int
(ty-abs)
ε ` λx .λf .f (x) + 1 : int → (int → int) → int
Typing Lambda Draft April 16, 2013
Simple types Explicit types Fixpoint operators
Sanity checks
I Repetition: Γ1 , x : σ1 , Γ2 , x : σ2 , Γ3 ` M : σ implies
Γ1 , Γ2 , x : σ2 , Γ3 ` M : σ
I Strengthening:
If x is not in fv(M) then Γ1 , x : σx , Γ2 ` M : σ implies
Γ1 , Γ2 ` M : σ.
I Weakening:
I Γ ` M : σ implies x : σx , Γ ` M : σ
I Γ ` M : σ implies Γ, x : σx ` M : σ, provided x does not occur in M.
I Permutation: Γ1 , x : σx , y : σy , Γ2 ` M : σ implies
Γ1 , y : σy , x : σx , Γ2 ` M : σ, provided x is different than y .
Typing Lambda Draft April 16, 2013
Simple types Explicit types Fixpoint operators
Well-typed programs don’t go wrong
Safety = Progress + Preservation
Progress:
Suppose M is a program closed term and ` M : σ Then either:
I M is a value
I or M → N for some N
Proof by induction on ` M
Preservation:
If Γ ` M : σ and M → N then Γ ` N : σ
Proof by Rule Induction on M → N
Requires Substitution Property for typing derivations
Typing Lambda Draft April 16, 2013
Simple types Explicit types Fixpoint operators
Substitution Property
Γ, x : σ1 ` M : σ2 and Γ ` N : σ1 implies Γ ` M{|N/x |} : σ2
I Proof by Rule induction on Γ, x : σ1 ` M : σ2
I See Course Notes for proof for language ExpB
I See Pierce page 107
Typing Lambda Draft April 16, 2013
Simple types Explicit types Fixpoint operators
Too many types
The type of a program indicates its intended use:
I int → int
I (int → int) → int → int
λx .x has many types:
I ` λx .x : bool → bool
I ` λx .x : int → int
I ` λx .x : (int → bool) → (int → bool)
Programs with multiple types are confusing
Typing Lambda Draft April 16, 2013
Simple types Explicit types Fixpoint operators
Simply typed LambdaT
M ∈ LambdaT ::= n | tt | ff | x
| (M1 + M2 ) | (M1 × M2 ) | M1 = M2
| if M1 then M2 else M3
| λx : σ .M | M1 M2
Using explicit types
Revision:
I Operational semantics unchanged
(ty-abs)
Γ, x : σ1 ` M : σ2
I Revised typing rule:
Γ ` λx : σ1 .M : σ1 → σ2
Typing Lambda Draft April 16, 2013
Simple types Explicit types Fixpoint operators
Pros and cons
Plus: In LambdaT types are unique:
Γ ` M : σ1 and Γ ` M : σ2 implies σ1 = σ2
Minus: Strong normalisation:
I For every program M there is a bound k such that M →n N
implies n ≤ k
I ∆ is not typable λx : σ .x x
def
I Fixpoint combinator A = λx : σ .λy .y (xxy ) not typable
I LambdaT does not support recursive programming
Typing Lambda Draft April 16, 2013
Simple types Explicit types Fixpoint operators
Adding fixpoint operators - lazy
M ∈ Lambdafix ::= . . .
| λx : σ .M | M1 M2
| fix.M
Semantics:
(l-fix)
fix.M →l M(fix.M)
Typing:
(ty-fix)
Γ`M:σ→σ
Γ ` fix.M : σ
Typing Lambda Draft April 16, 2013
Simple types Explicit types Fixpoint operators
Example
F , λf .λx .if x = 0 then 1 else f (x − 1)
fix.F 1 →l F (fix.F ) 1
→l (λx .if x = 0 then 1 else fix.F (x − 1)) 1
→l if 1 = 0 then 1 else fix.F (1 − 1)
→∗l fix.F (1 − 1)
→l F (fix.F ) (1 − 1)
→l (λx .if x = 0 then 1 else fix.F (x − 1)) (1 − 1)
→l if (1 − 1) = 0 then 1 else fix.F ((1 − 1) − 1)
→∗ 1
Typing Lambda Draft April 16, 2013
Simple types Explicit types Fixpoint operators
Does not work for eager semantics
F , λf .λx .if x = 0 then 1 else f (x − 1)
fix.F 1 →e F (fix.F ) 1
→e F (F fix.F ) 1
→e . . .
→e F (F (F . . . fix.F ) . . .) 1
Eager recursion: need mechanism for stopping evaluation of next
iteration
Typing Lambda Draft April 16, 2013
Simple types Explicit types Fixpoint operators
Eager fixpoint
M ≈sem λx .M x
provided:
I x is fresh to M
I M has a function type σ1 → σ2
Semantics: Typing:
(l-cbv.fix) (ty-cbv.fix)
fixcbv .M → M(λx .fixcbv .M x) Γ`M:σ→σ
Γ ` fixcbv .M : σ
Typing Lambda Draft April 16, 2013
Simple types Explicit types Fixpoint operators
Example: Eager
F , λf .λx .if x = 0 then 1 else f (x − 1)
fixcbv .F 1 → F (λy .fixcbv .F y ) 1 y fresh
→ (λx .if x = 0 then 1 else (λy .fixcbv .F y )(x − 1)) 1
→ if 1 = 0 then 1 else (λy .fixcbv .F y )(1 − 1)
→∗ (λy .fixcbv .F y )(1 − 1)
→∗ fixcbv .F 0
→ F (λy .fixcbv .F y ) 0
→ (λx .if x = 0 then 1 else (λy .fixcbv .F y )(x − 1)) 0
→ if 0 = 0 then 1 else . . . . . .
→∗ 1
Typing Lambda Draft April 16, 2013
Simple types Explicit types Fixpoint operators
Functional programming languages
I lazy Lambdafix : basis for lazy functional languages
e.g. Haskell
I eager Lambdafix : basis for eager/call-by-value functional
languages
e.g. ML
Typing Lambda Draft April 16, 2013
