Mutation and References (EECS490Lec15)

So so far, we’ve been programming with pure expressions, without any changeable state.

So, to reason about a function, we simply had to understand how input relates to output and, as for us variable names got meaning from substitution, we knew that, given some input, we knew what the output was. So for example:

// If we had a function f with f: Num -> Num -> Num list -> Num
// And if we had the following program:
let xs = [1;2;3] in
  let x1 = f 0 5 xs in
    let x2 = f 0 5 xs in
      ...(Part A)...

Then, in Part A of the code, xs == [1;2;3] and x1 == x2 , no matter what, as f can’t modify the underlying code in any manner

However, in Python and other so-called “imperative” languages, we could have the following:

xs = [1,2,3]
def f(a,b,xs):
	xs[a] += b
  return xs[a]
x1 = f(0,5,xs)
x2 = f(0,5,xs)

In this case, as xs is modified, xs != [1,2,3] and x1!=x2 .

So, we’ve come to a fundamental new idea: Mutation

Mutation: Allows you to modify memory in-place, without preserving previous versions

As a result of this idea / this operation, we need to change a few of our ideas:

1. We need to distinguish variables from reference to memory locations.

   • Variables are given meaning by substitution (Seriously, we need this on a shirt for this class)
   • Memory locations are given meaning by so-called read and write operations
2. We lose many equivalencies, as functional ordering now matters.

3. We now have two things to keep track of:

   1. The input-output behavior of functions
   2. Reads and writes to memory

Thus, this is why, in well-written and critical software, we separate pure from impure functions. It’s a lot easier to test/prove that a pure function works, so as long as we can separate the two as much as possible, we can move as much of the easily-verifiable logic to the pure side and keep the hard mutable parts as limited as possible.

In terms of nomenclature, mutation is known as a side-effect:

Side-effects: Observable events that occur during the evaluation (informally, the execution) of a program

Some other notable side-effects include the following:

• I/O Effects, like printf, graphics, networking, and file reads/writes

• Performance Motivated Effects:

  • Mutable Data Structures
  • Caching/Memoization, seen in self-adjusting data structures like red-black binary search trees

In OCaml, we have a rich amount of stuff to work with in terms of expressions:

• We’ve already covered these, but OCaml includes support for sum and product types, recursive types, polymorphism, type inference and pattern matching, which are hallmarks of pure functional programming languages.
• However, OCaml is an imperative programming language, so it also has support for references, reads, writes, and loops

It is important to note that we still have not left the world of expressions yet (i.e. we still haven’t introduced the idea of a statement). We’re just introducing the notion of mutability into our expression-filled world.

How? Using new types!

Reference Types

In OCaml, we’ve written the following before:

let x = 5 in
  ...

Now, we know that in the ”…” section, x shall always remain 5, at least until it becomes shadowed.

However, we can also write the following:

let x = ref 5 in
   ...

This x now has the type int ref , referring to the location in memory of the 5, like pointers to the heap. Thus, the following is a type error:

x + 1

As int ref has no support for addition (unlike in C/C++, where they very much do), this expression makes no sense! However, if we want to go from a reference to its value, we can do it through the dereference operator, ! (pronounced “bang”) :

!x + 1

which takes in x, de-references it to its value, 5, and returns that value plus one, or 6

This allows us to “read” from memory, like we would in C/C++. If we want to write to a reference, we need the following operator, := , which looks like the following:

x := !x + 1

What := does when its evaluated is the following:

• Evaluate the LHS to a reference type
• Evaluate the RHS
• Assigns the reference to the new value, in this case 6

It’s important to note that these operators preserve the type of the dereferenced variable, like removing the option from an optional type. So !x has the type of int , while := will only work if the value of !x is the same type as the RHS’s value.

Ordering Expressions

Now, it might seem like these state-filled operators involve some sort of sequence. After all, the order of reads-and-writes in any computer program does matter, especially if we’re writing something non-trivial, like a parallel program. However, the whole idea of sequential execution can exist in OCaml, through the ; operator. This operator serves as a shorthand. If we have the following:

let x = ref 5 in
x := !x + 1;
x := !x * 3;
!x - 1 

This is simply shorthand for the following:

let x = ref 5 in
  let _ = (x := !x + 1) in 
    let _ = (x := !x * 3) in
      !x - 1 

where the let expressions essentially say that we don’t care about the value of the := operator, as its of type Unit, but we do care about the side-effects of the expressions, as they modify !x .

Now, it is important to stress here that x does not have value ref 5 . ref 5 is some expression that evaluates to the location in memory containing 5, and cannot be simply substituted in, as we could have before. The location is persistent, but the actual value of x does not stay ref 5

An Example

Now that we’ve covered some of the OCaml syntax for references and for iterated execution, let’s create an example to show how we can start to model some imperative semantics, even without the idea of a statement:

In Python, we could have the following code:

counter = 0
def incr_counter():
	counter = counter + 1 
  return counter
x1 = incr_counter()
x2 = incr_counter()

With our expression syntax, we could have the following OCaml code:

let counter = ref 0 in
let incr_counter () = 
   counter := !counter + 1;
   !counter in 
let x1 = incr_counter() in 
let x2 = incr_counter() in
  ...

So, yes, OCaml is really an imperative programming language, even if we hadn’t needed to do it as of yet, due to OCaml’s rich expression syntax.

Another Example, with Counters!

Say we want to package all of this up into a module. We could have the following in OCaml:

let init_counter() = 
  let counter = ref() in
    let incr_counter() =
      counter := !counter + 1;
      !counter in
    let read_counter() = 
     !counter in
    ...
Where we could then use it like the following:
let my_counter = init_counter() in 
  ...
  my_counter.incr_counter()
  ...
  my_counter.read_counter()

This would translate, more or less, into the following Python class:

class Counter:
  def __init__(self):
    self.count = 0
  def incr(self):
    self.count += 1
    return self.count
  def read(self):
    return self.count

As we can see, OOP really involves the following collection of functions:

• Functions that create state
• Functions that interact with the state

with a lot of fancy syntax

Memory, or what’s actually happening when you use reference types

So, now that we’ve covered some of the uses that simply adding memory does for us, let’s look under the hood a tiny bit. If we had the following code:

let x = ref 6 in
  let y = ref 6 in
    let xs = [!x;!y] in
      let ys = ref[x,y] in
...

We can picture each ref statement as allocating memory. So when we evaluate the following:

let x = ref 6 in

ref 6 will evaluate to a location in memory, l1, that has 6 in it. Then, when we evaluate:

let y = reg 6 in

the next ref 6 will create another new location in memory, l2, that also has six in it, after which it will assign that location to y. However, when we evaluate:

let xs = [!x;!y] in

There is no ref expression, so nothing in memory is changed and xs simply refers to [6,6] , and no new memory location is created, with xs having type int list Lastly, when we evaluate:

let ys = ref[x;y] in

We have a new ref expression, so we allocate a new location in memory, l3, which currently has the value of [l1,l2] in it, as it stores the locations where each of our 6s are, where ys has type int ref list ref , referring to l3.

In terms of deallocation, we don’t do this explicitly. Instead, OCaml has a so-called “garbage” collecter, a system which removes unused memory once there are no references to it used anymore. This is a common tactic in non-C languages, and later, in Rust, we’ll learn more about another way to approach this need to specify deallocation.

Formalism

Now that we’ve covered the idea of references in some length, let’s cover the formal rules behind them and see if we can add to ALFA this idea that pervades a lot of CS

To do so, we’ll create a new language called “ALFA Mut” which builds on ALFA, but has references!

New Types and Expression Forms

In terms of types, we’ll add a new type called a reference type:

tau ::= ...
   | Ref(tau)             tau ref

where, keeping with OCaml, we’ll write “ref” after the type if that type is a reference type for the concrete syntax.

We’ll also create the following operators for the expression language:

e ::= ...
  | Alloc(e)     alloc(e)       (refers to ref(e) in OCaml)
  | Deref(e)    !e              (like *e in C, and looks up the location in memory
  | Assign(e,e,) e1 := e2       
  | Loc[e]         (No concrete syntax, but serves as a way
                    for us to distinguish reference types)

Now, let’s move onto the typing rules for this language.

New Typing Rules

For alloc:

$\frac{\Gamma \vdash e : \tau}{\Gamma \vdash \text{alloc(e)} : \tau \text{ref}}$

Which makes sense, as alloc introduces references.

For deref:

$\frac{\Gamma \vdash e : \tau \text{ ref}}{\Gamma \vdash \text{deref(e)} : \tau}$

Which also makes sense, as deref should eliminate a reference type for a value type.

Lastly, for assignment:

$\frac{\Gamma \vdash e_1 : \tau \text{ ref , } \Gamma \vdash e_2 : \tau }{\Gamma \vdash e_1 := e_2 : \text{Unit}}$

Which makes sense, as we’re focused on the side-effects of this operation, so it shouldn’t return anything meaningful in any meaningful type.

With these done, let’s finish off with the evaluation semantics.

Dynamic Semantics

So, at first, it seems like we should be able to have the evaluation judgement:

$e \Downarrow e'$

After all, that’s worked for all of the previous incarnations of ALFA. However, if we think about it, our functions are not pure anymore, as they change memory. Thus, we really need the following new evaluation judgment:

$e || \mu \Downarrow e'||\mu '$

Where the e||mu is known as a state, and mu refers to a mapping of locations l to values e of the form l1 → e1, …, ln → en, assuming that all memory locations are distinct and reorderable.

With this in hand, we then can have the following judgements for the evaluation of ALFA Mut:

For alloc:

$\frac{e||\mu_0 \Downarrow e' || \mu_1 , (l \text{ fresh }) }{alloc(e)||\mu_0 \Downarrow \text{Loc[l]}||\mu_1, l\rightarrow e'}$

Here, we’re essentially saying that, given that e evaluates to e’, and that the rest of the program changes the state from mu0 to mu1, and that L is a fresh location in memory, allocating e evaluates to the value Loc[l] , where L refers to the evaluated expression, e’.

For deref:

$\frac{e||\mu \Downarrow \text{Loc[l]}||\mu', \mu'[l]=e'}{\text{deref(e)}||\mu\Downarrow e'||\mu'}$

Here, we’re essentially saying that, if the inner expression evaluates to a location, and if that location holds value e’, then the value of deref(e) is simply that value.

For state assignment:

$\frac{e_1||\mu_1\Downarrow \text{Loc[l]}||\mu_1',e_2||\mu_1' \Downarrow e_2'||\mu_2, l\rightarrow e_3}{e_1:=e_2 || \mu_1 \Downarrow () || \mu_2 , l \rightarrow e_2'}$

Here, we’re saying that the memory write operator evaluates to Unit, and the memory cell e1 refers to becomes the value of e2, given that e1 is a reference, e2 is a value that changes some memory potentially, and l contains some value (i.e. it’s been allocated at some point).

We’re evaluating these expressions from left to right, where the change of the state of reference e1 happens last, after you change memory states from evaluating e1 and then e2. I can picture Cyrus putting an exam question about this somewhere, so just wanted to draw attention to it.

And thus, this lecture is done. On the next lecture, we’ll probably get into more imperative constructs and turn our little pure functional language into a full on imperative one.