CS 242: Assignment 6: Linear Types

Due: Thursday, November 7, 2019 at 11:59pm
Submission cutoff: Sunday, November 10, 2019 at 11:59pm

How do big ideas in programming languages come about? As I mentioned on the first day of class, inspiration comes from many places, whether from hardware or mathematics. The Rust reference lists sixteen programming languages that directly influenced its development. In this assignment, we will explore the theoretical underpinnings of linear types, an idea that led to the core design feature of Rust, the borrow checker. Then you’ll get some practice with linearity in Rust by implementing a binary search tree data structure.

1: Linear type theory (60%)

Linear types originate in a theory of linear logic, which represents the idea that truth is a finite resource that can be used once, but not duplicated or discarded. Which sounds strange, but just wait til you read the Wikipedia explanation:

Linear logic is a substructural logic proposed by Jean-Yves Girard as a refinement of classical and intuitionistic logic, joining the dualities of the former with many of the constructive properties of the latter. Proof-theoretically, it derives from an analysis of classical sequent calculus in which uses of (the structural rules) contraction and weakening are carefully controlled. Operationally, this means that logical deduction is no longer merely about an ever-expanding collection of persistent “truths”, but also a way of manipulating resources that cannot always be duplicated or thrown away at will. In terms of simple denotational models, linear logic may be seen as refining the interpretation of intuitionistic logic by replacing cartesian (closed) categories by symmetric monoidal (closed) categories, or the interpretation of classical logic by replacing boolean algebras by C*-algebras.

Ah yes, a substructural logic refining cartesian closed categories with symmetric monoidal categories, of course really just a C*-algebra. Clearly.

Just as the lambda calculus originated as a formalism for mathematics, and developed into a system of computation, so too did linear logic follow a path into computer science. Philip Wadler, a big name in PL theory research, published a paper in the 1990s called: “Linear types can change the world!” In this paper, he showed how the theory of linear logic applies to the lambda calculus. Specifically, he argued that linear types permitted an efficient implementation of in-place mutations and allocations of data structures in a way that standard functional programming could not.

In this part of the assignment, your task will be to read sections of Wadler’s paper, understand the fundamentals of linear types, then modify a compiler to use linear types and enable efficient usage of memory.

1.1: Read the paper (20%)

First, you should read the introduction and sections 1 and 2 of Wadler’s paper. Everything won’t make complete sense on the first read-through, but the hope is that your earlier experience in this course gives you the necessary foundations for understanding Wadler’s presentation of linear types.

To check your understanding, answer the following questions in part 1.1 of the written homework:

In your own words, what does Wadler mean by his aphorism “linear types can change the world”? How does this contrast with a functional programming language without linear types?
Below are a few examples of programs in Wadler’s linear lambda calculus. For each one, if it has a type, then say what the type is, and if it does not have a type, explain in English the issue.
- $\lfun{x}{\ltyprim{Bool}}{\ltyprim{True}}$
- $\lfun {x}{\ltyprim{Bool}}{(\lcase{x}{ \ltyprim{True} \rightarrow \ltyprim{False} \mid \ltyprim{False} \rightarrow \ltyprim{True}})}$
- $\lfun {x}{\ltyprim{Bool}}{(\lcase{x}{ \ltyprim{True} \rightarrow x \mid \ltyprim{False} \rightarrow \ltyprim{True}})}$
- $\lfun{l}{\ltyprim{List}}{ \lfun{f}{\ltyfun{\ltyprim{Val}}{\ltyprim{Val}}} {\lcase{l}{\ltyprim{Nil} \rightarrow \ltyprim{Nil} \mid \ltyprim{Cons}~x~l' \rightarrow \ltyprim{Cons}~(\lapp{f}{x})~l'}}}$

1.2: String language compiler

If you skim over section 4 and 5 of Wadler’s paper, he discusses an array language as an example of using linear types to efficiently update an array. The example is a little convoluted, so we’re going to implement a simpler version of the same idea as a string language. Specifically, we will create a tiny imperative string DSL:

$\begin{alignat*}{2} \msf{Expression}~e ::= \\ \mid \qamp s \qqamp \text{string literal} \\ \mid \qamp \sconcat{e_1}{e_2} \qqamp \text{string concatenation} \\ \mid \qamp x \qqamp \text{variable} \\ \mid \qamp x(e^*) \qqamp \text{function call} \\[1.2em] \msf{Statement}~stmt ::= \\ \mid \qamp x = e \qqamp \text{variable assignment} \\ \mid \qamp \sreturn{e} \qqamp \text{function return} \\[1.2em] \msf{Function}~f ::= \qamp \{\msf{name}{:}~s; ~\msf{params}{:}~s^*; ~\msf{body}{:}~stmt^*\}\\[1.2em] \msf{Program}~p ::= \qamp f^* \end{alignat*}$

The semantics are fairly simple. All a function can do is either create a string, concatenate it to another string, assign to a variable, or call another function. The only type of data in the language is strings, so we can define a static semantics using a simple “valid” judgment:

$\ir{T-String} {} {\validJC{s}} \s \ir{T-Concat} {\validJC{e_1} \s \validJC{e_2}} {\validJC{\sconcat{e_1}{e_2}}} \s \ir{T-Var} {x \in \ctx.\msf{vars}} {\validJC{x}} \nl \ir{T-Call} {f = \ctx.\msf{funcs}[x] \s |e| = |f.\msf{params}| \s \forall e_i . \validJC{e_i}} {\validJC{x(e^*)}} \nl \ir{T-Assign} {\validJC{e} \s \validJ{\{\ctx~\with~\msf{vars}{:}~\ctx.\msf{vars}, x\}}{stmt^*}} {\validJC{x = e, stmt^*}} \nl \ir{T-Return} {\validJC{e}} {\validJC{\sreturn{e}}} \s \ir{T-Function} {\validJC{f.\msf{body}}} {\validJC{f}} \nl \ir{T-Program} {\ctx = \{\msf{funcs}{:}~\{f_i.\msf{name} \rightarrow f \mid f_i \in f\}\} \s \forall f_i . \validJC{f_i}} {f^*~\msf{valid}}$

The language definition and the type-checker have been provided for you in assign6/program/ocaml/src/slang.ml. See the type definitions and the implementation of the typecheck_* functions, and make sure you believe that they correspond to the syntax/semantics above.

Rather than implement an interpreter for the language directly, our goal is to compile this imperative language into efficient WebAssembly. In wasm.mli, we have provided the type definitions for a subset of WASM. Then in translate.ml, we implement the function:

val translate : Slang.prog -> Wasm.module_

This function takes a program in the Slang programming language above and converts it into a WASM module. Most of the translation has been provided for you. Carefully study each translate_* function to understand how the translation works. At a high level:

A function in Slang maps to a function in WASM.
Each assignment in Slang becomes an assignment to a function-local variable in WASM.
String data is stored in memory as a sequence of characters (NOT null-terminated). A string header is two numbers, an address and a length, stored on the stack (length at the top of the stack, address beneath it).
Runtime memory allocation is provided by an external allocator, called with (call $alloc) and (call $dealloc). $alloc takes a length and returns an address of a memory allocation of that many slots. $dealloc takes an address and frees it.

For example, consider the translation for Slang.String s.

match e with
| Slang.String s ->
  let n : int = String.length s in
  let stores : instr list =
    String.to_list s
    |> List.mapi ~f:(fun (i : int) (c : char) ->
      [GetLocal "s"; Const i; Binop `Add; (* Compute the address *)
       Const (Char.to_int c);             (* Get the character value *)
       Store])                            (* Store it in memory *)
    |> List.concat
  in
  [Const n; Call "alloc"; SetLocal "s"]
  @ stores @
  [GetLocal "s"; Const n]

To create a string constant, the code allocates n slots and places the allocated address into the local s. Then it copies each character into the appropriate place in the string, and finally places the address and length on the stack.

Ultimately, your goal is to implement the translation for Slang.Concat such that its arguments can be immediately deallocated after performing the concatenation. For example, the expression x = "a"; return x ^ "b" should allocate "a", then allocate "b", then allocate/copy "ab", and immediately deallocate the a/b strings before returning.

However, this strategy does not work in the presence of aliasing. For example, the program x = "a"; return x ^ x would free x twice, causing a memory error. Hence, you will also change the type system above to be linear, requiring that all variables are used exactly once.

Testing Framework

It is assumed that your machine has Node.js installed. We have provided a similar test harness as in assignment 5. To get started:

In the assign6/program/wasm directory, run npm install && npm install wasm-alloc once to set up your dependencies.
In the same directory, run npm start to start a local web server. It should open a web page in your browser that contains the function tests.

More details about the tests will be discussed in 1.4.

1.3: Converting to linear types (20%)

Your first task is to change the type system in assign6/program/ocaml/src/slang.ml to be linear in variable assignments (but not function calls). That is, all variables must be used exactly once. After completing 1.4, your compiler should not be able to generate programs that have double frees, dangling pointers, or memory leaks.

You can make any level of structural changes to the provided starter code. The only requirement is that the signature typecheck remain unchanged, as it is the only function exported by the slang module. For example, you may want to think about changing the return type of typecheck_expr.

Testing

The assert tests provided in assign6/program/ocaml/src/main.ml check basic functionality of your typechecker. Feel free to add additional programs and assert statements.

1.4: Implementing `Concat` translation (20%)

Now that your type system is linear, you can safely implement an efficient Concat operation. In assign6/program/ocaml/src/translate.ml, fill in the Slang.Concat branch of translate_expr. Specifically, your operation should have the behavior:

After executing the two subexpressions, the top of the stack should be two strings, i.e. the stack has the shape [s1, n1, s2, n2] for string 1, length 1, string 2, length 2 (where “length 2” is at the top of the stack).
Concat should allocate a new string s3 of length n1 + n2 and copy s1 and s2 into the appropriate locations. The resulting string s3 should be returned.
We have provided you a function $memcpy that takes a source address, destination address, and length (in that order), and copies numbers from the source to the destination over the length.
If you want to use local variables during your computation, you should add them to the runtime_locals list at the top of translate.ml so the corresponding (local $x i32) declaration is included in the WASM module.

Testing

If your typechecker successfully typechecks one of the test programs, it will generate a .wat file of the module. The Node app will then test the functionality of your translated program. Specifically, we expect p_basic, p_concat, and p_funcall to typecheck. From these programs, we will then generate a .wat file, whose output will be checked by the Node app. Our suggestion is to not change the structure of any of these function to not interfere with our testing framework.

If you wish to write additional tests to check the output of a program which successfully typechecks, refer to const module_srcs in assign6/program/wasm/src/index.js to change the sources of your WebAssembly modules and to assign6/program/wasm/src/tests.js for example tests.

2: Rusty search trees (40%)

The string language is useful for understanding at a low-level how Rust can use an ownership model to implement efficient compile-time memory mangement. However, you also need a sense of how to build nontrivial systems and data structures using linear type mechanics. In this problem, you will implement a binary search tree in Rust.

2.1: Objects and enums in Rust

We briefly touched on objects in the Rust lab, but I wanted to discuss them in greater detail, particularly with an emphasis on ownership and borrowing.

`impl` blocks

In Rust, you can associate a function with a type (usually a struct) using an impl block:

use std::ops::Add;
use std::fmt::Display;

struct Point<T> { x: T, y: T }

impl<T: Add<Output=T> + Display + Copy> Point<T> {
  fn new(x: T, y: T) -> Point<T> {
    Point { x, y }
  }

  fn print(&self) {
    println!("({}, {})", self.x, self.y);
  }

  fn add_inplace(&mut self, other: &Point<T>) {
    self.x = self.x + other.x;
    self.y = self.y + other.y;
  }

  fn destroy(self) {}
}

The impl block allows you to associate functions with types (“methods” in an object-oriented vernacular). For example, new takes as input an x and y, returning a Point. By placing it in the impl block, we can now write: Point::new(1, 2) to create a point.

Functions in an impl block can have the special first argument self, &self, or &mut self. When you use the dot notation p.print(), this desugars to Point::print(&p). The notation of &self vs &mut self indicates whether the function expects an owned version of the type, an immutable reference, or a mutable reference. Intuitively, a function that takes &self can only read the self value. A function that takes &mut self can change the self value, and a function that takes self consumes ownership. For example, this sequence is valid:

let mut p: Point<i32> = Point::new(1, 2);
p.print(); // (1, 2)
let p2 = Point::new(3, 4);
p.add_inplace(&mut p2);
p.destroy();
// p.print(); <-- invalid, since p is moved after destroy

Again, when you do p.print() or p.add_inplace(...), this implicitly takes a pointer on p. So the mutation desugars as Point::add_inplace(&mut p, &mut p2).

The syntax impl<T: Add<Output=T> + Display + Copy> defines the capabilities of the type T using traits. We’ll talk more about this in lecture on Monday, but for now you can interpret this as: the type T must be addable to another T, it must be convertable into a string, and it must be bit-for-bit copyable without ownership problems (see Copy for explanation).

BST usage

In assign6/program/rust/src/lib.rs we have provided you the skeleton of a binary search tree library. It starts with the data type:

pub enum BinaryTree<T> {
  Leaf,
  Node(T, Box<BinaryTree<T>>, Box<BinaryTree<T>>)
}

The BST is parameterized by the element type T. A tree is either a leaf, or a node with an element, and a left/right subtree. Recall that a binary search tree has the invariant that at a given node with an element $t$ , all elements $t_L$ in the left sub-tree satisfy $t_L \leq t$ , and conversely $t_R \geq t$ for $t_R$ in the right-subtree. For example, if we want to create the tree:

  B
 / \
A   D

We can encode that in Rust as:

let mut t1: BinaryTree<&str> = Node(
  "B",
  Box::new(Node("A", Box::new(Leaf), Box::new(Leaf))),
  Box::new(Node("D", Box::new(Leaf), Box::new(Leaf))));
assert_eq!(t.len(), 3);

You are going to implement methods for the BST inside an impl block. For example, the length function:

impl<T: Debug + Display + PartialOrd> BinaryTree<T> {
  pub fn len(&self) -> usize {
     // TODO
  }

  // remaining methods...
}

One key question is, how does borrowing interact with a BST as a sum type? For example, if I do:

pub fn len(&self) -> usize {
   match self {
     BinaryTree::Leaf => { /* TODO */ },
     BinaryTree::Node(t, l, r) => { /* TODO */ }
   }
}

What are the types of t, l, and r? Because len takes &self as input, then self has type &BinaryTree<T>. When we match on self, we similarly get an & reference to each component. So t: &T, l: &Box<BinaryTree<T>>, and r: &Box<BinaryTree<T>>. Because Box has Rust trait magic, l and r actually have type &Box<BinaryTree<T>> or type &BinaryTree<T> based on their usage (i.e. the reference is forwarded from the Box struct to the actual value on the heap).

Pointer dereference

One other question you’ll run into: when do you need to dereference a pointer explicitly? As mentioned in lecture, Rust has a significant amount of inference/syntactic sugar to automatically insert pointer dereferences. For example:

let t: BinaryTree<i32> = Box::new(BinaryTree::Leaf);
let t: &&&BinaryTree<i32> = &&&t;
assert_eq!(t.len(), 0);

The Rust compiler will automatically dereference your 3-layer pointer down to an &BinaryTree<i32> before passing it to len. You could, for example, manually write this as:

assert_eq!(BinaryTree::len(**t), 0);

In the reference solution, we only need to use an explicit dereference in the following cases. First, if you have an &mut self mutable reference, you can replace the self entirely with a dereference assignment. For example:

pub fn replace_with_leaf(&mut self) {
  *self = BinaryTree::Leaf;
}

Second, if you have an element t1: T and another element t2: &T, and you want to compare them for inequality, you will have to explicitly dereference the reference like t1 >= *t2.

Finally, if you have an owned value tree: Box<BinaryTree<T>> and you want to move the BinaryTree<T> out of the box (i.e. off the heap and onto the stack), you can do:

let heap_tree: Box<BinaryTree<i32>> = Box::new(BinaryTree::Leaf);
let stack_tree: BinaryTree<i32> = *heap_tree;
// println!("{:?}", heap_tree); <-- invalid, heap_tree is moved
println!("{:?}", stack_tree); // valid!

2.2: BST interface (40%)

Next, you are going to implement a series of methods for the BST. You are free to introduce helper functions as necessary, or use any function in the Rust standard library.

len(&self) -> i32 (4%)

This function returns the number of nodes in the BST. Leaves do not count as nodes. For example:
```
assert_eq!(t.len(), 3)
```
to_vec(&self) -> Vec<&T> (4%)

This function converts the BST to a vector sorted in the same order as the tree. The elements of the vector are pointers to elements in the BST.
```
assert_eq!(t.to_vec(), vec!["A", "B", "D"]);
```
sorted(&self) -> bool (4%)

This function checks the sorted invariant of the search tree, i.e. that each node is properly greater than its left tree and less than its right tree.
```
assert!(t.sorted())
```
insert(&mut self, t: T) (4%)

This function adds a node to the BST. It should walk the tree until finding an appropriate leaf to replace.
```
t.insert("D");
```
search(&self, query: &T) -> Option<&T> (4%)

This function returns the smallest element greater than or equal to the query element. If no such element exists, then return None.
```
assert_Eq!(t.search(&"B"), Some(&"B"));
assert_eq!(t.search(&"C"), Some(&"D"));
assert_eq!(t.search(&"E"), None);
```
rebalance(&mut self) (20%)

This function performs a single rebalancing operation on the BST in-place (if applicable). The rebalancing algorithm is to lift the closest element on the larger sub-tree up to the root, rotating the former root as the root of a subtree. For example:
```
     D               C
    / \             / \
   B   E   -->     B   D
  / \             /     \
 A   C           A       E
```
```
A                  B
 \                / \
  B     -->      A   C
   \                  \
    C                  D
     \
      D
```
```
     E               D
    / \             / \
   B   F   -->     B   E
    \               \   \
     D               C   F
    /
   C
```
Our criterion for rebalancing is if the size of one subtree is at least two greater than the other subtree. In the last example, the subtrees of E are size 3 and 1, respectively, so we rebalance from left to right. Here, the rebalancing procedure walks down the right spine of the left subtree to find the element D. Then it moves that element up to the root, and replaces D with its left subtree of C. The second example shows the same procedure, but rebalancing right to left.

This function is tricky to implement in Rust, since we want to move data around while avoid cloning any data within the tree. (Cloning data is impossible even if we wanted to, because T: Clone is not a bound of our type parameter.) For example, let’s say we want to remove the left sub-tree of the running t1 example. In C++, this might be accomplished by setting tmp = t1.left; t1.left = NULL. However, we don’t have null pointers in Rust, and a tree node must always have a valid subtree. Instead, we can use mem::replace to perform surgery on the tree.
```
let t1_ref = &mut t1;
let left: Box<BinaryTree<&str>> = match t1_ref {
  BinaryTree::Node(t, left, right) => {
    mem::replace(left, Box::new(BinaryTree::Leaf))
  },
  BinaryTree::Leaf => unreachable!()
};
```
Feel free to add your own private helper functions to the impl block.

Testing

We have provided a handful of basic functionality tests at the bottom of program/ocaml/lib.rs. Follow the examples as noted in the Rust lab to run the tests. Feel free to add your own.

Submission

Run ./make_submission.sh in the program directory and upload the newly created assign6.zip file to the Gradescope programming assignment. We are expecting changes in ocaml/src/slang.ml, ocaml/src/translate.ml, and rust/src/lib.rs. Submit your write up for Problem 1 as well.

Sections

1: Linear type theory (60%)

1.1: Read the paper (20%)

1.2: String language compiler

Testing Framework

1.3: Converting to linear types (20%)

Testing

1.4: Implementing Concat translation (20%)

Testing

2: Rusty search trees (40%)

2.1: Objects and enums in Rust

impl blocks

BST usage

Pointer dereference

2.2: BST interface (40%)

Testing

Submission

1.4: Implementing `Concat` translation (20%)

`impl` blocks