Type Systems and Programming Languages ; chapter 13 “Reference”

Presentation on theme: "Type Systems and Programming Languages ; chapter 13 “Reference”"— Presentation transcript:

1 Type Systems and Programming Languages ; chapter 13 “Reference”
2001/5/21 hamanaka

2 構成 導入 Typing Operational Semantics Store Typing Safety

3 導入

4 reference cellへの参照 参照先の中身: compounded type 可 store reference 5
λx.succ(x) {i=5, b=true}

5 reference への操作 allocation dereferencing assignment
r = ref 5; ( r : Ref Nat ) dereferencing !r; ( 5 : Nat ) assignment r := 7; ( unit : Unit ) r = 5 !r

6 reference への操作 deallocation: 扱わない (例) let r = ref 0 in 型推論が困難
let s = r in free r; let t = ref true in t := false; succ(!s) deallocation: 扱わない 型推論が困難 runtime による garbage collection

7 alias 一つのセルへの複数の参照 型推論をややこしくする ( r:=1 ; r:= !s) ⇒ r:=!s
unless r, s are aliases for the same cell プログラムを便利にもする sequencing, shared state, etc. r = 5 s = 7 aliases

8 reference の利用例 Sequencing に適合 ← assignment は Unit型 Shared State として利用
(λ_:Unit. !r) (r:= succ(!r)); ⇒ (r:=succ(!r); !r) Shared State として利用 c = ref 0; incc = λx:Unit.(c:=succ(!c); !c); decc = λx:Unit.(c:=pred(!c); !c); o = { i = incc, d = decc}; (: Object)

9 reference の利用例 Compounded Type への参照の利用 NatArray = Ref (Nat → Nat);
newarray = λ_.Unit. (ref (λn:Nat.0)) as NatArray; lookup = λa:NatArray. λn:Nat. (!a) n; update = λa:NatArray. λm:Nat. λv:Nat. let oldf = !a in a:= (λn:Nat. if equal m n then v else oldf n);

10 Typing

11 Typing（仮） 型付け規則（仮） 別紙参照 実は、これでは不十分。後ほど修正。

12 Operational Semantics

13 location の導入 store(heap)を value の配列と抽象化 reference は location:
reference は store location の集合の要素 store は location から value への部分関数　　meta variable μ: μ(l) = v reference は location: store 配列の抽象index < value > 1 5 2 TRUE 3 λx.x location

14 Syntax including “store”
ref　式が返す location を考慮 　別紙参照

15 Operational Semantics including “store”
single-step 評価 t → t’ ⇒ t | μ → t’ | μ’ 評価規則 including store 　　　別紙参照

16 追加される semantics location に関する評価規則 　別紙参照

17 Store Typing

18 location の型 型付け規則（仮） 　　　　別紙参照 問題点 非効率的： 型推論時にμ(l)の型計算 cyclicデータ： 型付け不可能

19 location の型 問題点 解決方法 非効率的： 型推論時にμ(l)の型計算 cyclicデータ： 型付け不可能
初回allocate時の型で固定⇒ Store Typing

20 Store Typing finite function： ∑ 型付け規則 location → 型
μ(store) を見ずにlocationの型付け可能 型付け規則 　　別紙参照

21 Safety

22 Safety progress theorem これまでと同様にして証明可能 preservation theorem 少し工夫必要

23 Progress Theorem 別紙参照

24 Preservation Theorem 別紙参照