Linearity and uniqueness

In the last post, we looked at uniqueness mode and how uniqueness may be used to optimise. As we will see, uniqueness alone is insufficient in practice, and we also need a concept of linearity for uniqueness to be useful.

Capturing unique values

Let’s start with an example. Recall the signature of the unique reference module.

module type Unique_ref = sig
  type 'a t
  val alloc : 'a -> 'a t @ unique
  val free : 'a t @ unique -> unit
  val get : 'a t @ unique -> 'a Modes.Aliased.t * 'a t @ unique
  val set : 'a t @ unique -> 'a -> 'a t @ unique
end

Assume that we also have an implementation of the module:

module Unique_ref : Unique_ref

Consider the following example, which works fine:

let works () =
  let t = alloc 42 in (* Allocate a unique reference *)
  free t (* free it *)

Now consider this modified example:

let wat () =
  let t = alloc 42 in (* Allocate a unique reference *)
  let f () = free t in (* capture free in a closure *)
  f (); (* free it *)
  f () (* free it again??? *)

Observe that f has captured t in the closure, and when called frees t. It should be clear that calling f more than once is bad – leads to a double-free issue! What property do we want of f? Uniqueness is insufficient; we have a unique reference to f in this program, with which we call f twice.

What we want to enforce is that f can be called at most once. The compiler has a linearity mode which captures the idea of how many times a value can be used. We have two modes in the linearity axis – once, which stands for “at most once” and many (the default one for all values), which allows values to be used arbitrary number of times.

Whenever a unique value is captured by a closure, the closure gets a once mode, which allows the closure to be called at most once. This program rightly gets rejected by the compiler.

File "./unique_ref.ml", line 32, characters 2-3:
32 |   f () (* free it again??? *)
       ^
Error: This value is used here,
       but it is defined as once and has already been used:
File "./unique_ref.ml", line 31, characters 2-3:
31 |   f (); (* free it *)
       ^

A linear ref

Now, one might wonder whether the unique reference that we’ve implemented may be implemented with the linear mode. The answer is yes.

module type Linear_ref = sig
  type 'a t
  val alloc : 'a -> 'a t @ once
  val free : 'a t @ once -> unit
  val get : 'a t @ once -> 'a * 'a t @ once
  val set : 'a t @ once -> 'a -> 'a t @ once
end

module Linear_ref : Linear_ref = struct
  type 'a t = { mutable value : 'a }
  let alloc x = { value = x }
  let free t = ()
  let get t =
    t.value, t
  let set t x =
    t.value <- x;
    t
end

This works as expected:

open Linear_ref

let works () =
  let r = alloc 42 in
  let v,r = get r in
  let r = set r (v + 1) in
  let v,r = get r in
  print_int v;
  free r;
  ()

let fails () =
  let r = alloc 42 in
  free r;
  get r (* fails here *)

with the error message:

File "./linear_ref.ml", line 34, characters 6-7:
34 |   get r (* fails here *)
           ^
Error: This value is used here,
       but it is defined as once and has already been used:
File "./linear_ref.ml", line 33, characters 7-8:
33 |   free r;

Why both linearity and uniqueness?

Given this example, you might be wondering, if the safe reference may be implemented equivalently using both uniqueness and linearity, why do we need both? Obviously, there’s something interesting going on where unique values captured in a closure needs linearity. Does that mean linearity is sufficient?

It turns out that only recently was the relationship between the two formally studied in the same type system. While linear types and uniqueness types have a long history of being studied independently, Marshall et al. in their paper, “Linearity and Uniqueness: An Entente Cordiale”, present the ideas in the same type system. They provide some key insights.

The first insight is that

in a setting where all values must be linear, we can also guarantee that every value is unique, and vice versa! Intuitively, if it is never possible to duplicate a value, then it will never be possible for said value to have multiple references.

In our Unique_ref and Linear_ref every operation that operates on the ref requires uniqueness or linearity, respectively. Hence, they seem almost equivalent in expressive power.

It is when we also have the ability for unrestricted use (non-linear/non-unique) that differences between linearity and uniqueness begin to arise, as we will soon see.

In our language, we do have the ability for unrestricted use. That is, in the linearity axis, many is the default mode attributed to all the values not tagged or inferred as once. Similarly, aliased is the default mode attributed to all the values not tagged or inferred as unique.

The type system has submoding: values may move freely to greater modes (which typically restrict what can be done with those values) but not to lesser modes. For example, a many value may be safely use in a context where a once value is expected.

let works () =
  let set_to_20 (r @ once) =
    r := 20
  in
  let r @ many = ref 10 in
  set_to_20 r (* [r @ many] is passed to a function that expects [int ref @ once] *)

Similarly, you can use a unique value in a context where an aliased value is expected.

let dup r = r,r

let works () =
  let r = Unique_ref.alloc 42 in
  let a,b = dup r in
  a,b

The type of the works function is val works : unit -> int Unique_ref.t * int Unique_ref.t, which crucially lacks the fact that the references are at unique mode. We can’t call any functions from the Unique_ref module with these references, all of which expect a reference with unique mode.

Uniqueness is more appropriate for safe refs

In our running example of implementing a safe ref, it turns out that uniqueness is more appropriate. Consider the type signature of free in Unique_ref:

val free : 'a t @ unique -> unit

The type signature says that there are no other aliases to this reference. Hence, its memory may be safely deallocated. However, consider the Linear_ref.free signature:

val free : 'a t @ once -> unit

The signature says that this reference must be used at most once. In particular, just by looking at the signature, we cannot conclude that there are no other aliases to this reference. But we know that the API is safe since the only way to create a safe reference is through the alloc function, which returns a once-usable reference, and every other operation also expects and returns a once-usable reference.

The correctness of the linear version depends on reasoning over the whole API, whereas the unique version can be concluded to be safe just by looking at the signature of the free function. This modular reasoning makes uniqueness more appropriate for our safe reference API.

Past and the future

In a sense, uniqueness and linearity are duals of each other. Uniqueness talks about the past – whether a value may be aliased in the past. It is okay to alias a unique value in the future and lose the uniqueness mode. Linearity talks about the future – whether a value may be used more than once in the future. You can take any value and ascribe a linear mode to it, restricting its use in the future. However, there may be other aliases to this value in the past.

Conclusions

The code examples are available here. Section 2.1 of Marshall et al.’s paper is quite readable and explains the distinction between linearity and uniqueness with some historical context. I highly recommend it.

Acknowledgements

Thanks to Richard Eisenberg for the discussions which spurred this post.