1Simple Type Inference
1
Announcements
n Quiz 5
n Still grading HW4, sorry
n HW6 will be up soon
n I will work on paper list, guidelines and
presentation schedule over weekend
2
2
2Outline
n Simple type inference
n Expressions, types and type environment
n Goal and intuition
n Equality constraints (next time)
n Substitution (next time)
n Robinson’s unification (next time)
n Type inference strategies (next time)
n Algorithm V (Strategy One) and
n Algorithm V (Strategy Two)
3Programming in Haskell, A Milanova
3
Type Inference
Programming in Haskell, A Milanova (slide text due to
Simon Peyton Jones) 4
The task of type inference is to
Reject bad programs with a decent error message
Elaborate good programs
4
3Type Inference
Programming in Haskell, A Milanova 5
> twice = \f -> \x -> f (f x)
> :t twice
Every well-formed expression in Haskell has a type
In general, we don’t need to write type signatures, Haskell
can figure out (many) signatures. E.g.:
> fun = \x -> \y -> x
> :t fun
5
Programming in Haskell, A Milanova 6
Foundation is an algorithm known as Hindley Milner type
inference (also, Damas Milner)
Haskell builds on Hindley Milner to account for, most
notably, user-defined types, ADTs and pattern matching,
type classes and type class constraints
Classical Hindley Milner solves constraints on-the-fly
Haskell first generates constraints, then solves them
“offline”
6
4Simple Type Inference
7
Inference of simple types
Formally known as System F1 or Simply Typed Lambda
Calculus
NO polymorphism, i.e., functions work on a single type
Hindley Milner extends simple type inference with so-
called let-polymorphism. Functions work on many different
types
Important concepts: expressions and types, type
environment, equality constraints, substitution, unification
Programming in Haskell, A Milanova
7
Expressions
Programming in Haskell, A Milanova 8
E ::= c | x | lx.E | E1 E2 |
E1 + E2 | E1 = E2 |
if E1 then E2 else E3 |
let x = E1 in E2
Language of the Simply Typed Lambda calculus:
For the purposes of type inference, there are no types in
syntax
The type of each subexpression is derived by simple type
inference
8
5The Let Construct
let x = E1 in E2
Typing rule:
In the dynamic semantics, it is equivalent to (lx.E2) E1
In the static semantics, it is not equivalent to (lx.E2) E1
n In let, type of “argument” E1 is inferred/checked before the type of
function body E2
n let construct enables Hindley Milner style polymorphism!
Program Analysis CSCI 4450/6450, A Milanova 9
Γ |- E1 : σ Γ,x:σ |- E2 : τ
Γ |- let x = E1 in E2 : τ
9
The Letrec Construct
letrec x = E1 in E2
x can be referenced from within E1
extends calculus with general recursion
Haskell’s let is a letrec actually…
E.g.,
letrec plus = lx.ly. if (x=0) then y else ((plus x-1) y+1)
Or in Haskell:
letrec plus x y = if (x=0) then y else plus (x-1) (y+1)
10
10
6Types
Programming in Haskell, A Milanova 11
τ ::= b | τ1® τ2 | t
Types (as known as simple types or monotypes):
t is a type variable
(tyvar)
b is a base type
Assume Int and Bool
11
Type Environment
Programming in Haskell, A Milanova 12
Gamma ::= Identifiers -> Types
Type environment Gamma maps identifiers (variables) to
types:
For example, we can only type subexpression
(f x)
in a type environment that binds identifies f and x to
types. E.g., in Gamma = [f :: t -> t, x :: t]
12
7Goal and Intuition
Programming in Haskell, A Milanova 13
\x -> \y -> xGiven
\x -> \y -> x :: t1 -> t2 -> t1Deduce
1. Construct parse tree for expression. Associate a fresh
tyvar to each identifier and each subexpression
2. Generate equality constraints
3. Solve equality constraints using unification
4. Deduce type for expression
13
Programming in Haskell, A Milanova 14
\x -> \y -> x
14
8Programming in Haskell, A Milanova 15
\f -> \x -> f (f x)
15
Programming in Haskell, A Milanova 16
(\f -> f 5) (\x -> x + 1)
16
9Programming in Haskell, A Milanova 17
let f = \x -> x in f 1
17
Equality Constraints
Programming in Haskell, A Milanova 18
Two key concepts
§ Equality
§ What does it mean for two types to be equal?
§ Structural equality
§ Unification
§ Can two types be made equal by choosing appropriate
substitutions for their type variables?
§ Robinson’s unification algorithm
18
10
What does it mean for two types τa and τb to be equal?
Structural equality
Suppose τa = t1 ® t2
τb = t3 ® t4
Structural equality entails
τa ~ τb means t1 ® t2 ~ t3 ® t4 iff t1 ~ t3 and t2 ~ t4
19Programming in Haskell, A Milanova (based on MIT 2015 Program Analysis OCW)
19
Can two types be made equal by choosing appropriate
substitutions for their type variables?
Robinson’s unification algorithm
Suppose τa = Int®t1
τb = t2®Bool
Can we unify τa and τb?
Suppose τa = Int ®t1
τb = Bool®Bool
Can we unify τa and τb?
20
Yes, if Bool/t1 and Int/t2
No.
Programming in Haskell, A Milanova (based on MIT 2015 Program Analysis OCW)
20
11
Example
t1® Bool ~ (Int ® t2) ® t3
Programming in Haskell, A Milanova 21
® ®
t1 Bool ®
Int t2
t3
Yes, if Int®t2/t1 and Bool/t3
21
Substitution
Language of types
τ ::= b // base type: Int and Bool
| t // type variable (tyvar)
| τ1 ® τ2 // function type
A substitution is a map
S : Type Variable à Type
S = [τ1/t1, … τn/tn] // substitute type τi for tyvar ti
A substitution instance τ’ = S τ
S = [ t0®Bool / t1 ] τ = t1®t1 then
S τ = S(t1®t1) = (t0®Bool) ® (t0®Bool)
Programming in Haskell, A Milanova (based on MIT 2015 Program Analysis OCW) 22
22
12
Substitutions can be composed
S1 = [ t0®Bool/t1 ]
S2 = [ Int/t0 ]
τ = t1®t1
S2 S1 τ = S2 ( S1(t1®t1) ) = ?
Programming in Haskell, A Milanova 23
Exercises
23
Substitutions can be composed
S1 = [ tx/t1 ]
S2 = [ tx/t2 ]
τ = t2®t1
S2 S1 τ = ?
Programming in Haskell, A Milanova 24
24
13
Substitutions can be composed
S1 = [ t1/t2 ]
S2 = [ t3/t1 ]
S3 = [ t4®Int/t3 ]
τ = t1®t2
S3 S2 S1 τ = ?
Programming in Haskell, A Milanova 25
25
Principal Unifier
A unifier is a substitution that unifies (i.e., makes equal) a set of
constraints
A principal unifier is a most general unifier of a set of
constraints
{ (t1®t1)®t1®t1 ~ t2®t3 }
Programming in Haskell, A Milanova 26
26
14
Exercise
A principal unifier is the most general unifier of a set of
constraints
Find principal unifiers (when they exist) for
{ Int®Int ~ t1®t2 }
{ Int ~ Int®t2 }
{ t1 ~ Int®t2 }
{ t1 ~ Int, t2 ~ t1®t1 }
{ t1®t2 ~ t2®t3, t3 ~ t4®t5 }
Programming in Haskell, A Milanova 27
27
Unification
n Unify: tries to unify τ1 and τ2 and returns a principal
unifier for τ1 = τ2 if unification is successful
def Unify(τ1,τ2) =
case (τ1,τ2)
(τ1,t2) = [τ1/t2] provided t2 does not occur in τ1
(t1,τ2) = [τ2/t1] provided t1 does not occur in τ2
(b1,b2) = if (eq? b1 b2) then [ ] else fail
(τ11®τ12, τ21®τ22) = let S1 = Unify(τ11,τ21)
S2 = Unify(S1 τ12, S1 τ22)
in S2 S1 // compose substitutions
otherwise = fail 28
This is the occurs check!
28
15
Exercise
Unify ( Int®Int, t1®t2 ) yields ?
Unify ( Int, Int®t2 ) yields ?
Unify ( t1, Int®t2 ) yields ?
Programming in Haskell, A Milanova 29
29
Unify Set of Constraints C
Robinson’s algorithm unifies (i.e., solves) a single constraint
τ1 ~ τ2.
What if we have a set of constraints?
Intuition:
1. Pick a constraint τ1 ~ τ2 from the set
2. Solve τ1 ~ τ2 either failing or succeeding getting subst S
If fail, then done, constraints cannot be unified
If success, then first apply S on remaining constraints as S carries
structure that must be taken into account
30Programming in Haskell, A Milanova
30
16
Unify Set of Constraints C
UnifySet: tries to unify C and returns a principal unifier for C
if unification is successful
def UnifySet (C) =
if C is Empty Set then [] // Empty subsitution
else let
C = { τ1 ~ τ2 } U C’
S = Unify (τ1,τ2) // Unify returns a substitution S
in
UnifySet ( S(C’) ) S
// Compose the substitutions
31Programming in Haskell, A Milanova
31
Exercise
UnifySet { t1 ~ Int, t2 ~ t1®t1 } yields ?
UnifySet { t1®t2 ~ t2®t3, t3 ~ t4®t5 } yields ?
UnifySet { tf ~ t2®t1, tf ~ tx®t2 } yields ?
UnifySet { t2 ~ t4®t1, t2 ~ tf®t3, t4 ~ tx®Int, tf ~
Int®t3, tx ~ Int } yields ? 32
32
17
Outline
n Simple type inference
n Expressions, types and type environment
n Goal and intuition
n Equality constraints
n Substitution
n Robinson’s unification
n Type inference strategies
n Algorithm V (Strategy One) and
n Algorithm V (Strategy Two)
33Programming in Haskell, A Milanova
33
Type Inference Strategies
Strategy One aka constraint-based typing (Haskell)
Traverse expression’s parse tree and generate constraints.
Solve constraints offline producing substitution map S.
Finally, apply S on expression tyvar to infer the principal
type of expression
Strategy Two (Classical Hindley Milner)
Generate and solve constraints on-the-fly while traversing
parse tree. Build and apply substitution map incrementally
Programming in Haskell, A Milanova 34
34
18
def V(Γ, E) = case E of
c -> ({}, TypeOf(c))
x -> if (x NOT in Dom(Γ)) then fail
else ({}, Γ(x))
\x -> E1 -> let (CE1,TE1) = V(Γ+{x:tx},E1) – tx is fresh tyvar
in (CE1,tx®TE1)
Programming in Haskell, A Milanova (based on MIT 2015 Program Analysis OCW) 35
Constraint Generation
Strategy One
35
def V(Γ, E) = case E of
…
E1 E2 -> let (CE1,TE1) = V(Γ,E1)
(CE2,TE2) = V(Γ,E2)
in (CE1 + CE2 + {TE1 ~ TE2 ®t}, t) -- t is fresh tyvar
let x = E1 in E2 -> let (CE1,TE1) = V(Γ+{x:tx},E1)
(CE2,TE2) = V(Γ+{x:TE1},E2)
in (CE1 + CE2 + {tx ~ TE1}, TE2)
Programming in Haskell, A Milanova (based on MIT 2015 Program Analysis OCW) 36
36
19
Programming in Haskell, A Milanova 37
(\f -> f 5) (\x -> x + 1)
37
Programming in Haskell, A Milanova 38
let f = \x -> x in f 1
38
20
def V(Γ, E) = case E of
c -> ([], TypeOf(c))
x -> if (x NOT in Dom(Γ)) then fail
else ([], TE)
\x -> E1 -> let (SE1,TE1) = V(Γ+{x:tx},E1)
in (SE1, SE1(tx)®TE1)
Programming in Haskell, A Milanova (from MIT 2015 Program Analysis OCW) 39
On-the-fly Generation and
Resolution
Strategy Two
39
def V(Γ, E) = case E of
E1 E2 -> let (SE1,TE1) = V(Γ,E1)
(SE2,TE2) = V(SE1(Γ),E2)
S = Unify(SE2(TE1),TE2®t)
in (S SE2 SE1, S(t)) // S SE2 SE1
let x = E1 in E2 -> let (SE1,TE1) = V(Γ+{x:tx},E1)
S = Unify(SE1(tx),TE1)
(SE2,TE2) = V(S SE1(Γ)+{x:S(TE1)},E2)
in (SE2 S SE1, TE2)
Programming in Haskell, A Milanova (from MIT 2015 Program Analysis OCW) 40
40
21
Programming in Haskell, A Milanova 41
(\f -> f 5) (\x -> x + 1)
41

学霸联盟