程序代写代做代考 scheme algorithm Last time

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

??��������

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