Borrow Checking Zero-Cost Cyclic Mutability

[u/RndmPrsn11]

https://antelang.org/blog/safe_cyclic_mutability/

[u/ChampiiPote]

This is very interesting, I am also working on my own compiler and we share a lot of design goals (https://github.com/Rock-lang-org/Rock) I might take some inspiration from you work, it looks very nice !

[u/RndmPrsn11 → u/ChampiiPote]

I read this as Roc at first, what was the motivation behind the name?

[u/initial-algebra]

The ad-hoc and "hacky" rules for loops, closures and especially algebraic effects (not to mention trying to split any of this code up into functions) are exactly why you still need lifetimes in addition to places.

Creating a reference to p! would introduce an obligation that p itself must not be mutated for the lifetime of that reference. How to represent that obligation? Add a new effect, something like Stabilize p t, where t is a lifetime parameter, meaning "at any time during t, p! may be used". Dually, you could add a lifetime parameter for Mutate p t, which would mean "at any time during t, p may be mutated".

While mutually exclusive, a function may need both Stabilize and Mutate for the same place p, and seemingly for the same lifetime (e.g. for the duration of the function call), so how can that work? In reality, the function needs Stabilize p u₁ and Mutate p u₂, where u₁ and u₂ are non-overlapping and possibly non-contiguous subsets of an overall lifetime t, but the caller doesn't know exactly what u₁ and u₂ are, only the approximate t. One solution is to introduce a new effect to mean (Stabilize XOR Mutate) p t, where the callee gets to choose whether it is Stabilize p u or Mutate p u for each disjoint u ⊆ t.

There is one more change that I want to suggest. Instead of being unstable places, references to variants of tagged unions, elements of collections etc. should require immutability of an abstract field representing the parent's shape (abstract because it doesn't need to correspond to a real field that you can take a reference to--the tag of a tagged union may be optimized away, and for e.g. a vector it actually corresponds both to its length and its pointer). Technically, this models such types as dependent sum types, with the shape being the index; see representable/Naperian functors in type theory. This changes Stabilize to Immutable (you would also want to change the tense of Mutate and the can keyword for consistency). Having a generic immutability effect also opens up the possibility of subsuming imm and uniq references. An imm reference arises when you require immutability for a lifetime, and a uniq reference arises when you require both immutability and mutability for (again, unknown but disjoint subsets of) a lifetime.

EDIT: Because what I've called "lifetimes" aren't necessarily contiguous, and because they don't necessarily come from liveness analysis, they might deserve a different name.

[u/RndmPrsn11 → u/initial-algebra]

I'd push back on any of the rules for loops or closures being hacky. They follow rules for moves 1:1 so I think they're quite clean actually. The rules for effect handlers are a bit hacky I think, but also not yet finalized from a design standpoint. I hope to have time again soon to find a cleaner solution there.

Creating a reference to p! would introduce an obligation that p itself must not be mutated for the lifetime of that reference

The relationship is already encoded in the unstable place so I don't think a new trait would be necessary (Mutate itself is also technically unnecessary with polymorphic refs).

should require immutability of an abstract field representing the parent's shape

The invalidation rules already model the immutability rule you mention. Abstract places would be a useful thing to have, I mention them in footnote 6, but they're currently unimplemented. Thankfully, most commonly used types in the stdlib don't require this. Something like Vec for example is fine with loaning elements as 'v! without a dedicated 'v.elements! since there is no other source of unstable refs it needs to differentiate from.

[u/GiveMe30Dollars]

Interesting read!

I think that Polonius is much more similar to your borrow checker than you realise, being place-based and invalidating shared references (always unstable) when a place is mutated or a mutable reference is obtained. Partial borrows have also been a thing that is played around within the Rust community (it already exists! Just that the language lacks the syntax to express it within function signatures).

However, the effect system inducing place invalidation and distinguishing between stable and unstable references to allow for shared mutability is pretty cool! This is the first time I've seen clearly how a type system with shared mutability (shared borrows in particular) can be safe. Will need some time to chew through it but this does seem like an evolution of Polonius (which I consider pretty great lol). May try my hand at implementing something like this (albeit smaller).

I'll be keeping an eye out for Ante!