Programming Languages and Compilers (CS 421)Type Inference - The ProblemType Inference - OutlineType Inference - ExampleSlide 5Slide 6Slide 7Slide 8Slide 9Slide 10Slide 11Slide 12Slide 13Slide 14Slide 15Slide 16Slide 17Type Inference AlgorithmSlide 19Slide 20Type Inference Algorithm (cont)Slide 22Slide 23Slide 24Programming Languages and Compilers (CS 421)Elsa L Gunter2112 SC, UIUChttp://www.cs.uiuc.edu/class/sp07/cs421/Based in part on slides by Mattox Beckman, as updated by Vikram Adve and Gul AghaElsa L. Gunter Type Inference - The Problem•Given an expression e, and a typing environment , does there exist a type such that the judgment |- e : is valid - ie., follows from the typing rules?Elsa L. Gunter Type Inference - Outline•Begin by assigning a type variable as the type of the whole expression•Decompose the expression into component expressions•Use typing rules to generate constraints on components and whole•Recursively gather additional constraints to guarantee a solution for components•Solve system of constraints to generate a substitution•Apply substitution to orig. type var. to get answerElsa L. Gunter Type Inference - Example•What type can we give tofun x -> fun f -> f x?•Start with a type variable and then look at the way the term is constructedElsa L. Gunter Type 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. Gunter Type Inference - Example•Third approximate: use fun rule[f : ; x : ] |- (f x) : [x : ] |- (fun f -> f x) : [ ] |- (fun x -> fun f -> f x) : ( ); ( )Elsa L. Gunter Type 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. Gunter Type 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. Gunter Type 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. Gunter Type 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. Gunter Type Inference - Example•Type unification; solve like linear equations; [f : ; x : ] |- f : [f : ; x : ] |- x : [f : ; x : ] |- (f x) : [x : ] |- (fun f -> f x) : [ ] |- (fun x -> fun f -> f x) : ( ); ( ); ( ); Elsa L. Gunter Type 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. Gunter Type 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. Gunter Type 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. Gunter Type 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. Gunter Type 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 valid typeElsa L. Gunter Type Inference - The Problem•Given an expression e, and a typing environment , does there exist a type such that the judgment |- e : is valid - ie., follows from the typing rules?Elsa L. Gunter Type Inference AlgorithmLet has_type (, e, ) = …
View Full Document
Unlocking...