Type Systems and Programming Languages ; chapter 13 “Reference” 2001/5/21 hamanaka
構成 導入 Typing Operational Semantics Store Typing Safety
導入
reference cellへの参照 参照先の中身: compounded type 可 store reference 5 λx.succ(x) {i=5, b=true}
reference への操作 allocation dereferencing assignment r = ref 5; ( r : Ref Nat ) dereferencing !r; ( 5 : Nat ) assignment r := 7; ( unit : Unit ) r = 5 !r
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
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
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)
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);
Typing
Typing（仮） 型付け規則（仮） 別紙参照 実は、これでは不十分。後ほど修正。
Operational Semantics
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
Syntax including “store” ref 式が返す location を考慮 別紙参照
Operational Semantics including “store” single-step 評価 t → t’ ⇒ t | μ → t’ | μ’ 評価規則 including store 別紙参照
追加される semantics location に関する評価規則 別紙参照
Store Typing
location の型 型付け規則（仮） 別紙参照 問題点 非効率的： 型推論時にμ(l)の型計算 cyclicデータ： 型付け不可能
location の型 問題点 解決方法 非効率的： 型推論時にμ(l)の型計算 cyclicデータ： 型付け不可能 初回allocate時の型で固定⇒ Store Typing
Store Typing finite function： ∑ 型付け規則 location → 型 μ(store) を見ずにlocationの型付け可能 型付け規則 別紙参照
Safety
Safety progress theorem これまでと同様にして証明可能 preservation theorem 少し工夫必要
Progress Theorem 別紙参照
Preservation Theorem 別紙参照