I. Introduction to type checking A. What is a "type"? Can we define a type in a language independent way? B. What is a type error? what is a type error? 1. Preservation of invariants by modules in data 2. Seals (Morris 1973) a. prevent: alteration, discovery, impersonation Does an OO language prevent impersonation? b. seal mechanism c. allows invariant preservation: 3. Type error: attempt to access sealed data without proper capability a. containers (variables) and pointers II. Type Checking Notation and Techniques ------------------------------------------ TYPE CHECKING VS. TYPE INFERENCE Type Checking: Some declarations built-in (+, *, ...) User declares types (of names) Compiler infers types (of expressions) Compiler compares each inferred use to declared - with == in normal language - with <= in OO language (subtyping) Type Inference Some declarations built-in (+, *, ...) Compiler infers types (of expressions) Compiler compares all inferred uses - with == in normal language - with <= in OO language (subtyping) ------------------------------------------ A. Type checking ------------------------------------------ TYPE CHECKING NOTATION: JUDGEMENTS G |- x : T means given/assuming type envrionment G, one can prove that x has type T TYPE CHECKING NOTATION: AXIOMS AND INFERENCE RULES [var] G |- x : T if G(x) = T G |- E : T [asgn] ------------------- if G(x) = T G |- x := E : ok ------------------------------------------ In an atrribute grammar, like JastAdd, would G be an inherited or synthesized attribute? Would the type T be inherited or synthesized? 1. type environments (Watt's PL Syntax and Semantics, section 3.3.1) what if an expression E involves a variable x? ------------------------------------------ ENVIRONMENTS G \in TypeEnv = Identifier -> Type {} is the empty TypeEnv x:T,y:U is the mapping {x |-> T, y |-> U} Adding: If G = x:T then G,y:U is x:T,y:U Overlay: G(+)H is such that (G(+)H)(x) = H(x), if x in dom(H) G(x) if x not in dom(H) ------------------------------------------ 2. example type checking rules for WHILE ------------------------------------------ TYPE CHECKING FOR THE WHILE LANGUAGE ::= int | bool | ok define Programs: G_FV |- S : ok [prog] ----------------- if x \in FV(S) ==> G_FV(x) = int |- { S } : ok Statements: G |- E : T [asgn] ------------------- if G(x) = T G |- x := E : ok [skip] G |- skip : ok G |- S1 : ok, G :- S2 : ok [seq] -------------------------- G |- S1; S2: ok G |- E : bool, G |- S1: ok, G |- S2: ok [if] ------------------------- G |- if E then S1 else S2 : ok G |- E : bool, G |- S: ok [wh] -------------------------- while E do S : ok Expressions: [var] G |- x : T if G(x) = T [num] G |- n : int G |- E1 : int, G |- E2 : int [aexp] ----------------------------- G |- E1 op_a E2 : int [true] G |- true: bool [false] G |- false: bool G |- E : bool [not] --------------------- G |- not E : bool G |- E1 : bool, G |- E2 : bool [bexp] ----------------------------- G |- E1 op_b E2 : bool G |- E1 : int, G |- E2 : int [rexp] ----------------------------- G |- E1 op_r E2 : bool ------------------------------------------ a. variations What if we don't assume that all variables have type int in a program? What if we had type declarations for variables? ------------------------------------------ OPERATOR TYPES G |- E1: S, G |- E2: S, G |- op : S x S -> T [binexp] ------------------- G |- E1 op E2 : T Either have axioms for various operators: G |- + : int x int -> int G |- and : bool x bool -> bool G |- < : int x int -> bool Or put them in the initial environment for the program: G_FV |- S : ok [prog] ----------------- if x \in FV(S) ==> G_FV(x) = int |- { S } : ok and G(+) = int x int -> int, ... ------------------------------------------ When would you prefer putting operators in the environment? 3. example, type checking rules for SML-like expressions ------------------------------------------ TYPE CHECKING FOR SML SUBSET Abstract Syntax: E ::= I | E1(E2) | if E1 then E2 else E3 | fn I:T1 => E | let D in E2 | (E1,E2) D ::= val I:T = E | rec I:T = E | D1; D2 T ::= int | bool | T1 -> T2 | T1 * T2 | TV | T1 list | all TV . T1 TV ::= 'a | 'b | 'c | ... Expressions: [var] G |- I: T if [app] ---------------------- G |- E1(E2): T [if] ------------------------------- G |- (if E1 then E2 else E3): T [fn] --------------------------- if G' G |- (fn I:T1 => E): T1->T2 G |- D ==> G', G'' |- E2 : [let] --------------------- if G'' = G |- (let D in E2): T Declarations: [val] ----------------------- if G' = I:T G |- val I:T = E ==> G' [rec] ----------------------- if G' = I:T G |- rec I:T = E1 ==> G' [Dseq] ---------------------- G |- D1; D2 ==> ------------------------------------------ What about simultaneous binding? mutual recursion (and)? what should be the rule for pairs? For formals that are pairs? do we need a rule for applications where the arguments are pairs? do we really need the [pair] rule? 4. proofs ------------------------------------------ PROOFS OF TYPE CHECKING [var] Hfxy |- x: 'a, Hfxy |- y :'b [pair] ------------------------------ [var] Hfxy |- f :'a*'b->'c, Hfxy |- (x,y) : 'a*'b [app] ---------------------------- Hfxy |- f(x,y) : 'c [fn] ---------------------------- Hxy |- (fn f:'a*'b->'c => f(x,y)) : ('a*'b->'c) -> 'c [fn] ---------------------------- ETE |- (fn (x:'a,y:'b) => (fn f:'a*'b->'c => f(x,y))) : 'a*'b -> (('a*'b->'c) -> 'c) where ETE = {} and Hxy = x:'a, y:'b and Hfxy = f: 'a*'b->'c, x:'a, y:'b ------------------------------------------ can you prove G |- plus(x,3):int where G = 3:int, plus: int*int -> int, x: int ? B. Reconstructing (Inferring) type declarations for monomorphic expressions 1. example ------------------------------------------ TYPE RECONSTRUCTION EXAMPLE [var] Hfxy |- x: , Hfxy |- y : [pair] ------------------------------ [var] Hfxy |- f : Hfxy |- (x,y) : [app] ---------------------------- Hfxy |- f(x,y) : [fn] ---------------------------- Hxy |- (fn f => f(x,y)) : [fnp] ---------------------------- ETE |- (fn (x,y) => (fn f => f(x,y))) : where ETE = {} and Hxy = x:'a, y:'b} and Hfxy = f: x:'a, y:'b CONSTRAINTS: ------------------------------------------ 2. inference rules without considering polymorphism ------------------------------------------ TYPE RECONSTRUCTION (INFERENCE) PART 1 [var] H |- I: T if H(I) = T H |- E1: S -> T, H |- E2: S [app] --------------------------- H |- E1(E2): T H |- E1:bool, H |- E2:T, H |- E3:T [if] ---------------------------------- H |- (if E1 then E2 else E3): T [fn] ------------------------ if H' = H |- (fn I => E): T1->T2 H |- D ==> H', H'' |- E : T [let] -------------------- if H'' = H(+)H' H |- (let D in E): T ------------------------------------------ 3. polymorphism (skip) ------------------------------------------ WHEN IS A FUNCTION POLYMORPHIC? Is this a type error? (fn f => g(f(2), f(true))) What if f is: val id = (fn x => x) val succ = (fn x => x + 1) ------------------------------------------ ------------------------------------------ DON'T ALLOW CAPTURING let val g = (fn x => let val f = (fn y => x) in if f(3) then f(true) else x + 5 end) in ... end ------------------------------------------ ------------------------------------------ GENERIC TYPE VARIABLES in the type: all 'a . 'a -> 'b 'a is generic, and 'b is not [var] H |- id: all 'a . 'a -> 'a [gElim] -------------------------------- H |- id: 'b -> 'b, H |- id: 'c -> 'c, H |- 3: int, H |- true : bool [app] ------------------------------------ H |- id(3):int, H |- id(true): bool [pair] ----------------------------------- H |- (id(3), id(true)) : int * bool where H = {id |-> (all 'a . 'a -> 'a), 3 |-> int, true |-> bool} CONSTRAINTS: 'b = int 'c = bool ------------------------------------------ ------------------------------------------ TYPE RECONSTRUCTION (INFERENCE) GENERICS and BINDINGS H |- E: T ---------------------- if H' = I:gen(T,H) H |- (val I = E) ==> H' H'' |- E1: T [rec] ------------------- if H' = I:gen(T,H) H |- rec f = E1 ==> H' where gen(T, H) = all V1 . ... . all Vk . T if V1,...,Vk are all the free type variables in T that are not in range(H). H |- I : all V . T [gElim] ------------------ where T' = [T''/V]T H |- I : T' ------------------------------------------ 4. polymorphic rules (skip) ------------------------------------------ EXAMPLE G |- rec map = (fn f => (fn ls => if (null ls) then [] else (f (hd ls))::(map f (tl ls)))) ==> where G is (op ::): all 'a . 'a * 'a list -> 'a list, [] : all 'a . 'a list, null : all 'a . 'a list -> bool, hd : all 'a . 'a list -> 'a, tl : all 'a . 'a list -> 'a list ------------------------------------------ C. Limitations 1. No recursive types: 2. Polymorphic functions are not first-class objects! ------------------------------------------ NO POLYMORPHIC FUNCTIONS AS ARGUMENTS - fun F f = fn (a,b) => (f(a), f(b)); val F = fn : ('a -> 'b) -> 'a * 'a -> 'b * 'b - val W = (fn x => (x x)); std_in:1.18-1.20 Error: operator is not a function operator: 'Z in expression: (x x) ------------------------------------------ III. Type Checking in JastAdd