Last time
System Fω
K1 is a kind K2 is a kind ⇒-kind
K1 ⇒ K2 is a kind
Γ, α::K1 ⊢ A :: K2 ⇒-intro
Γ ⊢ λα::K1.A :: K1 ⇒ K2
Γ ⊢ A :: K1 ⇒ K2
Γ ⊢ B :: K1 ⇒-elim
Γ ⊢ A B :: K2
(and encoding data types: 1, 2, N, +, lists, nested types and ≡)
1/ 49
This time
Γ ⊢ M : ?
2/ 49
What is type inference?
# fun f g x -> f (g x);;
– : (’a -> ’b) -> (’c -> ’a) -> ’c -> ’b =
3/ 49
What is type inference?
# fun f g x -> f (g x);;
– : (’a -> ’b) -> (’c -> ’a) -> ’c -> ’b =
Goal
succinctness of annotation-free code
+
safety and expressiveness of System Fω
3/ 49
What is type inference?
# fun f g x -> f (g x);;
– : (’a -> ’b) -> (’c -> ’a) -> ’c -> ’b =
Goal
succinctness of annotation-free code
+
safety and expressiveness of System Fω
Bad news
the goal is unachievable
3/ 49
The ML calculus
4/ 49
The ML calculus
Fω
F
??��������
ML
OO
λ→
OO
5/ 49
Prenex quantifification
∀α.α → α
∀α.∀β.α → (β → β)
∀α.(∀β.β → β) → α
∀α.α → (∀β.β → β)
Let-bound polymorphism
l e t id = fun x -> x
in id id
l e t id x = x
in id id
l e t f id = id id
in f (fun x -> x)
(fun id -> id id)
(fun x -> x)
6/ 49
Prenex quantifification
∀α.α → α 3
∀α.∀β.α → (β → β)
∀α.(∀β.β → β) → α
∀α.α → (∀β.β → β)
Let-bound polymorphism
l e t id = fun x -> x
in id id
l e t id x = x
in id id
l e t f id = id id
in f (fun x -> x)
(fun id -> id id)
(fun x -> x)
6/ 49
Prenex quantifification
∀α.α → α 3
∀α.∀β.α → (β → β) 3
∀α.(∀β.β → β) → α
∀α.α → (∀β.β → β)
Let-bound polymorphism
l e t id = fun x -> x
in id id
l e t id x = x
in id id
l e t f id = id id
in f (fun x -> x)
(fun id -> id id)
(fun x -> x)
6/ 49
Prenex quantifification
∀α.α → α 3
∀α.∀β.α → (β → β) 3
∀α.(∀β.β → β) → α 7
∀α.α → (∀β.β → β)
Let-bound polymorphism
l e t id = fun x -> x
in id id
l e t id x = x
in id id
l e t f id = id id
in f (fun x -> x)
(fun id -> id id)
(fun x -> x)
6/ 49
Prenex quantifification
∀α.α → α 3
∀α.∀β.α → (β → β) 3
∀α.(∀β.β → β) → α 7
∀α.α → (∀β.β → β) 7
Let-bound polymorphism
l e t id = fun x -> x
in id id
l e t id x = x
in id id
l e t f id = id id
in f (fun x -> x)
(fun id -> id id)
(fun x -> x)
6/ 49
Prenex quantifification
∀α.α → α 3
∀α.∀β.α → (β → β) 3
∀α.(∀β.β → β) → α 7
∀α.α → (∀β.β → β) 7
Let-bound polymorphism
l e t id = fun x -> x
in id id
3
l e t id x = x
in id id
l e t f id = id id
in f (fun x -> x)
(fun id -> id id)
(fun x -> x)
6/ 49
Prenex quantifification
∀α.α → α 3
∀α.∀β.α → (β → β) 3
∀α.(∀β.β → β) → α 7
∀α.α → (∀β.β → β) 7
Let-bound polymorphism
l e t id = fun x -> x
in id id
3
l e t id x = x
in id id
3
l e t f id = id id
in f (fun x -> x)
(fun id -> id id)
(fun x -> x)
6/ 49
Prenex quantifification
∀α.α → α 3
∀α.∀β.α → (β → β) 3
∀α.(∀β.β → β) → α 7
∀α.α → (∀β.β → β) 7
Let-bound polymorphism
l e t id = fun x -> x
in id id
3
l e t id x = x
in id id
3
l e t f id = id id
in f (fun x -> x)
7
(fun id -> id id)
(fun x -> x)
6/ 49
Prenex quantifification
∀α.α → α 3
∀α.∀β.α → (β → β) 3
∀α.(∀β.β → β) → α 7
∀α.α → (∀β.β → β) 7
Let-bound polymorphism
l e t id = fun x -> x
in id id
3
l e t id x = x
in id id
3
l e t f id = id id
in f (fun x -> x)
7
(fun id -> id id)
(fun x -> x)
7
6/ 49
Types and schemes
B-types
Γ ⊢ B is a type
α ∈ Γ α-types
Γ ⊢ α is a type
Γ ⊢ A is a type
Γ ⊢ B is a type →-types
Γ ⊢ A → B is a type
Γ, α ⊢ A is a type
scheme
Γ ⊢ ∀α.A is a scheme
7/ 49
Environments
Γ-·· is an environment Γ is an environment
Γ ⊢ S is a scheme
Γ-:
Γ, x : S is an environment
8/ 49
Typing rules for →
Γ, x : A ⊢ M : B
→-intro
Γ ⊢ λx .M : A → B
Γ ⊢ M : A → B
Γ ⊢ N : A →-elim
Γ ⊢ M N : B
9/ 49
Typing rules for schemes
Γ ⊢ M : A α ∩ ftv(Γ) = Ø Γ, x : ∀α.A ⊢ N : B
scheme-intro
Γ ⊢ let x = M in N : B
x : ∀α.A ∈ Γ
Γ ⊢ B is a type (for B ∈ B)
scheme-elim
Γ ⊢ x : A[α := B]
10/ 49
Milner’s algorithm
11/ 49
Substitutions
[a1 7→ A1, a2 7→ A2, . . . an 7→ An]
For example, let
σ be [a 7→ B, b 7→ (B → B)]
A be a → b → a
Then
σA is B → (B → B) → B.
If
σA = B (for some σ)
then we say
B is a substitution instance of A.
12/ 49
Constraints
a = b
a → b = B → b
B = B
B = B → B
13/ 49
Unification
unify : ConstraintSet → Substitution
unify(∅) = []
unify({A = A} ∪ C ) = unify(C )
unify({a = A} ∪ C ) = unify([a 7→ A]C ) ◦ [a 7→ A]
when a /∈ ftv(A)
unify({A = a} ∪ C ) = unify([a 7→ A]C ) ◦ [a 7→ A]
when a /∈ ftv(A)
unify({A → B = A′ → B ′} ∪ C ) = unify({A = A′,B = B ′} ∪ C )
unify({A = B} ∪ C ) = FAIL
14/ 49
Algorithm J
J : Environment × Expression → Type
J (Γ, λx.M) = b → A
where A = J (Γ,x:b, M)
and b is fresh
J (Γ, M N) = b
where A = J (Γ, M)
and B = J (Γ, N)
and unify ’ ({A = B → b})
succeeds
and b is fresh
J (Γ, x) = A[α:=b]
where Γ(x) = ∀α.A
and b are fresh
J (Γ, let x = M in N) = B
where A = J (Γ, M)
and B = J (Γ,x:∀α.A, N)
and α = ftv(A) \ ftv(Γ)
15/ 49
Algorithm J in action
J(·, l e t apply = λf.λx.f x in
let id = λy.y in
apply id) =
16/ 49
Algorithm J in action
J(·, l e t apply = λf.λx.f x in
let id = λy.y in
apply id) =
J(·, λf.λx.f x) =
17/ 49
Algorithm J in action
J(·, l e t apply = λf.λx.f x in
let id = λy.y in
apply id) =
J(·, λf.λx.f x) =
J(·,f:b1, λx.f x) =
18/ 49
Algorithm J in action
J(·, l e t apply = λf.λx.f x in
let id = λy.y in
apply id) =
J(·, λf.λx.f x) = b1 → b2 → b3
J(·,f:b1, λx.f x) = b2 → b3
J(·,f:b1,x:b2, f x) = b3
19/ 49
Algorithm J in action
J(·, l e t apply = λf.λx.f x in
let id = λy.y in
apply id) =
J(·, λf.λx.f x) = b1 → b2 → b3
J(·,f:b1, λx.f x) = b2 → b3
J(·,f:b1,x:b2, f x) = b3
J(·,f:b1,x:b2, f) =
20/ 49
Algorithm J in action
J(·, l e t apply = λf.λx.f x in
let id = λy.y in
apply id) =
J(·, λf.λx.f x) = b1 → b2 → b3
J(·,f:b1, λx.f x) = b2 → b3
J(·,f:b1,x:b2, f x) = b3
J(·,f:b1,x:b2, f) = b1
21/ 49
Algorithm J in action
J(·, l e t apply = λf.λx.f x in
let id = λy.y in
apply id) =
J(·, λf.λx.f x) = b1 → b2 → b3
J(·,f:b1, λx.f x) = b2 → b3
J(·,f:b1,x:b2, f x) = b3
J(·,f:b1,x:b2, f) = b1
J(·,f:b1,x:b2, x) =
22/ 49
Algorithm J in action
J(·, l e t apply = λf.λx.f x in
let id = λy.y in
apply id) =
J(·, λf.λx.f x) = b1 → b2 → b3
J(·,f:b1, λx.f x) = b2 → b3
J(·,f:b1,x:b2, f x) = b3
J(·,f:b1,x:b2, f) = b1
J(·,f:b1,x:b2, x) = b2
23/ 49
Algorithm J in action
J(·, l e t apply = λf.λx.f x in
let id = λy.y in
apply id) =
J(·, λf.λx.f x) = b1 → b2 → b3
J(·,f:b1, λx.f x) = b2 → b3
J(·,f:b1,x:b2, f x) = b3
J(·,f:b1,x:b2, f) = b1
J(·,f:b1,x:b2, x) = b2
unify({b1 = b2 → b3}) =
24/ 49
Algorithm J in action
J(·, l e t apply = λf.λx.f x in
let id = λy.y in
apply id) =
J(·, λf.λx.f x) = b1 → b2 → b3
J(·,f:b1, λx.f x) = b2 → b3
J(·,f:b1,x:b2, f x) = b3
J(·,f:b1,x:b2, f) = b1
J(·,f:b1,x:b2, x) = b2
unify({b1 = b2 → b3}) = {b1 7→ b2 → b3}
25/ 49
Algorithm J in action
J(·, l e t apply = λf.λx.f x in
let id = λy.y in
apply id) =
J(·, λf.λx.f x) = (b2 → b3) → b2 → b3
J(·,f:b2 → b3, λx.f x) = b2 → b3
J(·,f:b2 → b3,x:b2, f x) = b3
J(·,f:b2 → b3,x:b2, f) = b2 → b3
J(·,f:b2 → b3,x:b2, x) = b2
unify({b1 = b2 → b3}) = {b1 7→ b2 → b3}
26/ 49
Algorithm J in action
J(·, l e t apply = λf.λx.f x in
let id = λy.y in
apply id) =
J(·, λf.λx.f x) = (b2 → b3) → b2 → b3
J(·,f:b2 → b3, λx.f x) = b2 → b3
J(·,f:b2 → b3,x:b2, f x) = b3
J(·,f:b2 → b3,x:b2, f) = b2 → b3
J(·,f:b2 → b3,x:b2, x) = b2
ftv((b2 → b3)→ b2 → b3) = {b2, b3}
ftv(·) = {}
{b2, b3} \ {} = {b2, b3}
27/ 49
Algorithm J in action
J(·, l e t apply = λf.λx.f x in
let id = λy.y in
apply id) =
J(·, λf.λx.f x) = (b2 → b3) → b2 → b3
J(·,apply:∀α2α3.(α2 → α3)→ α2 → α3,
l e t id = λy.y in apply id) =
28/ 49
Algorithm J in action
J(·, l e t apply = λf.λx.f x in
let id = λy.y in
apply id) =
J(·, λf.λx.f x) = (b2 → b3) → b2 → b3
J(·,apply:∀α2α3.(α2 → α3)→ α2 → α3,
l e t id = λy.y in apply id) =
J(·,apply:∀α2α3.(α2 → α3)→ α2 → α3,
λy.y) =
29/ 49
Algorithm J in action
J(·, l e t apply = λf.λx.f x in
let id = λy.y in
apply id) =
J(·, λf.λx.f x) = (b2 → b3) → b2 → b3
J(·,apply:∀α2α3.(α2 → α3)→ α2 → α3,
l e t id = λy.y in apply id) =
J(·,apply:∀α2α3.(α2 → α3)→ α2 → α3,
λy.y) = b4 → b4
J(·,apply:∀α2α3.(α2 → α3)→ α2 → α3,y:b4, y)
= b4
30/ 49
Algorithm J in action
J(·, l e t apply = λf.λx.f x in
let id = λy.y in
apply id) =
J(·, λf.λx.f x) = (b2 → b3) → b2 → b3
J(·,apply:∀α2α3.(α2 → α3)→ α2 → α3,
l e t id = λy.y in apply id) =
J(·,apply:∀α2α3.(α2 → α3)→ α2 → α3,
λy.y) = b4 → b4
ftv(b4 → b4) = {b4}
ftv(·,apply:∀α2α3.(α2 → α3) → α2 → α3) = {}
{b4} \ {} = {b4}
31/ 49
Algorithm J in action
J(·, l e t apply = λf.λx.f x in
let id = λy.y in
apply id) =
J(·, λf.λx.f x) = (b2 → b3) → b2 → b3
J(·,apply:∀α2α3.(α2 → α3)→ α2 → α3,
l e t id = λy.y in apply id) =
J(·,apply:∀α2α3.(α2 → α3)→ α2 → α3,
λy.y) = b4 → b4
J(·, apply:∀α2α3.(α2 → α3) → α2 → α3,id:∀α4.α4 → α4,
apply id) = b5
32/ 49
Algorithm J in action
J(·, l e t apply = λf.λx.f x in
let id = λy.y in
apply id) =
J(·, λf.λx.f x) = (b2 → b3) → b2 → b3
J(·,apply:∀α2α3.(α2 → α3)→ α2 → α3,
l e t id = λy.y in apply id) =
J(·,apply:∀α2α3.(α2 → α3)→ α2 → α3,
λy.y) = b4 → b4
J(·, apply:∀α2α3.(α2 → α3) → α2 → α3,id:∀α4.α4 → α4,
apply id) = b5
J(·, apply:∀α2α3.(α2 → α3) → α2 → α3,
id:∀α4.α4 → α4, apply)
= (b6 → b7)→ b6 → b7
33/ 49
Algorithm J in action
J(·, l e t apply = λf.λx.f x in
let id = λy.y in
apply id) =
J(·, λf.λx.f x) = (b2 → b3) → b2 → b3
J(·,apply:∀α2α3.(α2 → α3)→ α2 → α3,
l e t id = λy.y in apply id) =
J(·,apply:∀α2α3.(α2 → α3)→ α2 → α3,
λy.y) = b4 → b4
J(·, apply:∀α2α3.(α2 → α3) → α2 → α3,id:∀α4.α4 → α4,
apply id) = b5
J(·, apply:∀α2α3.(α2 → α3) → α2 → α3,
id:∀α4.α4 → α4, apply)
= (b6 → b7)→ b6 → b7
J(·, apply:∀α2α3.(α2 → α3) → α2 → α3,
id:∀α4.α4 → α4, id)
= b8 → b8
34/ 49
Algorithm J in action
unify ({(b6 → b7)→ b6 → b7 = (b8 → b8) → b5})
35/ 49
Algorithm J in action
unify ({(b6 → b7)→ b6 → b7 = (b8 → b8) → b5})
= unify ({b6 → b7 = b8 → b8,
b6 → b7 = b5})
36/ 49
Algorithm J in action
unify ({(b6 → b7)→ b6 → b7 = (b8 → b8) → b5})
= unify ({b6 → b7 = b8 → b8,
b6 → b7 = b5})
= unify ({b6 = b8,
b7 = b8,
b6 → b7 = b5})
37/ 49
Algorithm J in action
unify ({(b6 → b7)→ b6 → b7 = (b8 → b8) → b5})
= unify ({b6 → b7 = b8 → b8,
b6 → b7 = b5})
= unify ({b6 = b8,
b7 = b8,
b6 → b7 = b5})
= {b6 7→ b8, b7 7→ b8, b5 7→ b6 → b7}
38/ 49
Algorithm J in action
J(·, l e t apply = λf.λx.f x in
let id = λy.y in
apply id) =
J(·, λf.λx.f x) = (b2 → b3) → b2 → b3
J(·,apply:∀α2α3.(α2 → α3)→ α2 → α3,
l e t id = λy.y in apply id) =
J(·,apply:∀α2α3.(α2 → α3)→ α2 → α3,
λy.y) = b4 → b4
J(·, apply:∀α2α3.(α2 → α3) → α2 → α3,id:∀α4.α4 → α4,
apply id) = b5
J(·, apply:∀α2α3.(α2 → α3) → α2 → α3,
id:∀α4.α4 → α4, apply)
= (b6 → b7)→ b6 → b7
J(·, apply:∀α2α3.(α2 → α3) → α2 → α3,
id:∀α4.α4 → α4, id)
= b8 → b8
39/ 49
Algorithm J in action
J(·, l e t apply = λf.λx.f x in
let id = λy.y in
apply id) =
J(·, λf.λx.f x) = (b2 → b3) → b2 → b3
J(·,apply:∀α2α3.(α2 → α3)→ α2 → α3,
l e t id = λy.y in apply id) =
J(·,apply:∀α2α3.(α2 → α3)→ α2 → α3,
λy.y) = b4 → b4
J(·, apply:∀α2α3.(α2 → α3) → α2 → α3,id:∀α4.α4 → α4,
apply id) = b8 → b8
J(·, apply:∀α2α3.(α2 → α3) → α2 → α3,
id:∀α4.α4 → α4, apply)
= (b8 → b8)→ b8 → b8
J(·, apply:∀α2α3.(α2 → α3) → α2 → α3,
id:∀α4.α4 → α4, id)
= b8 → b8
40/ 49
Algorithm J in action
J(·, l e t apply = λf.λx.f x in
let id = λy.y in
apply id) =
J(·, λf.λx.f x) = (b2 → b3) → b2 → b3
J(·,apply:∀α2α3.(α2 → α3)→ α2 → α3,
l e t id = λy.y in apply id) =
J(·,apply:∀α2α3.(α2 → α3)→ α2 → α3,
λy.y) = b4 → b4
J(·, apply:∀α2α3.(α2 → α3) → α2 → α3,id:∀α4.α4 → α4,
apply id) = b8 → b8
41/ 49
Algorithm J in action
J(·, l e t apply = λf.λx.f x in
let id = λy.y in
apply id) =
J(·, λf.λx.f x) = (b2 → b3) → b2 → b3
J(·,apply:∀α2α3.(α2 → α3)→ α2 → α3,
l e t id = λy.y in apply id) = b8 → b8
J(·, apply:∀α2α3.(α2 → α3) → α2 → α3,id:∀α4.α4 → α4,
apply id) = b8 → b8
42/ 49
Algorithm J in action
J(·, l e t apply = λf.λx.f x in
let id = λy.y in
apply id) = b8 → b8
43/ 49
Type inference in practice
44/ 49
Type inference and recursion
Γ, x : A ⊢ M : A α /∈ ftv(Γ) Γ, x : ∀α.A ⊢ N : B
let-rec
Γ ⊢ let rec x = M in N : B
45/ 49
Supporting imperative programming: the value restriction
type ’a ref = { mutable contents : ’a }
val ref : ’a -> ’a ref
val ( ! ) : ’a ref -> ’a
val (:=) : ’a ref -> ’a -> unit
l e t r = ref None in
r := Some “boom”;
match !r with
None -> ()
| Some f -> f ()
46/ 49
Relaxing the value restriction: variance
type ’a printer = ’a -> string
(’a -> ’b) -> ’a printer -> ’b printer list
→
→
α+ β
−
→
printer
α+
list
printer
β−
47/ 49
Relaxing the value restriction: the rules
Should we generalize?
▶ covariant type variables
▶ invariant type variables
▶ contravariant type variables
▶ bivariant type variables
48/ 49
Relaxing the value restriction: the rules
Should we generalize?
▶ covariant type variables 3
▶ invariant type variables
▶ contravariant type variables
▶ bivariant type variables
48/ 49
Relaxing the value restriction: the rules
Should we generalize?
▶ covariant type variables 3
▶ invariant type variables 7
▶ contravariant type variables
▶ bivariant type variables
48/ 49
Relaxing the value restriction: the rules
Should we generalize?
▶ covariant type variables 3
▶ invariant type variables 7
▶ contravariant type variables 7
▶ bivariant type variables
48/ 49
Relaxing the value restriction: the rules
Should we generalize?
▶ covariant type variables 3
▶ invariant type variables 7
▶ contravariant type variables 7
▶ bivariant type variables 3
48/ 49
Next time
Γ ⊢ M : A → B
Γ ⊢ N : A
Γ ⊢ M N : B
Γ ⊢ A → B
Γ ⊢ A
Γ ⊢ B
49/ 49