Borrow Checking Zero-Cost Cyclic Mutability

Ante is a low-level1 functional language built on ownership semantics and borrowing, similar to Rust. Unlike Rust, however, a core goal of Ante is to be more lenient in its borrow checker, notably by relaxing Rust’s rule that you can either alias a reference or mutate it, but never both at the same time. // In Rust: let mut my_tuple = (1, 2); let first_elem = &my_tuple.0; // error[E0506]: cannot assign to `my_tuple` because it is borrowed my_tuple = (3, 4); println!("{first_elem}"); I wanted to allow for code like the above while still disallowing code that would lead to dangling pointers, and I wanted to do this entirely statically in the type system. Alas! That’s old news - the very first blog post on this site covered it. That post is frankly quite outdated now. It’s been years since then and Ante’s approach has substantially changed, having accrued many additions to make it more flexible. Now, it has changed again, having blended many elements from group borrowing with my own ideas to produce a more radically safe whole. In this post, I want to go over the new design and show how it leads to a more flexible kind of safe, shared mutability that is expressive enough to support cyclic mutability and complex data flow safely. Since many Rustaceans are skeptical of the value of shared mutability at all, it’s worth reiterating why being more lenient here is useful. More lenience means: Fewer borrow checker errors. Fewer errors both eases the learning curve for new users and speeds up iteration times for experienced ones. More design patterns are allowed. The observer pattern is difficult to get working without shared mutability. Cyclic types can also be more directly represented. Existing design patterns can have fewer workarounds. Fewer forced indices into vectors in particular. While this can be a useful pattern, I don’t believe the language should force users into this approach. More straightforward interop with other languages that also support shared mutability. The last point in particular is more important than it seems. Ante is meant to be opt-in to ownership to some extent so that by default using it feels more like C# than it does Rust. This is an aspirational goal but allowing shared mutability greatly helps here. Aside: What was wrong with Ante’s previous rules? I imagine most will not be familiar with Ante’s old borrow checking rules, but for those curious I’ll lay out some more motivations for the change. If this isn’t you, feel free to skip this section. I am not most readers The original article mentions Ante’s ref and mut references as being &Cell<T> analogues in a way, and this has largely remained true at its core. Most of the extensions made since then were to extend this in some way, notably by introducing “local uniqueness” where a shared mutable reference only needed to be locally unique to be used where a uniq reference (think &mut T in Rust) was expected. This meant the compiler only needed to show that any variable used at the same time as a mut String did not mutably alias it. This ended up taking the form of a Distinct a b trait which was implemented if a did not occur anywhere within b. For example, if you use a Vec I32 at the same time a mut String is treated as a uniq String, the compiler would check a Distinct String (Vec I32) constraint in the background. Since a String can’t occur within a Vec I32, the code is allowed and the String is locally unique. This would be repeated for each variable used while the converted uniq String reference was still alive. Allowing what is essentially a &Cell<T> to &mut T conversion like this was great for flexibility but had a few major flaws: Common types like String would occur within other types more often making them more difficult to use compared to less common types when converted into a local uniq reference. Distinct a b recurs into every field of b, including private fields. This meant adding a private field to a public struct in a library was a breaking change since it could make previously valid local unique conversions invalid. Converting between mut and local uniq happened often, and was confusing even though the compiler did it automatically. It relied on four reference types: ref and mut which allow shared mutability, and imm and uniq which don’t. It wasn’t all bad though. Notably, it was powerful enough to encode safe, cyclic mutability, with the caveat that some Rc values had to be cloned (have their reference count incremented) during traversal. For the reasons above though, it was clear the design had to change. The rest of the article is about the new design I eventually landed on which fixes all of these issues, but still keeps the good parts like safe, cyclic mutability2 and thread-safety. The Core Problem Why are some cases of shared mutability safe, like: my_safe_fn (var pair: String, String) = name = ref pair.first pair.first := "Foo" println name // Ok! While others are not: my_unsafe_fn (vec: mut Vec t) = elem = vec.get 1 vec.clear () println elem // Dangling ref! The difference is in what I call shape stability. If the shape of a type is stable, then there is no way to mutate it such that a previously valid reference into it becomes invalid. Picturing the references in memory helps here. Let’s look at how pair and name look in memory: Before mutation: name | V pair: ((first_ptr, first_len, ..), (second_ptr, second_len, ..)) After mutation: name | V pair: ((first_ptr, first_len, ..), (second_ptr, second_len, ..)) Each String is an unboxed tuple of ptr, len, metadata, and each component of the outer pair is also unboxed. With this layout, there’s no way we could mutate pair to invalidate name! Looking at vec and elem however, we see a clear difference: Before mutation: vec: (data_ptr, length, capacity) | V [0, 1, 2, 3] ^ | elem After mutation: vec: (data_ptr, length, capacity) | V [] ^ | elem elem is clearly dangling! The problem here is that mutating vec can mutate data_ptr, causing it to potentially point elsewhere when it is reallocated. Its shape has changed, leaving elem stranded. It’d be nice if a reference type could remember whether it’s pointing at something stable or unstable - then we could do away with uniqueness in favor of a much more accurate restriction that rejects fewer valid programs. Places Over Lifetimes The first core part of the puzzle is the use of places instead of lifetimes. Unlike a lifetime which is some arbitrary symbol representing an abstract region of code a variable or reference is valid for, a place is the exact set of things a reference may borrow from: foo (x: I32) (y: I32): Unit = r1: ref 'x I32 = ref x r2: ref 'y I32 = ref y r3: ref '(x, y) I32 = if true then ref x else ref y Above, r1 borrows from only x so it has the place 'x. Similarly, r2 borrows from only y so it has the place 'y. r3 may borrow from x or y so its place is the union of both: '(x, y). Places can also be paths such as 'z.bar to represent a reference borrowing from the struct field bar on a variable z. Places don’t always name variables. There are anonymous places as well such as those for a reference to a temporary like ref 2, but that’s not important for this article. Places make borrow checking easier in general too! Borrow checking in Ante is actually very simple: whenever a value is used, error if any place it refers to has already been moved. There is truthfully a little bit more to it than that, but that really is the core and it can be implemented in only a few lines of code. Unstable Places Once we have places we can model unstable places with a simple marker: !. An unstable place like a! will be invalidated by any mutation to the place a. This also means if we have 20 variables with place a!, we can mutate them all simultaneously since mutating them would only invalidate variables with place a!!. This is a bit abstract though, so let’s see how this works in practice. Starting off, we have some Rust code which should be safe but gets rejected by the compiler: fn rejected(v: &mut Vec<String>) { // error: cannot borrow `*v` as mutable more than once at a time let (first, last) = (v.first_mut().unwrap(), v.last_mut().unwrap()); *first = "Mutate first".to_string(); println!("{last}"); } Rust’s compiler rejects this even though there is no way we can mutate first which would invalidate last. Theoretically, even if the first element is also the last, this code should still be valid3. We can model this in Ante by flagging any references to returned elements of a vector as unstable: // Declare a `first_mut` method taking a mutable vector and returning // an unstable reference inside 'v to the first element Vec.first_mut (v: mut Vec t): mut 'v! t can Fail = ... Vec.last_mut (v: mut Vec t): mut 'v! t can Fail = ... Now, we can write the equivalent of rejected just fine: not_rejected (v: mut Vec String) = first, last = v.first_mut (), v.last_mut () first.* := "Mutate first" println last // ok! Above, first and last both have the type mut 'v! String so when we mutate first it would prevent us from using anything with a place of v!!4, but nothing does. So we’re free to use both first and last even if they alias. Whether a reference is unstable or not is inferred in practice and doesn’t always need to be a manual choice by users. Any reference through a tagged union or element of a collection type will be unstable for example. Loops Loops and branching in general are fairly straightforward. They largely follow the same rules ownership has where an error is issued if a variable declared outside of the loop is invalidated within it: var v = Vec.of [1, 2, 3] one = v.get 0 for _ in 0 .. 3 do println one // error: one may be invalidated by a later mutation in the for loop v.clear () // note: one invalidated here Similarly, any closure which invalidates any part of its captured environment is treated as a FnOnce in Rust terms, preventing it from being called more than a single time.