Implicitly Typed MinHS Inference Algorithm Unification
1
Damas-Milner Type Inference
Christine Rizkallah
CSE, UNSW Term 3 2020
Implicitly Typed MinHS Inference Algorithm Unification
Implicitly Typed MinHS
Explicitly typed languages are awkward to use1. Ideally, we’d like the compiler to determine the types for us.
Example
What is the type of this function?
recfunf x=fstx+1 We want the compiler to infer the most general type.
2
1See Java
Implicitly Typed MinHS Inference Algorithm Unification
3
Implicitly Typed MinHS
Start with our polymorphic MinHS, then:
remove type signatures from recfun, let, etc.
remove explicit type abstractions, and type applications (the @ operator). keep ∀-quantified types.
remove recursive types, as we can’t infer types for them. see whiteboard for why.
Implicitly Typed MinHS
Inference Algorithm
Unification
Typing Rules
x:τ∈Γ
Γ ⊢ x : τ Var
Γ⊢e1 :τ1 →τ2 Γ⊢e2 :τ1
Γ⊢e1 e2 :τ2 Γ⊢e1 :τ1 Γ⊢e2 :τ2
App
Γ ⊢ (Pair e e ) : τ × τ ConjI 1212
Γ⊢e1 :Bool Γ⊢e2 :τ Γ⊢e3 :τ
If
4
Γ⊢(Ife1 e2 e3):τ
Implicitly Typed MinHS Inference Algorithm Unification
5
Primitive Operators
For convenience, we treat prim ops as functions, and place their types in the environment.
(+) : Int → Int → Int, Γ ⊢ (App (App (+) (Num 2)) (Num 1)) : Int
Implicitly Typed MinHS
Inference Algorithm
Unification
Functions
x : τ1,f : τ1 → τ2,Γ ⊢ e : τ2
Γ⊢(Recfun(f.x.e)):τ →τ Func 12
6
Implicitly Typed MinHS
Inference Algorithm
Unification
Sum Types
Γ ⊢ e : τ1 Γ⊢InLe:τ +τ DisjI1
Γ⊢InRe:τ +τ DisjI2 12
Note that we allow the other side of the sum to be any type.
12 Γ ⊢ e : τ2
7
Implicitly Typed MinHS Inference Algorithm Unification
Polymorphism
If we have a polymorphic type, we can instantiate it to any type:
Γ⊢e :∀a.τ
Γ⊢e :τ[a:=ρ]AllE
We can quantify over any variable that has not already been used.
Γ⊢e:τ a∈/TV(Γ)
AllI
Γ ⊢ e : ∀a. τ
(Where TV (Γ) here is all type variables occurring free in the types of variables in Γ)
8
Implicitly Typed MinHS Inference Algorithm Unification
9
We want an algorithm for type inference: With a clear input and output. Which terminates.
Which is fully deterministic.
The Goal
Implicitly Typed MinHS Inference Algorithm Unification
Typing Rules
Γ⊢e1 :τ1 Γ⊢e2 :τ2 Γ⊢(Paire1 e2):τ1×τ2
Can we use the existing typing rules as our algorithm?
infer :: Context → Expr → Type
This approach can work for monomorphic types, but not polymorphic ones. Why not?
10
Implicitly Typed MinHS Inference Algorithm
Unification
First Problem
Γ⊢e :∀a.τ
Γ⊢e :τ[a:=ρ]AllE
The rule to add a ∀-quantifier can always be applied: .
Γ ⊢ (Num 5) : ∀a. ∀b. Int
AllE
AllE
Γ ⊢ (Num 5) : ∀a. Int Γ ⊢ (Num 5) : Int
11
This makes the rules give rise to a non-deterministic algorithm – there are many possible rules for a given input. Furthermore, as it can always be applied, a depth-first search strategy may end up attempting infinite derivations.
Implicitly Typed MinHS Inference Algorithm Unification
Another Problem
Γ⊢e :∀a.τ
Γ⊢e :τ[a:=ρ]AllE
The above rule can be applied at any time to a polymorphic type, even if it would break later typing derivations:
Γ ⊢ fst : ∀a. ∀b. (a × b) → a · · · Γ⊢fst:(Bool×Bool)→Bool Γ⊢(Pair1True):(Int×Bool)
Γ ⊢ (Apply fst (Pair 1 True)) : ???
12
Implicitly Typed MinHS Inference Algorithm Unification
Yet Another Problem
The rule for recfun mentions τ2 in both input and output positions. x : τ1,f : τ1 → τ2,Γ ⊢ e : τ2
Γ⊢(Recfun(f.x.e)):τ →τ Func 12
In order to infer τ2 we must provide a context that includes τ2 — this is circular. Any guess we make for τ2 could be wrong.
13
Implicitly Typed MinHS Inference Algorithm Unification
Solution
We allow types to include unknowns, also known as unification variables or schematic variables. These are placeholders for types that we haven’t worked out yet. We shall use α, β etc. for these variables.
Example
(Int × α) → β is the type of a function from tuples where the left side of the tuple is Int, but no other details of the type have been determined yet.
As we encounter situations where two types should be equal, we unify the two types to determine what the unknown variables should be.
14
Implicitly Typed MinHS
Inference Algorithm
Unification
Example
Γ ⊢ fst : ∀a. ∀b. (a × b) → a · · ·
Γ ⊢ fst : (α × β) → α Γ ⊢ (Pair 1 True) : (Int × Bool)
Γ ⊢ (Apply fst (Pair 1 True)) : γ (α×β)→α ∼ (Int×Bool)→γ
[α := Int,β := Bool,γ := Int]
15
Implicitly Typed MinHS Inference Algorithm Unification
We call this substitution a unifier.
Definition
Unification
A substitution S to unification variables is a unifier of two types τ and ρ iff Sτ = Sρ. Furthermore, it is the most general unifier, or mgu, of τ and ρ if there is no other unifier S′ where Sτ ⊑ S′τ.
Wewriteτ∼U ρifUisthemguofτandρ.
Example (Whiteboard)
α×(α×α) ∼ β×γ (α×α)×β ∼ β×γ Int+α ∼ α+Bool (α×α)×α ∼ α×(α×α)
16
Implicitly Typed MinHS Inference Algorithm Unification
17
Back to Type Inference
We will decompose the typing judgement to allow for an additional output — a substitution that contains all the unifiers we have found about unknowns so far.
Inputs Expression, Context Outputs Type, Substitution
We will write this as SΓ ⊢ e : τ, to make clear how the original typing judgement may be reconstructed.
Implicitly Typed MinHS Inference Algorithm
Unification
Application, Elimination
S1Γ⊢e1 :τ1 S2S1Γ⊢e2 :τ2 S2τ1 ∼U (τ2 →α) US2S1Γ ⊢ (Apply e1 e2) : Uα
(α fresh)
(x:∀a1.∀a2. …∀an.τ)∈Γ
Γ ⊢ x : τ[a1 := α1,a2 := α2,…,an = αn]
Example (Whiteboard)
(α1…αn fresh)
18
(fst : ∀a b. (a × b) → a) ⊢ (Apply fst (Pair 1 2))
Implicitly Typed MinHS Inference Algorithm Unification
Functions
S(Γ,x:α1,f:α2)⊢e:τ Sα2∼U(Sα1→τ) USΓ ⊢ (Recfun (f .x. e)) : U(Sα1 → τ)
(α1, α2 fresh)
Example (Whiteboard)
19
(Recfun (f .x. (Pair x x)))
(Recfun (f .x. (Apply f x)))
Implicitly Typed MinHS Inference Algorithm Unification
20
Generalisation
In our typing rules, we could generalise a type to a polymorphic type by introducing a ∀ at any point in the typing derivation. We want to be able to restrict this to only occur in a syntax-directed way.
Consider this example:
let f = (recfun f x = (x,x)) in (fst (f 4),fst (f True)) Where should generalisation happen?
Implicitly Typed MinHS Inference Algorithm Unification
Let-generalisation
To make type inference tractable, we restrict generalisation to only occur when a binding is added to the context via a let expression.
This means that let expressions are now not just sugar for a function application, they actually play a vital role in the language’s syntax, as a place for generalisation to occur.
We define Gen(Γ, τ ) = ∀(TV (τ ) \ TV (Γ)). τ Then we have:
S1Γ ⊢ e1 : τ S2(S1Γ,x : Gen(S1Γ,τ)) ⊢ e2 : τ′ S2S1Γ ⊢ (Let e1(x. e2)) : τ′
21
Implicitly Typed MinHS Inference Algorithm Unification
22
Summary
The rest of the rules are straightforward from their typing rule.
We’ve specified Robin Milner’s algorithm W for type inference. Many other algorithms exist, for other kinds of type systems, including explicit constraint-based systems.
This algorithm is restricted to the Hindley-Milner subset of decidable polymorphic instantiations, and requires that polymorphism is top-level — polymorphic functions are not first class.
We still need an algorithm to compute the unifiers.
Implicitly Typed MinHS Inference Algorithm Unification
23
Unification
unify :: Type → Type → Maybe Unifier
(where the Type arguments do not include any ∀ quantifiers and the Unifier returned is the mgu)
We shall discuss cases for unify τ1 τ2
Implicitly Typed MinHS Inference Algorithm Unification
24
Both type variables: τ1 = v1 and τ2 = v2: v1 = v2 ⇒ empty unifier
v1 ̸=v2 ⇒[v1 :=v2]
Cases
Implicitly Typed MinHS Inference Algorithm Unification
25
Both primitive type constructors: τ1 = C1 and τ2 = C2: C1 = C2 ⇒ empty unifier
C1 ̸= C2 ⇒ no unifier
Cases
Implicitly Typed MinHS Inference Algorithm Unification
26
Both are product types τ1 = τ11 × τ12 and τ2 = τ21 × τ22.
1 Compute the mgu S of τ11 and τ21.
2 Compute the mgu S′ of Sτ12 and Sτ22.
3 Return S ∪ S′
(same for sum, function types)
Cases
Implicitly Typed MinHS Inference Algorithm Unification
27
One is a type variable v, the other is just any term t. v occurs in t ⇒ no unifier
otherwise ⇒ [v := t]
Cases
Implicitly Typed MinHS Inference Algorithm Unification
28
Done
Implementing this algorithm will be the focus of Assignment 2. See course website for deadlines etc.
You should allow plenty of time to tackle it. You will be given a generous deadline but it requires time to complete.
Haskell-wise, this code will use a monad to track errors and the state needed to generate fresh unification variables.