Hux: this chapter is very similar to TAPL - ch13 References But under a “formal verification” concept, it’s more interesting and practical and push you to think about it!
computational effects - “side effects” of computation - impure features
The main extension will be dealing explicitly with a
interesting refinement: type preservation
forms of assignments:
For formal study, use ML’s model.
T ::=
| Nat
| Unit
| T → T
| Ref T
t ::=
| ... Terms
| ref t allocation
| !t dereference
| t := t assignment
| l location
Inductive ty : Type :=
| Nat : ty
| Unit : ty
| Arrow : ty → ty → ty
| Ref : ty → ty.
Inductive tm : Type :=
(* STLC with numbers: *)
...
(* New terms: *)
| unit : tm
| ref : tm → tm
| deref : tm → tm
| assign : tm → tm → tm
| loc : nat → tm. (** 这里表示 l 的方式是 wrap 一个 nat as loc **)
Gamma |- t1 : T1
------------------------ (T_Ref)
Gamma |- ref t1 : Ref T1
Gamma |- t1 : Ref T11
--------------------- (T_Deref)
Gamma |- !t1 : T11
Gamma |- t1 : Ref T11
Gamma |- t2 : T11
------------------------ (T_Assign)
Gamma |- t1 := t2 : Unit
Inductive value : tm → Prop :=
...
| v_unit : value unit
| v_loc : ∀l, value (loc l). (* <-- 注意这里是一个 Π (l:nat) . value (loc l) *)
Fixpoint subst (x:string) (s:tm) (t:tm) : tm :=
match t with
...
| unit ⇒ t
| ref t1 ⇒ ref (subst x s t1)
| deref t1 ⇒ deref (subst x s t1)
| assign t1 t2 ⇒ assign (subst x s t1) (subst x s t2)
| loc _ ⇒ t
end.
r:=succ(!r); !r
can be desugar to
(\x:Unit. !r) (r:=succ(!r)).
then we can write some “imperative programming”
r:=succ(!r);
r:=succ(!r);
r:=succ(!r);
!r
shared reference brings _shared state
let r = ref 5 in
let s = r in
s := 82;
(!r)+1
thunks as methods
let c = ref 0 in
let incc = \_:Unit. (c := succ (!c); !c) in
let decc = \_:Unit. (c := pred (!c); !c) in (
incc unit;
incc unit; -- in real PL: the concrete syntax is `incc()`
decc unit
)
constructor and encapsulation!
newcounter =
\_:Unit. -- add `(self, init_val)` would make it more "real"
let c = ref 0 in -- private and only accessible via closure (特权方法)
let incc = \_:Unit. (c := succ (!c); !c) in
let decc = \_:Unit. (c := pred (!c); !c) in
{ i=incc,
d=decc } -- return a "record", or "struct", or "object"!
Previously, we use closure to represent map, with functional update
这里的”数组” (这个到底算不算数组估计都有争议,虽然的确提供了 index 但是这个显然是 O(n) 都不知道算不算 random access…
并不是 in-place update 里面的数据的,仅仅是一个 ref
包住的 map 而已 (仅仅是多了可以 shared
其实或许 list (ref nat)
也可以表达数组? 反正都是 O(n) 每次都 linear search 也一样……
newarray = \_:Unit. ref (\n:Nat.0)
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);
nullptr!
Deref a nullptr:
type Option T = Unit + T
type Nullable T = Option (Ref T)
Why is Option
outside?
think about C, nullptr
is A special const location, like Unit
(None
in terms of datacon) here.
last issue: store de-allocation
w/o GC, extremely difficult to achieve type safety…if a primitive for “explicit deallocation” provided one can easily create dangling reference i.e. references -> deleted
One type-unsafe example: (pseudo code)
a : Ref Nat = ref 1; -- alloc loc 0
free(a); -- free loc 0
b : Ref Bool = ref True; -- alloc loc 0
a := !a + 1 -- BOOM!
what should be the values of type
Ref T
?
ref
allocate some memory/storage!
run-time store is essentially big array of bytes. different datatype need to allocate different size of space (region) we think store as array of values, abstracting away different size of different values we use the word location here to prevent from modeling pointer arithmetic, which is un-trackable by most type system
location n
is float
doesn’t tell you anything about location n+4
…
we defined replace
as Fixpoint
since it’s computational and easier. The consequence is it has to be total.
typing context:
Definition context := partial_map ty.
why not just make a context a map of pair? we don’t want to complicate the dynamics of language, and this store typing is only for type check.