logging in or signing up 08 typeinfer Sharck Download Post to : URL : Related Presentations : Share Add to Flag Embed Email Send to Blogs and Networks Add to Channel Uploaded from authorPOINT Insert YouTube videos in PowerPont slides with aS Desktop Copy embed code: (To copy code, click on the text box) Embed: URL: Thumbnail: WordPress Embed Customize Embed The presentation is successfully added In Your Favorites. Views: 134 Category: Product Traini.. License: All Rights Reserved Like it (0) Dislike it (0) Added: June 16, 2007 This Presentation is Public Favorites: 0 Presentation Description No description available. Comments Posting comment... Premium member Presentation Transcript Programming Languages and Compilers (CS 421): Programming Languages and Compilers (CS 421) Elsa L Gunter 2112 SC, UIUC http://www.cs.uiuc.edu/class/sp07/cs421/ Based in part on slides by Mattox Beckman, as updated by Vikram Adve and Gul Agha Type Inference - The Problem: 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? Type Inference - Outline: 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 answer Type Inference - Example: Type Inference - Example What type can we give to fun x -andgt; fun f -andgt; f x? Start with a type variable and then look at the way the term is constructed Type Inference - Example: Type Inference - Example First approximate: [ ] |- (fun x -andgt; fun f -andgt; f x) : Second approximate: use fun rule [x : ] |- (fun f -andgt; f x) : [ ] |- (fun x -andgt; fun f -andgt; f x) : ( ) Type Inference - Example: Type Inference - Example Third approximate: use fun rule [f : ; x : ] |- (f x) : [x : ] |- (fun f -andgt; f x) : [ ] |- (fun x -andgt; fun f -andgt; f x) : ( ); ( ) Type Inference - Example: Type Inference - Example Fourth approximate: use app rule [f : ; x : ] |- f : [f : ; x : ] |- x : [f : ; x : ] |- (f x) : [x : ] |- (fun f -andgt; f x) : [ ] |- (fun x -andgt; fun f -andgt; f x) : ( ); ( ) Type Inference - Example: Type Inference - Example Fifth approximate: use var rule [f : ; x : ] |- f : [f : ; x : ] |- x : [f : ; x : ] |- (f x) : [x : ] |- (fun f -andgt; f x) : [ ] |- (fun x -andgt; fun f -andgt; f x) : ( ); ( ); ( ) . Type Inference - Example: Type Inference - Example Sixth approximate: use var rule [f : ; x : ] |- f : [f : ; x : ] |- x : [f : ; x : ] |- (f x) : [x : ] |- (fun f -andgt; f x) : [ ] |- (fun x -andgt; fun f -andgt; f x) : ( ); ( ); ( ); Type Inference - Example: Type Inference - Example Done building proof tree; now solve! [f : ; x : ] |- f : [f : ; x : ] |- x : [f : ; x : ] |- (f x) : [x : ] |- (fun f -andgt; f x) : [ ] |- (fun x -andgt; fun f -andgt; f x) : ( ); ( ); ( ); Type Inference - Example: Type Inference - Example Type unification; solve like linear equations; [f : ; x : ] |- f : [f : ; x : ] |- x : [f : ; x : ] |- (f x) : [x : ] |- (fun f -andgt; f x) : [ ] |- (fun x -andgt; fun f -andgt; f x) : ( ); ( ); ( ); Type Inference - Example: Type Inference - Example Eliminate : [f : ; x : ] |- f : [f : ; x : ] |- x : [f : ; x : ] |- (f x) : [x : ] |- (fun f -andgt; f x) : [ ] |- (fun x -andgt; fun f -andgt; f x) : ( ); ( ); ( ); Type Inference - Example: Type Inference - Example Next eliminate : [f : ; x : ] |- f : [f : ; x : ] |- x : [f : ; x : ] |- (f x) : [x : ] |- (fun f -andgt; f x) : [ ] |- (fun x -andgt; fun f -andgt; f x) : ( ); (( ) ); ( ) ; Type Inference - Example: Type Inference - Example Next eliminate : [f : ; x : ] |- f : [f : ; x : ] |- x : [f : ; x : ] |- (f x) : [x : ] |- (fun f -andgt; f x) : (( ) ) [ ] |- (fun x -andgt; fun f -andgt; f x) : ( (( ) )); (( ) ); Type Inference - Example: Type Inference - Example Next eliminate : [f : ; x : ] |- f : [f : ; x : ] |- x : [f : ; x : ] |- (f x) : [x : ] |- (fun f -andgt; f x) : (( ) ) [ ] |- (fun x -andgt; fun f -andgt; f x) : ( (( ) )) ( (( ) )); Type Inference - Example: Type Inference - Example No more equations to solve; we are done [f : ; x : ] |- f : [f : ; x : ] |- x : [f : ; x : ] |- (f x) : [x : ] |- (fun f -andgt; f x) : (( ) ) [ ] |- (fun x -andgt; fun f -andgt; f x) : ( (( ) )) Any instance of ( (( ) )) is a valid type Type Inference - The Problem: 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? Type Inference Algorithm: Type 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 Type Inference Algorithm: Type 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 variables necessary for |- e : Let Unif(S) be a substitution of generalized types for type variables solving S Solution: Unif(S)() |- e : Unif(S)() Type Inference Algorithm: Type Inference Algorithm has_type (, exp, ) = Case exp of Var v --andgt; return { (v)} Const c --andgt; return { } where |- c : by the constant rules fun x -andgt; e --andgt; Let , be fresh variables Let S = has_type ([x: ] , e, ) Return { } S Type Inference Algorithm (cont): Type Inference Algorithm (cont) Case exp of App (e1 e2) --andgt; Let be a fresh variable Let S1 = has_type(, e1, ) Let S2 = has_type(, e2, ) Return S1 S2 Type Inference Algorithm (cont): Type Inference Algorithm (cont) Case exp of let x = e1 in e2 --andgt; Let be a fresh variable Let S1 = has_type(, e1, ) Let S2 = has_type([x: ] , e2, ) Return S1 S2 Type Inference Algorithm (cont): Type Inference Algorithm (cont) Case exp of let rec x = e1 in e2 --andgt; Let be a fresh variable Let S1 = has_type([x: ] , e1, ) Let S2 = has_type([x: ] , e2, ) Return S1 S2 Type Inference Algorithm (cont): Type Inference Algorithm (cont) To infer a type, introduce type_of Let be a fresh variable type_of (, e) = Let S = has_type (, e, ) Return Unif(S)() Need an algorithm for Unif You do not have the permission to view this presentation. In order to view it, please contact the author of the presentation.
08 typeinfer Sharck Download Post to : URL : Related Presentations : Share Add to Flag Embed Email Send to Blogs and Networks Add to Channel Uploaded from authorPOINT Insert YouTube videos in PowerPont slides with aS Desktop Copy embed code: (To copy code, click on the text box) Embed: URL: Thumbnail: WordPress Embed Customize Embed The presentation is successfully added In Your Favorites. Views: 134 Category: Product Traini.. License: All Rights Reserved Like it (0) Dislike it (0) Added: June 16, 2007 This Presentation is Public Favorites: 0 Presentation Description No description available. Comments Posting comment... Premium member Presentation Transcript Programming Languages and Compilers (CS 421): Programming Languages and Compilers (CS 421) Elsa L Gunter 2112 SC, UIUC http://www.cs.uiuc.edu/class/sp07/cs421/ Based in part on slides by Mattox Beckman, as updated by Vikram Adve and Gul Agha Type Inference - The Problem: 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? Type Inference - Outline: 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 answer Type Inference - Example: Type Inference - Example What type can we give to fun x -andgt; fun f -andgt; f x? Start with a type variable and then look at the way the term is constructed Type Inference - Example: Type Inference - Example First approximate: [ ] |- (fun x -andgt; fun f -andgt; f x) : Second approximate: use fun rule [x : ] |- (fun f -andgt; f x) : [ ] |- (fun x -andgt; fun f -andgt; f x) : ( ) Type Inference - Example: Type Inference - Example Third approximate: use fun rule [f : ; x : ] |- (f x) : [x : ] |- (fun f -andgt; f x) : [ ] |- (fun x -andgt; fun f -andgt; f x) : ( ); ( ) Type Inference - Example: Type Inference - Example Fourth approximate: use app rule [f : ; x : ] |- f : [f : ; x : ] |- x : [f : ; x : ] |- (f x) : [x : ] |- (fun f -andgt; f x) : [ ] |- (fun x -andgt; fun f -andgt; f x) : ( ); ( ) Type Inference - Example: Type Inference - Example Fifth approximate: use var rule [f : ; x : ] |- f : [f : ; x : ] |- x : [f : ; x : ] |- (f x) : [x : ] |- (fun f -andgt; f x) : [ ] |- (fun x -andgt; fun f -andgt; f x) : ( ); ( ); ( ) . Type Inference - Example: Type Inference - Example Sixth approximate: use var rule [f : ; x : ] |- f : [f : ; x : ] |- x : [f : ; x : ] |- (f x) : [x : ] |- (fun f -andgt; f x) : [ ] |- (fun x -andgt; fun f -andgt; f x) : ( ); ( ); ( ); Type Inference - Example: Type Inference - Example Done building proof tree; now solve! [f : ; x : ] |- f : [f : ; x : ] |- x : [f : ; x : ] |- (f x) : [x : ] |- (fun f -andgt; f x) : [ ] |- (fun x -andgt; fun f -andgt; f x) : ( ); ( ); ( ); Type Inference - Example: Type Inference - Example Type unification; solve like linear equations; [f : ; x : ] |- f : [f : ; x : ] |- x : [f : ; x : ] |- (f x) : [x : ] |- (fun f -andgt; f x) : [ ] |- (fun x -andgt; fun f -andgt; f x) : ( ); ( ); ( ); Type Inference - Example: Type Inference - Example Eliminate : [f : ; x : ] |- f : [f : ; x : ] |- x : [f : ; x : ] |- (f x) : [x : ] |- (fun f -andgt; f x) : [ ] |- (fun x -andgt; fun f -andgt; f x) : ( ); ( ); ( ); Type Inference - Example: Type Inference - Example Next eliminate : [f : ; x : ] |- f : [f : ; x : ] |- x : [f : ; x : ] |- (f x) : [x : ] |- (fun f -andgt; f x) : [ ] |- (fun x -andgt; fun f -andgt; f x) : ( ); (( ) ); ( ) ; Type Inference - Example: Type Inference - Example Next eliminate : [f : ; x : ] |- f : [f : ; x : ] |- x : [f : ; x : ] |- (f x) : [x : ] |- (fun f -andgt; f x) : (( ) ) [ ] |- (fun x -andgt; fun f -andgt; f x) : ( (( ) )); (( ) ); Type Inference - Example: Type Inference - Example Next eliminate : [f : ; x : ] |- f : [f : ; x : ] |- x : [f : ; x : ] |- (f x) : [x : ] |- (fun f -andgt; f x) : (( ) ) [ ] |- (fun x -andgt; fun f -andgt; f x) : ( (( ) )) ( (( ) )); Type Inference - Example: Type Inference - Example No more equations to solve; we are done [f : ; x : ] |- f : [f : ; x : ] |- x : [f : ; x : ] |- (f x) : [x : ] |- (fun f -andgt; f x) : (( ) ) [ ] |- (fun x -andgt; fun f -andgt; f x) : ( (( ) )) Any instance of ( (( ) )) is a valid type Type Inference - The Problem: 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? Type Inference Algorithm: Type 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 Type Inference Algorithm: Type 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 variables necessary for |- e : Let Unif(S) be a substitution of generalized types for type variables solving S Solution: Unif(S)() |- e : Unif(S)() Type Inference Algorithm: Type Inference Algorithm has_type (, exp, ) = Case exp of Var v --andgt; return { (v)} Const c --andgt; return { } where |- c : by the constant rules fun x -andgt; e --andgt; Let , be fresh variables Let S = has_type ([x: ] , e, ) Return { } S Type Inference Algorithm (cont): Type Inference Algorithm (cont) Case exp of App (e1 e2) --andgt; Let be a fresh variable Let S1 = has_type(, e1, ) Let S2 = has_type(, e2, ) Return S1 S2 Type Inference Algorithm (cont): Type Inference Algorithm (cont) Case exp of let x = e1 in e2 --andgt; Let be a fresh variable Let S1 = has_type(, e1, ) Let S2 = has_type([x: ] , e2, ) Return S1 S2 Type Inference Algorithm (cont): Type Inference Algorithm (cont) Case exp of let rec x = e1 in e2 --andgt; Let be a fresh variable Let S1 = has_type([x: ] , e1, ) Let S2 = has_type([x: ] , e2, ) Return S1 S2 Type Inference Algorithm (cont): Type Inference Algorithm (cont) To infer a type, introduce type_of Let be a fresh variable type_of (, e) = Let S = has_type (, e, ) Return Unif(S)() Need an algorithm for Unif