Programming Languages andCompilers (CS 421)Elsa L Gunter2112 SC, UIUChttp://www.cs.uiuc.edu/class/sp07/cs421/Based in part on slides by Mattox Beckman, as updatedby Vikram Adve and Gul AghaElsa L. GunterType Inference - The Problem• Given an expression e, and a typingenvironment Γ, does there exist atype τ such that the judgment Γ |- e : τ is valid - ie., follows from the typingrules?Elsa L. GunterType Inference - Outline• Begin by assigning a type variable as the type ofthe whole expression• Decompose the expression into componentexpressions• Use typing rules to generate constraints oncomponents and whole• Recursively gather additional constraints toguarantee a solution for components• Solve system of constraints to generate asubstitution• Apply substitution to orig. type var. to get answerElsa L. GunterType Inference - Example• What type can we give tofun x -> fun f -> f x?• Start with a type variable and then lookat the way the term is constructedElsa L. GunterType Inference - Example• First approximate:[ ] |- (fun x -> fun f -> f x) : α• Second approximate: use fun rule[x : β] |- (fun f -> f x) : γ[ ] |- (fun x -> fun f -> f x) : α• α ≡ (β → γ)Elsa L. GunterType Inference - Example• Third approximate: use fun rule[f : δ ; x : β] |- (f x) : ε[x : β] |- (fun f -> f x) : γ[ ] |- (fun x -> fun f -> f x) : α• α ≡ (β → γ); γ ≡ (δ → ε)Elsa L. GunterType Inference - Example• Fourth approximate: use app rule[f : δ; x : β] |- f : ϕ → ε [f : δ; x : β] |- x : ϕ[f : δ ; x : β] |- (f x) : ε[x : β] |- (fun f -> f x) : γ[ ] |- (fun x -> fun f -> f x) : α• α ≡ (β → γ); γ ≡ (δ → ε)Elsa L. GunterType Inference - Example• Fifth approximate: use var rule[f : δ ; x : β] |- f : ϕ → ε [f : δ ; x : β] |- x : ϕ[f : δ ; x : β] |- (f x) : ε[x : β] |- (fun f -> f x) : γ[ ] |- (fun x -> fun f -> f x) : α• α ≡ (β → γ); γ ≡ (δ → ε); δ ≡ (ϕ → ε) .Elsa L. GunterType Inference - Example• Sixth approximate: use var rule[f : δ ; x : β] |- f : ϕ → ε [f : δ ; x : β] |- x : ϕ[f : δ ; x : β] |- (f x) : ε[x : β] |- (fun f -> f x) : γ[ ] |- (fun x -> fun f -> f x) : α• α ≡ (β → γ); γ ≡ (δ → ε); δ ≡ (ϕ → ε); ϕ ≡ βElsa L. GunterType Inference - Example• Done building proof tree; now solve![f : δ ; x : β] |- f : ϕ → ε [f : δ ; x : β] |- x : ϕ[f : δ ; x : β] |- (f x) : ε[x : β] |- (fun f -> f x) : γ[ ] |- (fun x -> fun f -> f x) : α• α ≡ (β → γ); γ ≡ (δ → ε); δ ≡ (ϕ → ε); ϕ ≡ βElsa L. GunterType Inference - Example• Type unification; solve like linearequations;[f : δ ; x : β] |- f : ϕ → ε [f : δ ; x : β] |- x : ϕ[f : δ ; x : β] |- (f x) : ε[x : β] |- (fun f -> f x) : γ[ ] |- (fun x -> fun f -> f x) : α• α ≡ (β → γ); γ ≡ (δ → ε); δ ≡ (ϕ → ε); ϕ ≡ βElsa L. GunterType Inference - Example• Eliminate ϕ:[f : δ ; x : β] |- f : β → ε [f : δ ; x : β] |- x : β[f : δ ; x : β] |- (f x) : ε[x : β] |- (fun f -> f x) : γ[ ] |- (fun x -> fun f -> f x) : α• α ≡ (β → γ); γ ≡ (δ → ε); δ ≡ (β → ε); ϕ ≡ βElsa L. GunterType Inference - Example• Next eliminate δ :[f : β → ε; x : β] |- f : β → ε [f : δ; x : β] |- x : β[f : β → ε; x : β] |- (f x) : ε[x : β] |- (fun f -> f x) : γ[ ] |- (fun x -> fun f -> f x) : α• α ≡ (β → γ); γ ≡ ((β → ε) → ε); δ ≡ (β → ε) ;Elsa L. GunterType Inference - Example• Next eliminate γ :[f : β → ε; x : β] |- f : β → ε [f : δ; x : β] |- x : β[f : β → ε; x : β] |- (f x) : ε[x : β] |- (fun f -> f x) : ((β → ε) → ε)[ ] |- (fun x -> fun f -> f x) : α• α ≡ (β → ((β → ε) → ε)); γ ≡ ((β → ε) → ε);Elsa L. GunterType Inference - Example• Next eliminate α :[f : β → ε; x : β] |- f : β → ε [f : δ; x : β] |- x : β[f : β → ε; x : β] |- (f x) : ε[x : β] |- (fun f -> f x) : ((β → ε) → ε)[ ] |- (fun x -> fun f -> f x) : (β → ((β → ε) → ε))• α ≡ (β → ((β → ε) → ε));Elsa L. GunterType Inference - Example• No more equations to solve; we are done[f : β → ε; x : β] |- f : β → ε [f : δ; x : β] |- x : β[f : β → ε; x : β] |- (f x) : ε[x : β] |- (fun f -> f x) : ((β → ε) → ε)[ ] |- (fun x -> fun f -> f x) : (β → ((β → ε) → ε))• Any instance of (β → ((β → ε) → ε)) is a validtypeElsa L. GunterType Inference - The Problem• Given an expression e, and a typingenvironment Γ, does there exist atype τ such that the judgment Γ |- e : τ is valid - ie., follows from the typingrules?Elsa L. GunterType Inference AlgorithmLet has_type (Γ, e, τ) = S• Γ is a typing environment• e is an expression• τ is a (generalized) type,• S is a set of equations betweengeneralized typesElsa L. GunterType Inference Algorithm• Let has_type (Γ, e, τ) = S– Γ is a typing environment,– e is an expression,– τ is a (generalized) type,– S is a set of equations between generalized types.Idea: S is the constraints on type variablesnecessary for Γ …
View Full Document
Unlocking...