Type CheckingOne-Slide SummaryLecture OutlineExample: 1 + 2SoundnessType Checking ProofsRules for ConstantsRule for NewTwo More RulesSlide 10Slide 11Slide 12Slide 13Slide 14Slide 15Slide 16Slide 17Slide 18Slide 19Slide 20Slide 21Slide 22Typing DerivationsA ProblemA Solution: Put more information in the rules!Type EnvironmentsModified RulesNew RulesLetLet ExampleLet. Example.Slide 32Slide 33Slide 34Slide 35Slide 36Slide 37Slide 38Slide 39Slide 40Slide 41Slide 42Slide 43Slide 44NotesQ: General (455 / 842) Q: Movies (377 / 842) Slide 48Let with InitializationSlide 50SubtypingLet With Initialization (Better)Type System Tug-of-WarExpressiveness of Static Type SystemsDynamic And Static TypesDynamic and Static Types. (Cont.)Dynamic and Static Types in COOLDynamic and Static TypesSubtyping ExampleExample of Wrong Let Rule (1)Slide 61Slide 62Example of Wrong Let Rule (2)Example of Wrong Let Rule (3)Slide 65Typing Rule NotationAssignmentInitialized AttributesIf-Then-ElseIf-Then-Else exampleLeast Upper BoundsIf-Then-Else RevisitedCaseNext Time (Post-Midterm)Homework#1Type Type CheckingChecking#2One-Slide Summary•A type environment gives types for free variables. You typecheck a let-body with an environment that has been updated to contain the new let-variable. •If an object of type X could be used when one of type Y is acceptable then we say X is a subtype of Y, also written X · Y. •A type system is sound if  E. dynamic_type(E) · static_type(E)#3Lecture Outline•Typing Rules•Typing Environments•“Let” Rules• Subtyping•Wrong Rules#4Example: 1 + 2` 1 : Int` 1 + 2 : Int` 2 : Int#5 Soundness•A type system is sound if–Whenever ` e : T –Then e evaluates to a value of type T•We only want sound rules– But some sound rules are better than others:` i : Object(i is an integer)If we canprove it, then it's true!#6Type Checking Proofs•Type checking proves facts e : T–One type rule is used for each kind of expression•In the type rule used for a node e–The hypotheses are the proofs of types of e’s subexpressions–The conclusion is the proof of type of e itself#7Rules for Constants` false : Bool[Bool]` s : String[String](s is a string constant)#8Rule for Newnew T produces an object of type T–Ignore SELF_TYPE for now . . .` new T : T[New]#9Two More Rules` not e : Bool` e : Bool[Not]` while e1 loop e2 pool : Object` e1 : Bool ` e2 : T[Loop]#10Typing: Example•Typing for while not false loop 1 + 2 * 3 poolwhile loop pool#11Typing: Example•Typing for while not false loop 1 + 2 * 3 poolwhile loop poolnotfalse#12Typing: Example•Typing for while not false loop 1 + 2 * 3 poolwhile loop poolnotfalse : Bool#13Typing: Example•Typing for while not false loop 1 + 2 * 3 poolwhile loop poolnotfalse+: Bool: Bool#14Typing: Example•Typing for while not false loop 1 + 2 * 3 poolwhile loop poolnotfalse+1: Bool: Bool#15Typing: Example•Typing for while not false loop 1 + 2 * 3 poolwhile loop poolnotfalse+1: Bool: Bool: Int#16Typing: Example•Typing for while not false loop 1 + 2 * 3 poolwhile loop poolnotfalse+1*2: Bool: Bool: Int#17Typing: Example•Typing for while not false loop 1 + 2 * 3 poolwhile loop poolnotfalse+1*2: Bool: Bool: Int: Int#18Typing: Example•Typing for while not false loop 1 + 2 * 3 poolwhile loop poolnotfalse+1*23: Bool: Bool: Int: Int#19Typing: Example•Typing for while not false loop 1 + 2 * 3 poolwhile loop poolnotfalse+1*23: Bool: Bool: Int: Int: Int#20Typing: Example•Typing for while not false loop 1 + 2 * 3 poolwhile loop poolnotfalse+1*23: Bool: Bool: Int: Int: Int: Int#21Typing: Example•Typing for while not false loop 1 + 2 * 3 poolwhile loop poolnotfalse+1*23: Bool: Bool: Int: Int: Int: Int: Int#22Typing: Example•Typing for while not false loop 1 + 2 * 3 poolwhile loop poolnotfalse+1*23: Bool: Bool: Int: Int: Int: Int: Int: Object#23Typing Derivations•The typing reasoning can be expressed as a tree:` 2 * 3 : Int` 2 : Int ` 3 : Int` not false : Bool` false : Bool` 1 : Int` while not false loop 1 + 2 * 3 : Object` 1 + 2 * 3: Int•The root of the tree is the whole expression• Each node is an instance of a typing rule•Leaves are the rules with no hypotheses#24A Problem•What is the type of a variable reference?•The local structural rule does not carry enough information to give x a type. Fail.` x : ?[Var](x is an identifier)#25A Solution: Put more information in the rules!•A type environment gives types for free variables–A type environment is a mapping from Object_Identifiers to Types– A variable is free in an expression if:•The expression contains an occurrence of the variable that refers to a declaration outside the expression– in the expression “x”, the variable “x” is free– in “let x : Int in x + y” only “y” is free–in “x + let x : Int in x + y” both “x”, “y” are free#26Type EnvironmentsLet O be a function from Object_Identifiers to TypesThe sentence O ` e : Tis read: Under the assumption that variables have the types given by O, it is provable that the expression e has the type T#27Modified RulesThe type environment is added to the earlier rules:O ` i : Int[Int]O ` e1 + e2 : IntO ` e1 : Int O ` e2 : Int[Add](i is an integer)#28New RulesAnd we can write new rules:Equivalently:O ` x : T[Var] (O(x) = T)O ` x : TO(x) = T[Var]#29LetO[T0/x] means “O modified to map x to T0 and behaving as O on all other arguments”: O[T0/x] (x) = T0 O[T0/x] (y) = O(y)(You can write O[x/T0] on tests/assignments.)O ` let x : T0 in e1 : T1O[T0/x] ` e1 : T1[Let-No-Init]#30Let Example•Consider the Cool expressionlet x : T0 in (let y : T1 in Ex, y) + (let x : T2 in Fx, y) (where Ex, y and Fx, y are some Cool expression that contain occurrences of “x” and “y”)• Scope–of “y” is Ex, y–of outer “x” is Ex, y–of inner “x” is Fx, y•This is captured precisely in the typing rule.#31Example of Typing “let”let x : T0 in let y : T1 in +let x : T2 in Ex, yFx, yxAST#32Example of Typing “let”let x : T0 in let y : T1 in +let x : T2 in Ex, yFx, yO `xASTType env.#33Example of Typing “let”let x : T0 in let y : T1 in +let x : T2 in Ex, yFx, yO `xO[T0/x] `ASTType env.#34Example of Typing “let”let x : T0 in let y : T1 in +let x : T2 in Ex, yFx, yO `xO[T0/x] `ASTType env.O[T0/x] `O[T0/x] `#35Example of Typing “let”let x : T0 in let y : T1 in +let x : T2 in Ex, yFx, yO