IA014: Advanced Functional
Programming
4. Polymorphism and Type Inference
Jan Obdržálek obdrzalek@fi.muni.cz
Faculty of Informatics, Masaryk University, Brno
IA014 4. Polymorphism and Type Inference 1
Polymorphism I
IA014 4. Polymorphism and Type Inference 2
Motivation
Typing id ≡ λx. x
• In λ→:
(λx : Nat. x) : Nat → Nat
(λx : Bool. x) : Bool → Bool
· · ·
• What we really mean:
(λx. x) : ∀α.α → α
• In HASKELL:
Prelude > :info id
id :: a -> a -- Defined in `GHC.Base '
IA014 4. Polymorphism and Type Inference 3
More examples
double := λf.λx.f(f x) : ∀α.(α → α) → α → α
Lists
• null : ∀α.[α] → Bool
• nil : ∀α.[α]
• cons : ∀α.α → ([α] → [α])
• hd : ∀α.[α] → α
• tl : ∀α.[α] → [α]
IA014 4. Polymorphism and Type Inference 4
Polymorphism
The id ≡ λx. x function is, by its nature, polymorphic.
Types of polymorphism
• parametric polymorphism
• “all types”
• Allows single piece of code to be typed parametrically, i.e.
using type variables, and instantiated when needed.
• All instances behave the same.
• ad-hoc polymorphism
• “some types”
• overloading: one function has many implementations
(differeng by the types of the arguments)
• May behave differently for different types of arguments.
Goal: extend λ-calculus with parametric polymorphism
so we can use functions like id
IA014 4. Polymorphism and Type Inference 5
Extending λ – syntax
System HM (Hindley-Milner)
term and values
t ::= x variable
| t t application
| λx.t abstraction
| let x = t in t let binding
monotypes
T ::= α type variable
| T → T function type
type schemes (polytypes)
S ::= T monotype
| ∀α.T generic type
IA014 4. Polymorphism and Type Inference 6
Type variables and schemes
T ::= α | T → T S ::= T | ∀α.T
Type variables
• α, α , β . . .
• can stand for any monotype
• we assume we have an infinite supply of type variables
Type schemes
• either a monotype T or a generic type ∀α1 . . . ∀αn.T
• α1, . . . , αn are generic type variables
• notions of free/bound type variables (notation FV (S))
• can be instantiated
IA014 4. Polymorphism and Type Inference 7
Type substitution/instantiation
substitution
• mapping from type variables to types
• notation: θ = {T1/α1, . . . , Tn/αn}
• θS – application to a type scheme S
• replace each free occurrence of αi in S with Ti
• rename generic variables if necessary
• θS is an instance of S
• naturally extends to contexts:
θ(Γ) = θ(x1 : T1, . . . , xk : Tk) = x1 : θT1, . . . , xk : θTk
• can be composed: θ2θ1S
IA014 4. Polymorphism and Type Inference 8
Type ordering
What is the relationship among the many types of id ≡ λx.x?
∀α.α → α Nat → Nat (Nat → Nat) → (Nat → Nat)
• ∀α.α → α is more general than any of the others
• Nat → Nat is more specialized than ∀α.α → α
• we write ∀α.α → α Nat → Nat
Specialization rule
T = {Ti/αi}T βi ∈ FV (∀α1 . . . ∀αn.T)
∀α1 . . . ∀αn.T ∀β1 . . . ∀βm.T
• ∀β1 . . . ∀βm.T is an instance of ∀α1 . . . ∀αn.T
IA014 4. Polymorphism and Type Inference 9
Type inference
IA014 4. Polymorphism and Type Inference 10
Motivation
Two flavours of λ→
• Implicitly typed
• Haskell B. Curry, 1934
• I = (λx.x) : A → A
• I = (λx.x) : (A → B) → (A → B)
• Explicitly typed
• Alonzo Church, 1940
• IA = (λx : A.x) : A → A
• IA→B = (λx : (A → B).x) : (A → B) → (A → B)
Goal: Support implicit typing
To do this, we must be able to automatically infer (reconstruct)
types of terms.
IA014 4. Polymorphism and Type Inference 11
Type inference (reconstruction)
• The goal is to automatically derive types for the term.
• At the heart of e.g. ML and HASKELL.
• Also used for type-checking.
Some of the types may be given explicitly.
Hindley-Milner algorithm
• first discovered by Hindley (1969)
• in the context of ML rediscovered by Milner (1978)
• formal analysis and proofs: Milner and Damas (1982)
• also called Damas-Hindley-Milner algorithm
• works for lambda calculus with let-polymorphism
IA014 4. Polymorphism and Type Inference 12
Type inference idea
What is the type of λx. succ x?
• Assume Γ = succ : Nat → Nat
• We do not know the type of x (yet) so we put x : α
• From environment we know that succ : Nat → Nat
• For succ to be applied to x we need x to be of type Nat
• Solution: substitution θ = {Nat/α}.
What about let id = λx.x in (id false, id 0)?
• We do not know the type of x (yet) so we put x : α
• Therefore id : α → α
• On let-binding we generalize this to ∀α : α → α
• For each use of id we instantiate α with a fresh variable
say β → β in the first case and γ → γ in the second
• β gets unified with Bool and γ with Nat
• the sought-for type is therefore (Bool, Nat).
IA014 4. Polymorphism and Type Inference 13
System HM – Typing rules
x : S ∈ Γ
Γ x : S
(T-Var)
Γ, x : T1 t : T2
Γ λx.t : T1 → T2
(T-Abs)
Γ t1 : T1 → T2 Γ t2 : T1
Γ t1 t2 : T2
(T-App)
Γ t1 : S Γ, x : S t2 : T
Γ let x = t1 in t2 : T
(T-Let)
Γ t : S S S
Γ t : S
(T-Inst)
Γ t : S α ∈ FV (Γ)
Γ t : ∀α.S
(T-Gen)
Observation
• The first four rules are syntax driven.
• We have a choice for T-Inst and T-Gen.
IA014 4. Polymorphism and Type Inference 14
Let polymorphism
T-Abs vs T-Let
• no type can be inferred for λf.(f true, f 0)
• type of let f = λx.x in (f true, f 0) is (Bool, Nat)
The rules on previous slide give so-called let polymorphism
• type of parametric polymorphism
• let-expressions allow local bindings to have polymorphic
types
that’s why let is in the syntax!
• λ-bound variables are always assumed to be monotypes
• let-bound variables can have polymorphic types, because
we know what they are bound to
• strikes balance between expressivity and decidability
IA014 4. Polymorphism and Type Inference 15
Type inference examples
(1) Show Γ id n : Nat for Γ = id : ∀α.α → α, n : Nat
id : ∀α.α → α ∈ Γ
(T-Var)
Γ id : ∀α.α → α ∀α.α → α Nat → Nat
(T-Inst)
Γ id : Nat → Nat
n : Nat ∈ Γ
(T-Var)
Γ n : Nat (T-App)
Γ id n : Nat
(2) Show let id = λx.x in id : ∀α.α → α
x : α ∈ {x : α}
(T-Var)
x : α x : α(T-Abs)
λx.x : α → α(T-Gen)
λx.x : ∀α.α → α
id : ∀α.α → α ∈ {id : ∀α.α → α}
(T-Var)
id : ∀α.α → α id : ∀α.α → α(T-Let)
let id = λx.x in id : ∀α.α → α
IA014 4. Polymorphism and Type Inference 16
Combining rules
To get an algorithm, it would be nice if the type system is completely
syntax directed.
T-Inst
We can instantiate when we introduce a variable:
x : S ∈ Γ S S
Γ x : S’
(T-Var’)
T-Gen
We can generalize immediately at the level of let expressions:
Γ t1 : S Γ, x : ∀α.S t2 : T
Γ let x = t1 in t2 : T
(T-Let’)
where α = FV (S) FV (Γ) (generalizing as far as possible)
IA014 4. Polymorphism and Type Inference 17
Algorithm W
Algorithm W
INPUT: a context Γ and a term t
OUTPUT: substitution θ and a type T, such that θΓ t : T
• We will follow [Damas, Milner 1982].
• Along the rules of the type system.
• Uses the unification algorithm of Robinson (1965).
IA014 4. Polymorphism and Type Inference 18
Unification
INPUT: types T1 and T2
OUTPUT: substitution θ (called unifier) such that θT1 = θT2
or fail if such θ does not exist
unify α T2 = if α ∈ FV (T2) then {T2/α} else fail
unify T1 α = if α ∈ FV (T1) then {T1/α} else fail
unify S1 → S1 S2 → S2 = let θ1 = unify S1 S2
θ2 = unify θ1(S1) θ1(S2)
in θ2θ1
unify _ _ = fail
Theorem (Robinson)
Let θ = unify(T1, T2) and κ another unifier of T1 and T2. Then
there exist θ such that κ = θ θ.
In other words, θ is the most general unifier.
IA014 4. Polymorphism and Type Inference 19
Algorithm W (1)
x : S ∈ Γ S S
Γ x : S
(T-Var’)
W(Γ, x) = (θid, inst(T)) where x : T ∈ Γ
inst(∀α1 . . . αn.T) = {β1/α1, . . . , βn/αn}T where β1, . . . , βn are fresh
Γ t1 : T1 → T2 Γ t2 : T1
Γ t1 t2 : T2
(T-App)
W(Γ, t1 t2) = let (θ1, T1) = W(Γ, t1)
(θ2, T2) = W(θ1Γ, t2)
θ3 = unify(θ2T1, T2 → β) where β is fresh
in (θ3θ2θ1, θ3β)
IA014 4. Polymorphism and Type Inference 20
Algorithm W (2)
Γ, x : T1 t : T2
Γ λx.t : T1 → T2
(T-Abs)
W(Γ, λx.t) = let (θ, T) = W(Γ ∪ {x : β}, t) where β is fresh
in (θ, θ(β → T))
Γ t1 : S Γ, x : ∀α.S t2 : T
Γ let x = t1 in t2 : T
(T-Let)
W(Γ, let x = t1 in t2) = let (θ1, T1) = W(Γ, t1)
(θ2, T2) = W(θ1Γ ∪ {x : gen(θ1Γ, T1)}, t2)
in (θ2θ1, T2)
gen(Γ, T) = ∀α.T where α = FV (T) FV (Γ)
IA014 4. Polymorphism and Type Inference 21
Algorithm W (complete)
W(Γ, x) = (θid, inst(T)) where x : T ∈ Γ
W(Γ, t1 t2) = let (θ1, T1) = W(Γ, t1)
(θ2, T2) = W(θ1Γ, t2)
θ3 = unify(θ2T1, T2 → β) where β is fresh
in (θ3θ2θ1, θ3β)
W(Γ, λx.t) = let (θ, T) = W(Γ ∪ {x : β}, t) where β is fresh
in (θ, θ(β → T))
W(Γ, let x = t1 in t2) = let (θ1, T1) = W(Γ, t1)
(θ2, T2) = W(θ1Γ ∪ {x : gen(θ1Γ, T1)}, t2)
in (θ2θ1, T2)
gen(Γ, T) = ∀α.T where α = FV (T) FV (Γ)
inst(∀α1 . . . αn.T) = {β1/α1, . . . , βn/αn}T where β1, . . . .βn are fresh
IA014 4. Polymorphism and Type Inference 22
Algorithm W – properties
Theorem (Soundness of W)
If W(Γ, t) = (θ, T) then θΓ t : T
S is a principal type scheme of t under Γ iff
1 Γ t : S
2 for every other S such that Γ t : S we have S S
Theorem (Completeness of W)
If Γ t : T for some T then W(Γ, t) = (θ, T ), and, moreover
T T (i.e. W finds a principal type scheme for t under Γ)
IA014 4. Polymorphism and Type Inference 23
Algorithm W
Time complexity?
• proven to be DEXPTIME-hard
• non-linear behaviour manifests only on pathological inputs
• polynomial if depth of let nesting is bounded
IA014 4. Polymorphism and Type Inference 24
Alternative approach to type inference
• Let’s look at some terms:
• t1 t2: for this to typecheck, t1 must be of type α → β, t2 of
type α and t1 t2 of type β
• t1 + t2: for this to typecheck, t1 must be of type Nat, t2 of
type Nat and t1 + t2 of type Nat
• . . . these are constraints!
• If we solve the constraint system, we have our typing.
Constraint generation
• label each term with a new type variable
• generate constraints according to rules above
• example 1: t1 t2
• type variables: t1 : α1, t2 : α2, t1 t2 : β
• constraints: α1 = α2 → β
• example 2: t1 + t2
• type variables: t1 : α1, t2 : α2, t1 + t2 : β
• constraints: α1 = Nat, α2 = Nat, β = Nat
IA014 4. Polymorphism and Type Inference 25
Constraint generation
Select rules
term type constraints
1, 2, 3, . . . Nat
false Bool
nil List α
t1 t2 β t1 : α → β, t2 : α
λx.t α → β x : α, t : β
t1 + t2 Nat t1 : Nat, t2 : Nat
t1 ∗ t2 Nat t1 : Nat, t2 : Nat
if t1 then t2 else t3 α t1 : Bool, t2 : α, t3 : α
hd t α t : List α
tl t List α t : List α
cons t1 t2 List α t1 : α, t2 : List α
IA014 4. Polymorphism and Type Inference 26
Polymorphism II – Beyond HM
IA014 4. Polymorphism and Type Inference 27
Typing recursion in HM
Problem: Y is not typeable in HM
Solution:
• add x of type ∀α.(α → α) → α
• together with the appropriate typing and evaluation rules
• let rec is then defined using let and x
• see extensions to λ→(Lecture 3)
IA014 4. Polymorphism and Type Inference 28
Other terms not typeable in HM
What is the type of λf.(f true, f 0)?
• (∀α.α → α) → (Bool, Nat) ?
• (∀α.α → Nat) → (Nat, Nat) ?
• (∀α.α → β) → (β, β) ?
In all cases, the argument is a “normal” polymorphic function.
Church numerals
• 0 := λf.λx.x
• 1 := λf.λx.f x
• . . .
• n := λf.λx.fn
(x)
Type of n? ∀α : (α → α) → α → α
Now try to type succ := λn.λf.λx.f (n f x) !
IA014 4. Polymorphism and Type Inference 29
Type rank
Rank
• Universally quantified types have rank 1.
• Functions of rank n have at least one argument of rank n-1,
but no arguments of a higher rank.
examples
∀α.α → α rank 1
(∀α.α → α) → Nat rank 2
Nat → (∀α.α → α) → Nat → Nat rank 2
((∀α.α → α) → Nat) → Nat rank 3
Note: System HM: only rank 1 types!
IA014 4. Polymorphism and Type Inference 30
System F – syntax
term and values
t ::= x variable
| t t application
| λx : T.t abstraction
| Λα.t type abstraction
| t [T] type application
v ::= λx : T.t abstraction value
| Λα.t type abstraction value
types
T ::= α type variable
| T → T function type
| ∀α.T universal type
IA014 4. Polymorphism and Type Inference 31
System F – typing and evaluation
We need to extend λ→with the following rules:
typing
Γ t : T α ∈ FV (Γ)
Γ Λα.t : ∀α.T
(T-TAbs) (T-Gen)
Γ t : ∀α.T1
Γ t [T2] : {T2/α}T1
(T-TApp) (T-Inst)
evaluation
t → t
t [T] → t [T]
(E-Tapp)
(Λα.t) [T] → {T/α}t (E-TappTabs)
IA014 4. Polymorphism and Type Inference 32
System F – examples
Identity
id = Λα.λx : α.x id : ∀α.α → α
id [Nat] : Nat → Nat (id [Nat] 0) → 0
id [Bool] : Bool → Bool
double = Λα.λf : α → α.λx : α.f (f x)
double : ∀α.(α → α) → α → α
double [Nat] : (Nat → Nat) → Nat → Nat
quadruple = Λα. double [α → α] (double [α])
quadruple : ∀α.(α → α) → α → α
IA014 4. Polymorphism and Type Inference 33
Typing self-application and recursion
Recall: ω = λx.x x is not typeable in λ→
self = λx : ∀α.α → α.x [∀α.α → α] x
self : (∀α.α → α) → (∀α.α → α)
Evaluation
self id → id [∀α.α → α] id =
(Λβ.λy : β.y) [∀α.α → α] id →
(λy : (∀α.α → α).y) id →
id
Typing Y / x
Easy peasy: x : ∀α.(α → α) → α !
IA014 4. Polymorphism and Type Inference 34
System F – Type safety
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 .
Theorem (Preservation)
If Γ t : T and t → t , then Γ t : T
Proofs of both theorems are simple extensions of the
corresponding proofs for λ→.
IA014 4. Polymorphism and Type Inference 35
System F – Normalization
Theorem (Normalization)
Well-typed System F terms are (strongly) normalizing.
Proof.
Actually quite difficult and surprising [Girard 1972].
IA014 4. Polymorphism and Type Inference 36
System F – Type inference
Type erasing
erase(x) = x
erase(λx : T.t) = λx. erase(t)
erase(t1 t2) = erase(t1) erase(t2)
erase(Λα.t) = erase(t)
erase(t [T]) = erase(t)
Theorem (Wells 1994)
It is undecidable whether, given a closed term M of the untyped
lambda-calculus, there is some well-typed term t in System F
s.t. erase(t) = M.
Note:Type-checking is decidable.
IA014 4. Polymorphism and Type Inference 37
System F – type inference 2
Theorem (Kfoury, Wells 1999)
Type reconstruction for rank ≥ 3 is undecidable.
Practical solutions
• limit your language to rank 1 types
• approach of ML and HASKELL98
• limit your language to rank 2 types
• the complexity of type inference is the same as for
HINDLEY-MILNER
• use System F and provide some type information
• approach of HASKELL
IA014 4. Polymorphism and Type Inference 38
Beyond System F
IA014 4. Polymorphism and Type Inference 39
Lambda cube
• classification of type
systems
• starts with λ→
• extensions:
1 polymorphic types
2 type operations
3 dependent types
• λ2 – System F
IA014 4. Polymorphism and Type Inference 40
Dependencies between types and terms
• terms depending on terms
normal functions
• terms depending on types
polymorphism
• types depending on types
type operators
• types depending on terms
dependent types
IA014 4. Polymorphism and Type Inference 41
Corners of the Lambda cube
λ→
– simply typed lambda
calculus
λ2 – polymorphic lambda
calculus (System F)
λω – simply typed lambda
calculus with type operators
λω – System Fω
λPω – calculus of constructions
λP – dependent types (LF)
All eight are strongly normalizing!
IA014 4. Polymorphism and Type Inference 42