types4

COMPSCI 3MI3 – Principles of Programming Languages
J. Carette
McMaster University
Adapted from “Types and Programming Languages” by Benjamin C. Pierce
J. Carette (McMaster University) Types for references and memory Fall 2023 1 / 18
Types for references and memory

The left-hand-side of := is a location of a memory cell.
J. Carette (McMaster University) Types for references and memory Fall 2023 2 / 18

The left-hand-side of := is a location of a memory cell.
When these can be stored to multiple times (without allocation), called mutable references.
J. Carette (McMaster University) Types for references and memory Fall 2023 2 / 18

The left-hand-side of := is a location of a memory cell.
When these can be stored to multiple times (without allocation), called mutable references.
In general, three operations:
Memory allocation, aka creating a reference. A “store” operation, aka assignment.
A “retrieve” operation, aka dereferencing.
Depending on the programming language, some or all of these operations may be implicit in the grammar.
Python hides allocation and retrieval, but storage is explicit. C/C++ hides retrieval, with allocation and storage being explicit. In ML, all three operations are explicit.
Haskell buries these very deeply in a library.
J. Carette (McMaster University) Types for references and memory Fall 2023 2 / 18

References
⟨t⟩ ::= … | reft
Types (to be refined):
⟨v⟩ ::= λ x:⟨T⟩.⟨t⟩ | unit
⟨T⟩ ::= …
Γ⊢t1 :T1 Γ⊢ref t1 :Ref T1
Γ⊢t1 :Ref T1 Γ ⊢!t1 : T1
Γ⊢t1 :Ref T1 Γ⊢t2 :T1 Γ⊢t1 :=t2 :Unit
(T-Deref )
(T-Assign)
J. Carette
(McMaster University)
Types for references and memory

A Sample Program
1letx=ref0in
lety=ref0in letz=ref1in
z := !x + !y;
ref is like new in Java.
J. Carette (McMaster University) Types for references and memory Fall 2023 4 / 18

1letx=ref5in 2 lety=xin
3 x := 10; 4!y
J. Carette (McMaster University) Types for references and memory Fall 2023 5 / 18
Programming Help, Add QQ: 749389476
Sharing is not necessarily bad
Aliases cells as implicit communication channels:
1 2 3 4 5 6
The values of c are 1 then 2 then 1 again. Shades of OO…
J. Carette (McMaster University) Types for references and memory Fall 2023 6 / 18
letc=ref0in
let inc c = λx : Unit. (c := succ (!c); !c) in let dec c=λx : Unit. (c := pred (!c); !c) in
inc c unit; inc c unit; dec c unit

Heap / Store
Heap array of (typed) values, ’memory store’ with ’locations’. Let L denote some set of store locations. Use l to range over L.
J. Carette (McMaster University) Types for references and memory Fall 2023 7 / 18

Heap / Store
Heap array of (typed) values, ’memory store’ with ’locations’. Let L denote some set of store locations. Use l to range over L.
A memory store is then a (partial) function from L to values.
Vocabulary:
We will use μ to denote memory stores. References will be called locations. “memory store” wil be just store.
J. Carette (McMaster University) Types for references and memory Fall 2023 7 / 18

Store passing style
Attach μ directly to terms:
Evaluation might affect the store; change evaluation relation:
t | μ → t′ | μ′
(λx : T11.t12)v2 | μ → [x 7→ v2]t12 | μ
t 1 | μ → t 1′ | μ ′ t1t2|μ→t1′ t2|μ′
t 2 | μ → t 2′ | μ ′ t1t2|μ→t1t2′ |μ′
New evaluation rules:
(E-AppAbs)
J. Carette
(McMaster University)
Types for references and memory

程序代写 CS代考加QQ: 749389476
Dereferencing
New evaluation rules for dereferencing. μ(l) = v
!l | μ → v | μ μ(l) = v
!l | μ → v | μ t 1 | μ → t 1′ | μ ′
! t 1 | μ → ! t 1′ | μ ′
(E-DerefLoc)
(E-DerefLoc)
(E-Deref )
Dereferencing a location: if we have a value for that location, return it.
Otherwise evaluate t1 (possibly with an effect) Note: ! 5 is stuck.
J. Carette (McMaster University) Types for references and memory Fall 2023 9 / 18

Assignment
l := v2 | μ → unit | [l 7→ v2]μ t 1 | μ → t 1′ | μ ′
t1:=t2|μ→t1′ :=t2|μ′ t 2 | μ → t 2′ | μ ′
(E-Assign)
(E-Assign1)
(E-Assign2) [l 7→ v2]μ means “a store which maps l to v, with all other locations
v1 := t2 | μ → v1 := t2′ | μ′ mapping to the same things as in μ.”
J. Carette (McMaster University) Types for references and memory Fall 2023 10 / 18

Allocation
l ∈/ dom(μ)
ref v1 |μ→l|μ⊕l7→v1
t 1 | μ → t 1′ | μ ′
ref t1 | μ → ref t1′ | μ′
E-RefV: we select a fresh location l not already used in μ. Extend μ with the new mapping
The term ref v evaluates to this fresh location l.
J. Carette (McMaster University) Types for references and memory Fall 2023 11 / 18

Typing the store
Skip entirely: a first “simple” approach that does not scale.
J. Carette (McMaster University) Types for references and memory Fall 2023 12 / 18

Typing the store
Skip entirely: a first “simple” approach that does not scale.
Recall: type of a location is derivable at allocation from the type of the instantiating value.
J. Carette (McMaster University) Types for references and memory Fall 2023 12 / 18

Typing the store
Skip entirely: a first “simple” approach that does not scale.
Recall: type of a location is derivable at allocation from the type of the instantiating value.
Create a typing store Σ in parallel with contexts Γ. Σ(l) = T1
Γ|Σ⊢l:Ref T1
Γ starts off empty, and has typings added as the program is traversed. Σ will be the same
Write empty Γ and emptr Σ as Ø.
J. Carette (McMaster University) Types for references and memory Fall 2023 12 / 18

Typed Stores
Definition
A store μ is said to be well typed with respect to a typing context Γ and a store typing Σ if:
dom(μ) = dom(Σ)
∀l ∈ dom(μ) | μ(l) : Σ(l)
We write this Γ | Σ ⊢ μ
J. Carette (McMaster University) Types for references and memory Fall 2023 14 / 18

Preservation?
(Γ | Σ ⊢ t : T ) ∧ (t | μ → t′ | μ′) ∧(Γ|Σ ⊢ μ)
=⇒ (Γ|Σ⊢t′ :T) But stepping can change μ and thus also Σ.
J. Carette (McMaster University) Types for references and memory Fall 2023 15 / 18

程序代写 CS代考加微信: cstutorcs
THEOREM: [Progress]
Suppose Ø | Σ ⊢ t : T for some T and Σ. Then either t is a value, or else, foranystoreμsuchthatØ|Σ⊢μ,thereissometermt′ andstoreμ′ such that t | μ → t′ | μ′.
Proof Sketch
Induction on typing derivations.
The canonical forms lemma needs two additional cases, stating that all
values of type Ref T are locations, and similarly for Unit.
J. Carette (McMaster University) Types for references and memory Fall 2023 18 / 18