Variables are self-explanatory, they are changing, i.e. they are mutable. This means our implementations of new, deref, and set can be used to implement variables.

Variable Declaration

We can using a sequencing assignment (:=) to help declare and set variables. We can also use bind and new to create an identifier and location to store our value in.

(var x := t1 in t2) == (bind x = new t2 in t2)

This just makes x a location that contains the value we want to store.

Variable Dereference

Because all variables are just identifiers bound to locations we have to dereference them to get a useable value.

(x + 1) == ((deref x) + 1)

or in our interpreter (roughly)

eval e st (Var x) = (deref (lookup x e) st)

Variable Assignment

We can again use the walrus operator to force sequencing.

(x := t1) == (set x t1)

We have to evaluate t1 as locations only point to values. So the order of operations would go as such.