Mutability Part 2 (EECS490Lec16)

So last time, we worked with references and got the formalism behind working with memory allocation / reading and writing. Now, let’s make use of that and see how these idea work wen we try to apply them to our language.

Lists: Mutable and Immutable

When we implemented the recursive list before, it was an immutable list. So, when we edited the list and re-assigned it to some variable, we don’t overwrite the old value of the list at any point ( though we may shadow it )

Now, however, we have the ability to work with memory directly. As a result, we can now create mutable lists, like those seen in EECS281.

First, we’ll write up a type definition for this list:

type 'a mutlist = 'a cell ref
and 'a cell = 
  | Nil
  | Cons of 'a ref * 'a mutlist

As you can see, this is quite literally our old definition of an immutable list, but now we’re storing cells, where each cell contains a reference to the next AND a reference to it’s current value. This is quite similar to how one would implement a linked list in C/C++, where we’d keep a pointer to the next element and store our current value for every member of the linked list.

As an example, then, imagine we had the following list:

let my_list : int mutlist = ref(Cons ( ref ( 3,  ref ( Cons ( ref 4, ref (Nil)))))

Here, we’re storing out elements like the C-style string “34”:

[3,Ptr_to_4],[4,Ptr_to_null],[Null_Element]

In this case, we’re now using the Nil element as a way to terminate our mutable list in a fashion that makes sense. With this, we could now imagine creating a cons:

let rec append x:'a xs:'a mutlist = 
   match !xs with
   | Nil -> xs := Cons(ref x, ref Nil)
   | Cons(_, tl) := append x tl

Here, what we’re going for is we’re searching through to the end of the list recursively, till we reach the null pointer that must be at the end of each and every list for the list to terminate. Then, once we find that null pointer, we point the previous element to this new value’s reference, and point to the Nil value again, to maintain the invariant that “Nil remains at the end”

We could also write an imperative map function, in a similar way:

let impmap (f: 'a -> 'a) (xs: 'a mutlist) : unit

For this function, however, what’s important is that the function returns unit. This is like a lot of procedures one finds in C/C++ code, where you pass something in by reference to mutate it and, hopefully, gain a sizeable speed advantage as a result.

Append “yet again” to list ref

Now that we have imperative constructs, however, we can also start implementing functions in some very unique ways. For example, let’s look at another definition of append. We’re worked with recursive functions, but in imperative functions we tend to use loops. Formally, these refer to calls using the ; operator to chain side-effects, mutating state until we exit ( For an excellent use of stuff similar to this look into any good book on Lisp, which delved deep into this distinction ) to bypass the need for recursion:

let append (x : 'a) (xs : 'a mutlist) = 
   let cur  = ref xs in 
     while (!!cur<>Nil) do
       match !!cur with
       | Nil -> failwith("Impossible")
       | Cons(hd,tl) -> cur := tl
     done
   !cur := Cons (ref x, ref Nil)

Here, if you notice, we’re using a While loop. In OCaml, this refers to precisely what you expect it to be, and we essentially keep on moving along the chain, using cur to refer to the current element we’re looking at, until we get to a Nil element, where we’ll exit the loop by failing the condition, after which we’ll simply add the new element to the end. In this manner, we’re explicitly making our function tail-recursive and ensuring that we do not maintain a massive callstack, keeping a low memory usage on our computer.

Mutable Record Field in OCaml

While linked lists are, as we can see, quite useful and quite easy to in OCaml. However, due to the sheer common-nature of mutable data structures in normal programming, OCaml has a few shortcuts for common mutable data structure building blocks. For example, we could have used the following cell definition in our definition of a mutlist:

type 'a cell = 
  | Nil
  | Cons of { mutable hd : 'a, tl : 'a mutlist }

The pair inside the curly brackets is what is known as a mutable record type, which is like a product type except we can specify that certain members are mutable. So here, the term mutable refers to the fact that hd is a reference. This built-in by OCaml stores pairs more effectively than the multiple pointer system used above, making it slightly more efficient, and easier to read. To assign to a mutable field, you can do the following:

e.hd <- e'

Where <- is the assignment operator ( like = in C++/C/Python… )

As a note, ref cells are actually implemented in OCaml as record fields with one record, known as ‘content’

Mutable Arrays in OCaml

Additionally, OCaml also supports, as primitives, mutable arrays, with the following syntax:

Introduction Form: [| 1; 2; 3 |] : int array
Assignment: e_arr.(e_idx) <- e_val

Again, on the low-level, these are easy to add to a system, and are common enough that they make programming a lot easier to look at and do. (Plus, they add to cache-locality and other optimizations). Additionally, the lengths of these arrays are FIXED; these aren’t lists in Python

Formalism.once_again

Alright. So last time, there were a few judgement we missed, and a few things we just need to tie up. Firstly, we need to discuss the val judgement. For this judgement, we have to add the following:

$\frac{}{\text{\#l } val}$

This is largely just so we know that references are values, and so we can encode that into future judgements without any hassle.

Cyrus does use two different notations for locations in memory: the # notation seen here, and the loc[] notation seen previously. I’m guessing that we’ll stick with the former from now on, but check the reference given to decide.

Secondly, we need to go back to evaluation. While it might seem that last time we added all of the rules that we needed to, we did miss a rule in our quest of creating this new “imperative” evaluation syntax. Namely, when evaluating pairs, we hadn’t given a focus on if the left item or the right item should be evaluated first, something which does matter in practice for some constructs like short-circuit and evaluation. For us, we’ll have the following rule:

$\frac{e_1||\mu \Downarrow e_1'||\mu_1 , e_2||\mu_1 \Downarrow e_2'||\mu_2}{(e_1, e_2)||\mu \Downarrow (e_1', e_2')||\mu_2}$

We evaluate pairs from left-to-right.

Again, while this is inline with similar imperative constructs, when we’re being formal there is no such thing as an “obvious rule”. As a result, we need to be specific, or we’ll fall into the trap of adding a null reference or something else that fundamentally makes a language more prone to bugs / harder to prove correctness in.

So we have achieved formalism… what did we lose?

Now, that was a relatively simple and painless process to add imperative semantics to our system. However, in logical systems like these, changing small things can cause large effects, like assuming / not assuming Euclid’s Fifth in Euclidean Geometry. As we now have to reason about reads and writes in ADDITION to input and output behavior, we now have counterexamples for some of our proofs and the proof structure no longer holds as cleanly.

As an example, recall when we proved the following:

map f ( map g xs ) = map (f%g) xs

While this held for pure / immutable functions, it definitely does not hold for mutable functions. If we had two functions that depended on the same internal reference location, applying all of g and then all of f would be different than applying g, then f, to every member of the array, as we expect.

Thus, while this proof might still hold if our functions are pure, it does not hold in general, making it harder to implement global optimizations like the one above.

An Alternative Approach to Imperative References

Cyrus marks the formalism for this language as optional content for us, so if you’re in a hurry maybe spend more time elsewhere. (Though you should know why this matters)

Now, what makes this tradeoff interesting is that we may not necessarily need to take it. In languages like Haskell, a darling of PL theory and one with a LOT of use among academics for its mathematical equivalencies, the designers made a distinction between pure expressions, which do not have side effects, and imperative commands, which do.

They then have expressions which return encapsulated commands, which take a pure expression and then convert it into an imperative commands. According to Cyrus, this is essentially like having a program that builds a cake recipe, which deliver it to some system that bakes the cake from your recipe. The actual recipe itself is a pure data structure, so we can describe it functionally, but the building process is imperative, so we make a distinction between them to allow for easy processing.

Another way of looking at this, if you’ve taken EECS 485 already, is to look at Project1, where we built a static-site generator. In that class, you essentially wrote some glue-code that could take a program that outputs a template, and then builds the template. If a user then builds a pure function that makes their website templates, they can trust the implementation and focus on making sure their templates describe what they want us to describe, while our system worries about taking that input and building the actual HTML for the website.

To do this formally, what you do is add the following type:

tau ::= ...
   | cmd                 (Called "I/O Monad" in Haskell)

Which denotes an encapsulated command, and we also add the following introduction forms to encapsulate the command, and make it “impure”.

We also add a new expression to introduce this command type, cmd(…):

Exp e::= ...
     | cmd(m)

Lastly, we add a new type of language called the command language, which refers to the various imperative constructs we’ll program in:

Cmd m:== get  (read some value)
         | set l to e ( write some value )
         | return e   (return some expression)
         | bind x <- e in m 
         | declare l <- e in m (Explicitly work with locations)

So how does this work?

One simple idea: Separation of Ideas

We keep our functional language pure and functional, allowing us to reason cleanly about it in the way we have had already, and the commands will simply be a type that isn’t executed yet, so you can still reason about them in this pure manner.

Judgements

So, in this hypothetical extension, we’ll need to add a typing judgment:

$\frac{\Gamma;\cdot \vdash m \text{ ok }}{\Gamma \vdash \text{cmd(m)}: \text{cmd}}$

So, we’re essentially saying, so long as we have a valid command, we can then say that the type of the expression is a command. (I.E the “Woah, this command is made of a command” judgement)

However, in defining this judgement, we need a new judgement, as we can’t yet tell, formally, if a command is an “ok” command or not. So to do so, we’ll need a new command-specific judgment that determines if a command is valid or not.

To do that, we’ll need a new judgement form:

$\Gamma ; \Sigma \vdash m \text{ ok }$

Where Sigma is a new aspect to care about - a mapping of memory locations l to the types each contain:

$\Sigma : l_1 : \tau_1 ,..., l_n : \tau_n$

Now, here are the judgements:

The Primitive Side Effects

For get:

$\frac{}{\Gamma;\Sigma,l:\tau \vdash \text{ get l ok }}$

This makes sense, as we must, somewhere, have location l corresponding to a value tau so we can retrieve it. Such a rule, when managed well, could also prevent tons of headaches for a programmer, like undefined memory writes/reads in C/C++.

For set:

$\frac{\Gamma \vdash e : \tau}{\Gamma ; \Sigma, l : \tau \vdash \text{ set l to e ok}}$

Here, once again, what we’re going makes sense. If we’re trying to set a value of type tau to another value, e, we need to confirm that e has the same type so we can write to l.

For declare:

$\frac{\Gamma \vdash e : \tau , \Gamma ; \Sigma , l : \tau \vdash m \text{ ok }}{\Gamma ; \Sigma \vdash \text{ declare l }\leftarrow \text{ e in m ok}}$

For declare, as it isn’t a primitive, we need to do a bit more work. Firstly, we need to make sure e is of a valid type tau, as otherwise it’ll be very difficult to type check it. Secondly, we also need to make sure that m, the list of commands that dictate how we’ll process memory, is a valid list of commands given that new piece of memory has type tau, so we know we can process it effectively. With these safeguards, we can then be sure we won’t mess up, and can continue running our program.

Command Language Specific

Besides these primitives, we also need to worry about the forms specific to making this command language workable and useful given our primitive side effects.

For return:

$\frac{\Gamma \vdash e:\text{ Num}}{\Gamma ; \Sigma \vdash \text{ return e ok }}$

Here, we’re simply stating that return only succeeds if e is a number, reminiscent of returning from main in C/C++. While Cyrus does not that we can make this command language return any arbitrary type, we’ll avoid it for now due to the added complexity.

For bind:

$\frac{\Gamma \vdash e \text{ cmd }, \Gamma,x:\text{Num}; \Sigma \vdash m \text{ ok }}{\Gamma ; \Sigma \vdash \text{ bind x } \leftarrow \text{e in m ok} }$

What bind does, formally, is it provides the sort of sequencing in commands that you want in any imperative programming language. For the type-checker, it checks if the command to be run previously, e, is a command sequence that returns an int, and then it checks that the rest of the commands are valid, allowing for us to place commands sequentially.

While Cyrus does not cover the dynamic semantics of this language, the point of this example is that we’re able to separate the expression language judgements from the command language judgements. In doing so, we manage to separate pure and impure functions, allowing us to reason about our programs a lot better.