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. The core language type system for a functional language (like SML) A. Type checking ------------------------------------------ THE TYPE CHECKING PROBLEM & NOTATION E : int [fun] ---------------------------------- fun f (x:int):int = E : int -> int ------------------------------------------ 1. environments (Watt's PL Syntax and Semantics, section 3.3.1) what if E involves x? What if E involves f? What if E involves y? ------------------------------------------ ENVIRONMENTS H \in TypeEnv = Identifier -> Type empty-type-env : TypeEnv bind : Identifier * Type -> TypeEnv dom : TypeEnv -> PowerSet(Identifier) overlay : TypeEnv * TypeEnv -> TypeEnv find : TypeEnv * Identifier -> Type [ |-> ] : TypeEnv * Identifier * Type -> TypeEnv empty-type-env = { } bind(I,T) = { I |-> T } find(H, I) = H(I) dom(empty-type-env) = { } dom(bind(I,T)) = {I} dom(overlay(H1,H2)) = dom(H1) union dom(H2) find(overlay(H1, H2), I) = if I in dom(H1) then H1(I) else H2(I) [I |-> T]H = overlay(bind(I,T), H) ------------------------------------------ so what is find(overlay(bind(i,int), bind(i:real)), i)? so how do we formalize the notation for the rule above? 2. type checking rules ------------------------------------------ TYPE CHECKING [var] H |- I: T where [app] ---------------------- H |- E1(E2): T [if] ------------------------------- H |- (if E1 then E2 else E3): T [fn] --------------------------- where H' H |- (fn I:T1 => E): T1->T2 H |- D ==> H', H'' |- E2 : where H'' = [let] --------------------- H |- (let D in E2): T [val] ----------------------- where H' = H |- val I:T = E ==> H' bind(I,T) where H' = [rec] ----------------------- bind(I,T) H |- rec I:T = E1 ==> H' ------------------------------------------ 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? 3. 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 = empty-type-env and Hxy = {x |-> 'a, y |-> 'b} and Hfxy = {f |-> 'a*'b->'c, x |-> 'a, y |-> 'b} ------------------------------------------ can you prove H |- plus(x,3):int where H = {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 = empty-type-env 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 where I \in dom(H), find(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] ------------------------ where H' = H |- (fn I => E): T1->T2 H |- D ==> H', H'' |- E : T where H'' = [let] -------------------- overlay(H',H) H |- (let D in E): T ------------------------------------------ 3. a problem, when to decide something is polymorphic. ------------------------------------------ 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 where H' = [val] ------------------- bind(I,gen(T,H)) H |- (val I = E) ==> H' H'' |- E1: T where H' = [rec] ------------------- bind(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' = H |- I : T' [T''/V]T ------------------------------------------ 4. rules ------------------------------------------ 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) ------------------------------------------