Underlying type system:axioms and rules (1) 「FULC:Tc 「上ULx:T if「(x)=T r[x→Tx]FUL eo:To 「FUL fnr 2=>e0:Tx→T0 「[f→Tx→To][x→Tx]上ULeo:To 「FUL funr f x=>eo:Tx→To 「卜ULe1:T2→T0「FULe2:T2 「-uLe1e2:To PPA Section 5.1 C F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 6
Underlying type system: axioms and rules (1) Γ `UL c : τc Γ `UL x : τ if Γ(x) = τ Γ[x 7→ τx] `UL e0 : τ0 Γ `UL fnπ x => e0 : τx → τ0 Γ[f 7→ τx → τ0][x 7→ τx] `UL e0 : τ0 Γ `UL funπ f x => e0 : τx → τ0 Γ `UL e1 : τ2 → τ0 Γ `UL e2 : τ2 Γ `UL e1 e2 : τ0 PPA Section 5.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 6
Underlying type system:axioms and rules (2) 「rULe0:boo1「FULe1:T「-ULe2:T FUL if eo then e1 else e2:T 厂上ULe1:T1「[x→T1]HULe2:T2 「FUL let x=e1ine2:T2 「huLe1:T品「FuLe2:T 「r-ULe1ope2:Top PPA Section 5.1 C F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 7
Underlying type system: axioms and rules (2) Γ `UL e0 : bool Γ `UL e1 : τ Γ `UL e2 : τ Γ `UL if e0 then e1 else e2 : τ Γ `UL e1 : τ1 Γ[x 7→ τ1] `UL e2 : τ2 Γ `UL let x = e1 in e2 : τ2 Γ `UL e1 : τ 1 op Γ `UL e2 : τ 2 op Γ `UL e1 op e2 : τop PPA Section 5.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 7
Example: let g=(funF f x =f (fny y =y)) in g (fn7 z =z) Abbreviation:「fx=[f一(r→T)→(T→T)][x一T→T] Inference tree: 「fx[y一T]FULy:T 「x FUL f:(T→T)一(T→T)「x上UL fny y=>y:T一T 「fx卜ULf(fnyy=>y):T一T []HUL funF f x=>f(fnYy=>y):(T→T)→(r一T) PPA Section 5.1 C F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 8
Example: let g = (funF f x => f (fnY y => y)) in g (fnZ z => z) Abbreviation: Γfx = [f 7→ (τ → τ) → (τ → τ)][x 7→ τ → τ] Inference tree: Γfx[y 7→ τ] `UL y : τ Γfx `UL f : (τ → τ) → (τ → τ) Γfx `UL fnY y => y : τ → τ Γfx `UL f (fnY y => y) : τ → τ [ ] `UL funF f x => f (fnY y => y) : (τ → τ) → (τ → τ) PPA Section 5.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 8
Control Flow Analysis The aim of the analysis: For each subexpression,which function abstractions might it evaluate to? Values of type int and bool can only evaluate to integers and booleans Values of type T1-72 can only evaluate to function abstractions annotate the arrow with the program points for these abstractions Example:fnx x =>x int (XL int fny x =x:int xY int subeffecting PPA Section 5.1 F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 9
Control Flow Analysis The aim of the analysis: For each subexpression, which function abstractions might it evaluate to? Values of type int and bool can only evaluate to integers and booleans Values of type τ1 → τ2 can only evaluate to function abstractions • annotate the arrow with the program points for these abstractions Example: fnX x => x : int {X →} int fnX x => x : int {X,Y →} int subeffecting PPA Section 5.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 9
Control Flow Analysis:typing judgements HCFA e 子：=int|bool|122 广：=[]|[x→] p:={π}|p1Up2|0 Back to the underlying type system:remove the annotations Lint」=int bool]=bool L方12=L」→L2 For type environments:[](x)=(x)]for all x PPA Section 5.1 C F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 10
Control Flow Analysis: typing judgements Γb `CFA e : τb ✻ τb ::= int | bool | τb1 →ϕ τb2 ✻ ϕ ::= {π} | ϕ1 ∪ ϕ2 | ∅ ✻ Γ ::= [ ] b | Γ[ b x 7→ τb] Back to the underlying type system: remove the annotations bintc = int bboolc = bool bτb1 ϕ → τb2c = bτb1c → bτb2c For type environments: bΓbc(x) = bΓ(b x)c for all x PPA Section 5.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 10