Principles of Program Analysis: Type and Effect Systems Transparencies based on Chapter 5 of the book:Flemming Nielson, Hanne Riis Nielson and Chris Hankin:Principles of Program Analysis. Springer Verlag 2005.CFlemming Nielson Hanne Riis Nielson Chris Hankin. PPA Chapter 5 C F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 1
Principles of Program Analysis: Type and Effect Systems Transparencies based on Chapter 5 of the book: Flemming Nielson, Hanne Riis Nielson and Chris Hankin: Principles of Program Analysis. Springer Verlag 2005. c Flemming Nielson & Hanne Riis Nielson & Chris Hankin. PPA Chapter 5 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 1
Basic idea:effect systems If an expression e maps entities of type T1 to entities of type 72 e:T1→T2 then we can annotate the arrow with properties of the program e:12 Example analysis Choice of the property of a function call Control Flow which function abstractions might arise Side Effect which side effects might be observed Exception which exceptions might be raised Region which regions of data might be effected Communication which temporal behaviour might be observed PPA Section 5.1 C F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 2
Basic idea: effect systems If an expression e maps entities of type τ1 to entities of type τ2 e : τ1 → τ2 then we can annotate the arrow with properties of the program e : τ1 ϕ → τ2 Example analysis Choice of the property ϕ of a function call Control Flow which function abstractions might arise Side Effect which side effects might be observed Exception which exceptions might be raised Region which regions of data might be effected Communication which temporal behaviour might be observed PPA Section 5.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 2
The plan a typed functional language with a traditional underlying type system several extensions to effect systems: Analysis characteristica properties Control Flow subeffecting sets Side Effect subtyping sets Exception polymorphism sets Region polymorphic recursion sets Communication polymorphism temporal PPA Section 5.1 F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 3
The plan • a typed functional language • with a traditional underlying type system • several extensions to effect systems: Analysis characteristica properties Control Flow subeffecting sets Side Effect subtyping sets Exception polymorphism sets Region polymorphic recursion sets Communication polymorphism temporal PPA Section 5.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 3
Syntax of the Fun language e:=cxfnπx=>e0funπfx=>e0e1e2 ↑ ↑ program points if eo then e1 else e2 let x e1 in e2 e1 op e2 not polymorphic Examples:·(fnxx=>x)(fnYy=>y） .let g (funF f x =f (fny y =y)) in g (fnz z =z) PPA Section 5.1 C F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 4
Syntax of the Fun language e ::= c | x | fnπ x => e0 | funπ f x => e0 | e1 e2 ↑ ↑ program points | if e0 then e1 else e2 | | let x = {z e1 in e2} not polymorphic | e1 op e2 Examples: • (fnX x => x) (fnY y => y) • let g = (funF f x => f (fnY y => y)) in g (fnZ z => z) PPA Section 5.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 4
Underlying type system:typing judgements 「-uLe:T T:=int|boo1T1→2 「=[]|「[x→T] Assumptions: each constant c has a type Tc true has type Ttrue =bool;7 has type T7=int each operator op expects two arguments of type Top andp and ● gives a result of type Top expects two arguments of type int and gives a result of type bool PPA Section 5.1 F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 5
Underlying type system: typing judgements Γ `UL e : τ ✻ τ ::= int | bool | τ1 → τ2 ✻ Γ ::= [ ] | Γ[x 7→ τ] Assumptions: • each constant c has a type τc true has type τtrue = bool; 7 has type τ7 = int • each operator op expects two arguments of type τ 1 op and τ 2 op and gives a result of type τop > expects two arguments of type int and gives a result of type bool PPA Section 5.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 5