Types and Programming Languages Chapter 13 References
We began the meeting by accidentally having a stand-up around our collected snacks and beverages (featuring a brand new smorgasbord of soft drinks provided by Geckoboard), discussing our recent trip to Bletchley Park and Paul's adventures with Net::HTTP.
Tom kicked off the meeting by stressing that, while the chapter introduces a lot of new notation in the evaluation and typing rules, the underlying concepts are not wildly more complicated than what we've seen so far.
Paul took to the whiteboard to write up some examples of the new syntax introduced for references:
ref 0
x := 2
!x
These examples highlight the following new features in our language:
ref t
This allocates a reference, providing an initial value t for the new cell.
t1 := t2
Assign a value t2 to a reference t1, changing its stored value.
!t
Read the current value of the cell referenced by t (e.g. dereferencing ref 0 would return 0).
Our first point of confusion is that the book uses the following example:
x = ref 0
But x = is not part of our language, it is instead meant to represent some sort of imaginary type-checking REPL but this escaped a lot of us.
We thought it would be helpful to walk through some example programs using these new constructs and step through their evaluation.
Tom took to the board to step through the following example which makes use of let (as seen in Simple Extensions), ref t and !t:
let x = ref 0 in !x
Intuitively, we expect this program to evaluate to 0 as we're allocating a reference to a cell populated with 0 with ref 0, binding that reference to the name x and then dereferencing x to get its value 0.
More formally, we used the evaluation rules in the chapter to evaluate the source program a single step at a time by first evaluating the let binding of x until it was a value.
This meant taking ref 0 and applying the evaluation rule E-RefV (as 0 is already a value) which returns a "location". But what is a location?
Tom decided to represent locations as colours which avoided confusion with other terms (e.g. numbers) and helped express another important point: locations may be produced as we evaluate step-by-step but they cannot be entered directly by a programmer in the original program.
So we could now replace ref 0 with a location represented by the colour red:
let x =in !x
As well as doing this, we needed to represent some "store" which now contains the value of the reference: in this case, 0.
With that done, we could now evaluate one more step: evaluating the let by replacing every mention of x in the body with its value:
!
(The store remains the same with ↦ 0
Finally, we can evaluate the dereference to get our final value:
0
And the store? Well, that remains unchanged and still contains ↦ 0
We walked through another program, this time with an assignment in it:
let x = ref 0 in x := succ !x; !x
Evaluating this a step at a time, we first replace ref 0 with a new location (again, represented by the colour red) and add 0 to the store (using μ to describe the current state of the store):
let x =
We can then evaluate the let, replacing every occurrence of x with the location:
We now have a sequence and need to do the following:
- Evaluate the left-hand side until it is
unit; - Evaluate the assignment until its right-hand side is a value;
- Evaluate
succuntil its argument is a value; - Evaluate
!until it is a value.
Starting with the last point, dereferencing in
succ ! gives us:
Now the argument to succ is a value, the right-hand side of the assignment is also itself a value so we can change the value of in the store and the entire assignment is evaluated to
unit:
unit; !
The evaluation rules for a sequence mean that we can now discard the first term, leaving the second:
!
This leaves us with one final dereference to do:
succ 0 μ =
And we're done!
Confident that we understood how reference allocation, assignment and dereferencing evaluates, we decided to move onto the types of these operations and how we might use types to detect errors in programs using these primitives.
We began by discussing the kinds of problems we might be able to prevent if we could type references and their related operations:
- Assigning to something other than a reference (e.g.
true := 0); - Dereferencing a non-reference (e.g.
!true); - Passing a reference with the wrong type to an abstraction that requires a reference of a specific type (e.g.
(λx:Ref Nat . x) (ref true)).
We decided to try to infer the appropriate typing rules for references by taking an example well-typed program and type checking it:
(λx:Ref Nat . x := succ !x; !x) (ref 0)
We began by looking at ref 0 and asking what the type of this term would be:
Γ ⊢ 0 : Nat
-------------------
Γ ⊢ ref 0 : Ref Nat
We decided that it should have the type Ref Nat and we could check this by looking at the type of its value (in this case Nat). More generally, this gave us a generic typing rule for ref t:
Γ ⊢ t : T
-------------------
Γ ⊢ ref t : Ref T
For assignment, we similarly derived the following:
Γ ⊢ x : Ref Nat 0 : Nat
--------------------------
x := 0 : Unit
Which gave us the generic typing rule for t := t:
Γ ⊢ t1 : Ref T t2 : T
------------------------
t1 := t2 : Unit
Similarly, for dereferencing (which is sort of the opposite of our typing rule for allocating a reference):
Γ ⊢ t : Ref T
-------------
Γ ⊢ !t : T
We justified the fact that references had to have their own type constructor Ref T much like we've seen with functions (T → T) and lists as we need to preserve both the fact that they are references (and not, say, Nat directly) in order to type check dereferencing and assignment and preserve the type of their value so that we can type check a term after dereferencing.
While we were pretty pleased with our very own typing rules, it turns out that the chapter still had a treat for us in store: the concept of store typing.
Evaluating and even type checking our example programs hadn't led us to explicitly keep track of the types of references but, in order to prove the safety of the type system, we need to be able to type check a term like the following:
!
But we can't possibly do that if we don't know what the type of is.
Enter store typing (denoted by Σ)!
While we've had typing contexts (denoted by Γ) populated by variable declarations in our programs previously, we now have a second store of types.
This means that our typing rules need to also take this into account, e.g.
Γ | Σ ⊢ t : T
---------------------
Γ | Σ ⊢ ref t : Ref T
The unusual thing here is that, unlike the typing context Γ, none of our rules ever populate the store typing. Instead, it is a side-effect of evaluation.
James explained "aliasing" by contrasting the following two programs:
{ref 0, ref 0}
(λx. {x, x}) ref 0
The first would allocate two separate references, evaluating to:
{, 
}
Whereas the second would allocate a single reference but return a pair with two instances of this same reference (these being aliases):
{, }
- We continue to enjoy TAPL with some pleasant surprise how far we've made through what is really a postgraduate type theory textbook
- The meetings (and Tom's leadership) continue to be invaluable as a few people agreed that they would not be able to understand the material without the club
- The variety of soft drinks were a great new addition
- There was some discussion about the ownership of Attending.io pages (with each organiser using their own account meaning they are the only one who can make edits) but no one felt strong enough to make a change (e.g. create a single unified club account)
Paul rambled on about how expectations/preconceptions seem to have a huge impact on software development job satisfaction, how to coach junior developers and was dismayed to be called out by Leo and Chris when he started telling a fascinating work-related anecdote about office reception signage only to discover he'd told it before.
Thanks to Leo and Geckoboard for hosting and providing beverages (both soft and not), Laura for organising the meeting and bringing bread and dips, to Tom for leading the meeting, to James for some valiant whiteboarding, to Chris for yet more delicious bread, Charlie and all those who contributed snacks.