TAPL 読書会@東京 第8回 - tokyotaplreading @ ウィキ

第八回 9/10
p153 References

garbage collection

13.1
[0] * 2
共有するかしないか
13.1.1

a = {ref 0, ref 0}
b = (\x:Ref Nat, {x, x})(ref 0)

Shared state

lookup
update

13.2 typing

13.3 evalation

e-appabs
e-app1
e-app2

スタート幾何

13.4 store typing

(l1 |-> \x:Nat. 999,
l2 |-> \x:Nat. (!l1) x,
l3 |-> \x:Nat. (!l2) x,
l4 |-> \x:Nat. (!l3) x,
l5 |-> \x:Nat. (!l4) x),

(l1 |-> \x:Nat. (!l2) x,
l2 |-> \x:Nat. (!l1) x),

13.4.1
let x1 = ref (\n. 999) in
let x2 = ref (\n. (!x))n in

(x1 := ref (\n. (!x2))n;
 x2);;

Σ(l) = T1

---

Γ|Σ |- l: Ref T1

T-LOC

figure 13-1

13. Reference
13.1 Introduction
13.2 Typing
13.3 Evaluation
13.4 Store Typing

13.5 Safety
13.6 Notes

13.1 Introduction
新しい演算子

ref

r = ref 5;
r : Ref Nat 参照を与える(作る)

!

!r
5 : Nat

:=

r := 7
unit: Unit

参照の基本的な操作
allocation
dereferencing
assignment

Side Effects and Sequencing

(r:=succ(!r); !r)
 8 : Nat

(λ_ : Uni. !r)(r := succ(!r)) こうも書けるけど…

Referencing and Aliasing
s = r
s : Ref Nat

r と s が同じところを指す

s := 82;
として
!r
をすると?

13.1.1 Exercise ★
Draw a similar diagram showing the effect of evaluating the expressions
a = {ref 0, ref 0} and b = (λx:Ref Nat. {x, x})(ref 0).

#{} で pair を表現

Shared State

c = ref 0;
c : Ref Nat

incc = λx:Unit. (c := succ (!c); !c);
incc : Unit → Nat

decc = λx:Unit. (c := pred (!c); !c);
decc : Unit → Nat

#負の添え字とかどうなるんだろう

?

#とりあえず今は

pred 0 は 0 となるオヤクソクでやっている

#PythonやらRubyやらで実験

Referencing to Compound Types
NatArray = Ref (Nat→Nat);

newarray = λ_:Unit. ref (λn:Nat.0);
newarray : Unit → NetArray

lookup(参照) と update(更新)を定義
lookup = λa:NetArray. λn:Nat. (!a) n;
lookup : NatArray → Nat → Nat

update = λa:NatArray. λm:Nat. λv:Nat.

           let oldf = !a in
           a := (λn:Nat. if  equal m n then v else oldf n);

update : NatArray → Nat → Nat → Unit

13.1.2 Exercise ★★
If we defined update more compactly like this
update = λa:NatArray. λm:Nat λv:Nat.

      a := (λn:Nat. if equal m n then v else (!a) n);

would it behave the same?

Garbage Collection
(省略)
型安全性を壊してしまう可能性が!

13.1.3 Exercise ★★
Show how this can lead to a violation of type safety.

13.2 Typing
(T-REF)

Γ |- t1 : T1

---

Γ ref t1 : Ref T1

(T-DEREF)
Γ |- t1 : Ref T1

---

Γ |- !t1 : T1

(T-ASSIGN)
Γ |- t1 : Ref T1 Γ |- t2 : T1

---

Γ |- t1 := t2 : Unit

13.3 Evaluation
(E-APPABS)
(E-APP1)
(E-APP2)
(E-DEREF)
(E-DEREFLOC)
(E-ASSIGN1)
(E-ASSIGN2)
(E-ASSIGN)
(E-REF)
(E-REFV)

13.3.1
Exercise ★★★
How might our evaluation rules be refined to model garbage collection?
What theorem would we then need to prove, to argue that this
refinment is correct?

13.4 Store Typing
13.4.1
Exercise ★
Can you find a term whose evaluation will create this paricular cyclic store?