IA014: Advanced Functional
Programming
3. Simply Typed Lambda Calculus
Jan Obdržálek obdrzalek@fi.muni.cz
Faculty of Informatics, Masaryk University, Brno
IA014 3. Simply Typed Lambda Calculus 1
Motivation
Untyped λ-calculus:
• does not distinguish between functions and arguments
everything is a function!
• the evaluation may get stuck
• (x y) → not a value
• (λx. succ x) true → succ true →
• 42 + λx.x →
Solution? Types!
In this lecture we will:
• define the simply typed λ-calculus λ→
• be working with λ-calculus extended with Booleans
• use t, t . . . for terms (instead of M, M , N, . . .)
IA014 3. Simply Typed Lambda Calculus 2
Type systems
A type system is a tractable syntactic method for proving the
absence of certain program behaviours by classifying phrases
according to the kinds of values they compute.
B. Pierce, Types and Programming Languages
Desirable properties
1 type safe
well-typed programs “do not go wrong”
2 not too conservative
most useful programs should be typeable
IA014 3. Simply Typed Lambda Calculus 3
Revision: Call-By-Value λ-calc.
syntax
t ::= x variable
| t t application
| λx.t abstraction
v ::= λx.t abstraction value
semantics
(λx.t) v → t[x := v]
t1 → t1
t1 t2 → t1 t2
t → t
v t → v t
IA014 3. Simply Typed Lambda Calculus 4
Adding types – syntax of λ→
Terms and Values
t ::= x variable
| t t application
| λx :T .t abstraction
| true constant true
| false constant false
| if t then t else t conditional
v ::= λx :T .t abstraction value
| true true value
| false false value
Types
T ::= T → T function type
| Bool Boolean type
IA014 3. Simply Typed Lambda Calculus 5
Basic type terminology
T ::= T → T function type
| Bool Boolean type
The grammar above defines the set of simple types over Bool:
• Bool is a base type (also atomic type)
• T1 → T2 is a function type: type of functions expecting
arguments of type T1 and returning results of T2
• “→” is a type constructor
(creates a new type based on T1 and T2)
Notation
• t : T means t is of type T
IA014 3. Simply Typed Lambda Calculus 6
Typing relation, context
Consider a term t := λx.t .
• the type of the body t depends on the type of the
argument x
• type of t depends on the type of both t and x
• when typing t we need to “know” the type of x (a context)
Typing context Γ
Γ t : T
Term t has type T in the typing context Γ.
• binding x : T is a pair variable+type
• Γ is a sequence of bindings
• we can assume that all bindings in Γ are distinct
• for empty context, we write just t : T
IA014 3. Simply Typed Lambda Calculus 7
Typing rules
Γ true : Bool (T-True)
Γ false : Bool (T-False)
x : T ∈ Γ
(T-Var)
Γ x : T
Γ, x : T1 t : T2
(T-Abs)
Γ λx.t : T1 → T2
Γ t1 : T1 → T2 Γ t2 : T1
(T-App)
Γ t1 t2 : T2
Γ t1 : Bool Γ t2 : T Γ t3 : T
(T-If)
Γ if t1 then t2 else t3 : T
IA014 3. Simply Typed Lambda Calculus 8
Typing derivation trees
What is the type of λx : Bool → Bool.λy : Bool.x y ?
x : Bool → Bool ∈ {x : Bool → Bool, y : Bool}
x : Bool → Bool, y : Bool x : Bool → Bool
y : Bool ∈ {x : Bool → Bool, y : Bool}
x : Bool → Bool, y : Bool y : Bool
x : Bool → Bool, y : Bool x y : Bool
x : Bool → Bool (λy : Bool.x y) : Bool → Bool
(λx : Bool → Bool.λy : Bool.x y) : (Bool → Bool) → Bool → Bool
Term t is well typed if there exists a type T s.t. t : T
IA014 3. Simply Typed Lambda Calculus 9
Evaluation rules for λ→
(λx : T.t)v → t[x := v]
(E-Abs)
t1 → t1
t1 t2 → t1 t2
(E-App1)
t → t
v t → v t
(E-App2)
Types have no effect on the evaluation!
IA014 3. Simply Typed Lambda Calculus 10
Type safety (soundness)
Type safety: Well-typed terms do not “go wrong”.
(E.g. do not get stuck.)
Safety = progress + preservation
Progress A well-typed term is not stuck.
(It’s either a value, or it can take one more step
according to the evaluation rules.)
Preservation If a well-typed term takes a step of evaluation,
then the resulting term is also well typed.
IA014 3. Simply Typed Lambda Calculus 11
Progress for λ→
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 = λx : T1.t
Theorem (Progress)
Let t be a closed, well-typed term (i.e. ∃T s.t. t : T). Then
either t is a value, or there exists t such that t → t .
IA014 3. Simply Typed Lambda Calculus 12
Preservation for λ→
Lemma (Preservation of types under substitution)
If Γ, x : S t : T and Γ s : S, then Γ t[x := s] : T
Theorem (Preservation)
If Γ t : T and t → t , then Γ t : T
IA014 3. Simply Typed Lambda Calculus 13
Normalization for λ→
Term is normalizable iff its evaluation is guaranteed to halt in a
finite number of steps.
Theorem ((Weak) Normalization for λ→
)
If t : T, then t is normalizable.
• the theorem above is stated for the CBV semantics
• holds also for full β-reduction (strong normalization)
Consequences
• ω = λx.x x is neither strongly nor weakly normalizing
• . . . ω is not typeable (as any term with an infinite
computation), therefore
• . . . λ→is not Turing complete!
IA014 3. Simply Typed Lambda Calculus 14
From λ-calculus to functional
programming II
IA014 3. Simply Typed Lambda Calculus 15
Recursion
Revision (untyped lambda calculus)
G := λf.λn. if n = 0 then 1 else n ∗ (f (n − 1))
fact := FIX G = G (FIX G)
Recursion in λ→
H :=λf : Nat → Bool.λx : Nat.
if iszero x then true
else if iszero (pred x) then false
else f iszero (pred(pred x))
H : (Nat → Bool) → Nat → Bool
iseven := FIX H iseven : Nat → Bool
IA014 3. Simply Typed Lambda Calculus 16
Typing FIX
some combinators for FIX
• Y := λf.(λx.f(x x)) (λx.f(x x))
• Θ := (λxf.f(x x f))(λxf.f(x x f))
What is the type of Y ?
• problem: self-application: λx : T.x x
• the type T would need to be
• a function type
• an argument type (of the same type!)
• FIX is not typeable in λ→
• also follows from normalization for λ→
IA014 3. Simply Typed Lambda Calculus 17
Recursion in λ→
problem: FIX is not typeable in λ→
solution: extend λ→ with a new primitive x
syntax
t ::= . . . terms
| x t fixed point of t
typing
Γ t : T → T (T-Fix)
Γ x t : T
evaluation
x(λx : T1.t2) → t2[x := (x(λx : T1.t2))] (E-FixBeta)
t → t
x t → x t
(E-Fix)
Note: adding x breaks strong normalization!
IA014 3. Simply Typed Lambda Calculus 18
Unit type
syntax
t ::= . . . terms
| unit constant unit
v ::= . . . values
| unit constant unit
T ::= . . . types
| Unit unit type
typing rule
Γ unit : Unit (T-Unit)
• “the most simple” base type
• similar to void in C or Java
• uses: languages with side effects
• if we do not care about the returned value
• value is secondary to the side-effect
IA014 3. Simply Typed Lambda Calculus 19
Sequencing
syntax
t ::= . . . terms
| t1; t2 sequence
typing rule
Γ t1 : Unit Γ t2 : T2
Γ t1; t2 : T2
(T-Seq)
evaluation rules
t1 → t1
t1; t2 → t1; t2
(E-Seq1) unit; t2 → t2 (E-Seq2)
different approach
• t1; t2 is an abbreviation for (λx : Unit. t2) t1
• sequencing is therefore a derived form:
typing and evaluation rules can be derived
• derived forms are syntactic sugar
IA014 3. Simply Typed Lambda Calculus 20
Let bindings
Is let just a derived form?
let x = t1 in t2 := (λx : T1.t2) t1
problem: where to get T1 from? (when desugaring)
answer: the typechecker
...
Γ t1 : T1
...
Γ, x : T1 t2 : T2
(T-Let)
Γ let x = t1 in t2 : T2
converts to
...
Γ t1 : T1
...
Γ, x : T1 t2 : T2
(T-Abs)
Γ λx : T1.t2 : T1 → T2
(T-App)
Γ (λx : T1.t2) t1 : T2
IA014 3. Simply Typed Lambda Calculus 21
Let bindings II
• let is not a derived form in λ→!
• we therefore have to add it externally
syntax
t ::= . . . terms
| let x = t in t let binding
typing rule
Γ t1 : T1 Γ, x : T1 t2 : T2
Γ let x = t1 in t2 : T2
(T-Let)
evaluation rules
let x = v in t → t[x := v] (E-LetV)
t1 → t1
let x = t1 in t2 → let x = t1 in t2
(E-Let)
IA014 3. Simply Typed Lambda Calculus 22
Recursive let bindings
Example
let rec iseven : Nat → Bool =
λx : Nat.
if iszero x then true
else if iszero (pred x) then false
else iseven (pred (pred x))
in
iseven 7;
Note: let in Haskell/ML
non-recursive recursive
ML let let rec
HASKELL – let
let rec is a derived form:
let rec x : T1 = t1 in t2 := let x = x(λx : T1.t1) in t2
IA014 3. Simply Typed Lambda Calculus 23
Pairs
syntax
t ::= . . . terms
| (t, t) pair
| t.1 first projection
| t.2 second projection
v ::= . . . values
| (t, t) pair value
T ::= . . . types
| T1 × T2 product type
typing rules
Γ t1 : T1 Γ t2 : T2
Γ (t1, t2) : T1 × T2
(T-Pair)
Γ t : T1 × T2
Γ t.1 : T1
(T-Proj1)
Γ t : T1 × T2
Γ t.2 : T2
(T-Proj2)
Note: × is a new type constructor
IA014 3. Simply Typed Lambda Calculus 24
Pairs – evaluation
evaluation rules
(v1, v2).1 → v1 (E-PairV1)
(v1, v2).2 → v2 (E-PairV2)
t → t
t.1 → t .1
(E-Proj1)
t → t
t.2 → t .2
(E-Proj2)
t1 → t1
(t1, t2) → (t1, t2)
(E-Pair1)
t2 → t2
(v1, t2) → (v1, t2)
(E-Pair2)
Note: Pairs can be naturally extended to tuples and records.
IA014 3. Simply Typed Lambda Calculus 25
Lists
syntax
t ::= . . . terms
| nil[T] empty list
| cons[T] t t list constructor
| null[T] t test for empty list
| hd[T] t head of a list
| tl[T] t tail of a list
v ::= . . . values
| nil[T] empty list
| cons[T] v v list constructor
T ::= . . . types
| List T type of lists
some typing rules
Γ nil[T] : List T (T-Nil)
Γ t1 : T Γ t2 : List T
Γ cons[T] t1 t2 : List T
(T-Cons)
Try the rest yourselves!
IA014 3. Simply Typed Lambda Calculus 26
Type Ascription
syntax
t ::= . . . terms
| t as T ascription
typing rule
Γ t : T
Γ t as T : T
(T-Asc)
evaluation rules
t → t
t as T → t as T
(E-Asc1) v as T → v (E-Asc2)
• t as T is an assertion that t has type T
• usefull typechecking and documentation purposes
IA014 3. Simply Typed Lambda Calculus 27