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 to 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 := succ 0
!x

These examples highlight the following new features in our language:

ref t

This creates a new reference to some value t and returns its location (more on that later).

t1 := t2

Assign a value t2 to a reference t1, overwriting its previous value, returning unit.

!t

Explicitly dereference a reference t, returning the value it points to (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 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 creating a reference to 0 with ref 0, binding that 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 by first evaluating the let binding until it is 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?

In order to minimise confusion with natural numbers, Tom decided to represent locations with colours which also helped express another important point: locations may be produced as we evaluate a program but they cannot be entered directly by a programmer in the original source.

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 contained the value of the reference: in this case, 0.

 ↦ 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.

Thanks

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.