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
Finally, we can evaluate the dereference to get our final value:
0
And the store? Well, that remains unchanged and still contains
We walked through another program that also included an assignment:
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:
x := succ !
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.
This gives us:
x := succ 0; !
Now the argument to succ is a value, the right-hand side of the assignment is also itself a value and so therefore 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:
0 μ =
And we're done!
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, Charlie and all those who contributed snacks.