Ante has taken the first step towards something we all thought was impossible: blending reference counting and borrow checking without run-time crashes. 0
This is very promising, because it means that someday, we can more easily use each approach when it makes sense without risking crashes. If there was a language like that, I could prototype a game in a flexible way with reference-counting, and gradually migrate it to faster borrow-checked code. 1
No mainstream language has figured out how to combine them seamlessly, even though many have tried.
Rust tried, but when we try to use Rust's reference-counting Rc type, it often requires RefCell (like Rc<RefCell<Spaceship>>) which can crash at run-time if you hold it wrong. 2 3 I wish rustc could check for proper Rc usage at compile-time! 4 5
Swift too has tried, with its new borrowing system, but it has an expensive run-time check which crashes at run-time if you hold it wrong.
It turns out, blending reference counting and borrow checking is hard, for reasons you'll see below.
So let's talk about Ante!
To be more specific, Ante has found a way to blend reference counting and borrow checking for mutable objects, without run-time panics or overhead that come from Rust's RefCell or Swift's exclusivity checking.
This is close to the same reason I work on Vale! But Vale uses generational references, which often risk these exact kinds of program halts.
For example, two people getting unique (read-write) references to it at the same time would crash it.
It also has try_borrow() and try_borrow_mut() methods which don't panic, but just moves the problem somewhere else.
And alas, GhostCell / QCell doesn't count, they bring in other limitations and aren't a drop-in replacement for RefCell.
There is Cell, but it doesn't let you get references to its innards. For example you can’t go from &Cell<(T, U)> to a &Cell<U>. Rust also tends to have a lot of friction when internal mutability is used in general, leading to many users avoiding it.
Ante aims to be a simpler Rust, a systems programming language with memory-safety and thread-safety. It has single ownership and borrow checking, so values are inline (on the stack, or in the containing struct/array).
And when the user wants to prioritize simplicity, they can opt into reference counting with the shared keyword on their types.
For example, this snippet would balance a red-black tree:
// Color can be either an R or a B
shared type Color = | R | B
// RbTree can either be an Empty or a Tree
shared type RbTree t =
| Empty
| Tree Color (RbTree t) t (RbTree t)
// A balance function, for RbTree of any element type t
balance (tree: RbTree t) {Copy t}: RbTree t =
match tree
| Tree B (Tree R (Tree R a x b) y c) z d
| Tree B (Tree R a x (Tree R b y c)) z d
| Tree B a x (Tree R (Tree R b y c) z d)
| Tree B a x (Tree R b y (Tree R c z d)) -> Tree R (Tree B a x b) y (Tree B c z d)
| other -> otherI normally favor C-style syntax, but even I have to admit, this is beautiful. And it's concise too, as small as the Python equivalent, and smaller than the C++ equivalent and Rust equivalent.
But the most interesting thing for me is what Ante is doing in memory safety. Ante has shared mutability superpowers: if you want to mutably borrow reference-counted data, you don't need to risk run-time errors. No mainstream language can do that, not even Rust or Swift.
Before I talk about its shared mutability superpowers, let's start basic. Let's see how it does borrow checking, and then we'll add reference counting into the mix.
Ante has a concept of shape-stability, which means "a reference to something of stable shape is always valid 6 no matter what mutations are made elsewhere."
Because of this, Ante code can safely have multiple mutable borrow references to the same struct at the same time.
To set the stage, here's a heal function taking two mutable references to Entitys:
type Entity =
energy: I32
health: I32
heal (healer: mut Entity) (target: mut Entity) =
healer.energy := healer.energy - 10
target.health := target.health + 10In Ante, we can call heal with the same Entity for both parameters — for example, when an entity heals itself:
self_heal (entity: mut Entity) =
heal entity entityMutating healer can't invalidate shared references to the Entity in any way, 7 so the compiler accepts this code as valid.
In other words, even though healer and target might point to the same Entity, this is memory safe: nothing here can destroy the Entity, so both references stay valid. 8
Now let's get a little more complicated.
Ante code can actually have multiple mutable borrow references to the same struct, or any of its struct fields, or any of their struct fields, at the same time.
For example, here we have a mutable borrow reference pointing at the ship, and another mutable borrow reference pointing at the ship's engine, at the same time.
type Engine =
fuel: I32
type Spaceship =
engine: Engine
name: String
refuel (ship: mut Spaceship) =
engine_alias: mut Engine = ship.engine
// Can still use original `ship`
ship.engine.fuel := 200
engine_alias.fuel := 100Ante knows this is completely memory safe, because during this function, nobody can destroy ship, and therefore nobody can destroy its engine or its fuel.
In other words, these references are to shape-stable data.
Those familiar with Rust and Swift will be surprised by this:
Now let's add some reference counting into the mix!
Here, "valid" means dereferenceable; you can dereference the reference without risking any memory unsafety or undefined behavior.
Similar to how in Rust you can't use a &mut Spaceship to destroy the Spaceship it's pointing at. Even in Rust, it would be perfectly safe to have multiple &mut Spaceship references pointing at the same Spaceship local variable.
Similar to how in Rust you can't use a &mut Spaceship to destroy the Spaceship it's pointing at. Even in Rust, it would be perfectly safe to have multiple &mut Spaceship references pointing at the same Spaceship local variable.
We can sometimes get close with Cell, but see the appendix section for why Ante goes further than Rust's Cell.
The above ability is a perfect fit with reference counting, as we'll see below.
In Ante, if you put shared in front of a type definition, it means that type is automatically reference counted. 10
And when you have a shared mut type, you can mutate its fields without locking, like set_fuel is doing to Spaceship's engine: Engine field:
type Engine =
fuel: I32
shared mut type Spaceship =
engine: Engine
name: String
launch (var ship: Spaceship) =
set_fuel (mut ship.engine)
set_fuel (engine: mut Engine) =
engine.fuel := 100I'll explain this snippet further below, but for now: this is similar to the Rust equivalent and Swift equivalent, but without the crash risk of Rust's .borrow_mut() or Swift's automatic run-time exclusivity checking.
launch can make a mut Engine borrow reference because launch knows the engine will stay alive because launch is keeping the containing Spaceship alive.
More generally: you can always make a mut borrow reference to a shared mut type's fields, even though they are shared. 11
At least for now. Eventually, the application (not the code) will be able to configure how their memory is managed, e.g. via RC, GC, or a custom mechanism.
Though, you can't always take a mut borrow reference to the things inside those fields, as we'll see later. There are different mechanisms for that.
From here on out, I'll be using the more explicit Rc Spaceship syntax instead of the shared mut type syntactic sugar (you'll see why later).
With the more explicit Rc syntax, the above snippet would look like this: 12
type Engine =
fuel: I32
type Spaceship =
engine: Engine
name: String
launch (var ship: Rc Spaceship) =
set_fuel (mut ship.engine)
set_fuel (engine: mut Engine) =
engine.fuel := 100Differences:
We're assuming an Ante syntax where we can access fields of an Rc's contents. Without it, this might instead be something like set_fuel (ship.as_mut ()).engine
Unions are really good for speed. 13 We like unions.
Unfortunately, unions are notoriously unsafe, and it's hard for memory-safe languages to support them well.
To see why, look at the below example, where Engine is a union, and we're trying to do unsafe shenanigans with it.
type Engine =
| StringTheoryEngine (str: String)
| ImpulseEngine (fuel: I32)
type Spaceship =
engine: Engine
name: String
launch (var ship: Rc Spaceship) (var other_ship: Rc Spaceship) =
match uniq ship.engine
| StringTheoryEngine str ->
other_ship.engine := ImpulseEngine 0x42
str.[0] := 'z'
| ImpulseEngine fuel ->
()This program can actually segfault if we pass the same Spaceship in for both ship and other_ship!
For this reason, Ante needs to refuse to compile the above. Ante has this rule:
If you have a mut borrow reference to a union, you cannot make a mut borrow reference to one of its variants.
This is the opposite of the struct rule from before:
If you have a mut borrow reference to a struct, you can make a mut borrow reference to one of its fields.
In a perfect world, Ante would refuse the above program with an error like this:
match uniq ship.engine
| StringTheoryEngine str ->
// error: Mutating `other_ship.engine` may cause `ship.engine` to be dropped while still in use
// note: `other_ship.engine` is an `Engine` which may alias with `ship.engine`
other_ship.engine := ImpulseEngine 0x42
str.[0] := 'z'
| ImpulseEngine fuel ->
()But how would Ante know that? Is that even possible?
It is! Ante knows to give this error because ship.engine went through a temporary uniq conversion.
So what do I mean by that, and what is uniq?
Unions are fast because they hold their contents inline, which leads to less cache misses (or "pointer chasing"). For example, in C if we have a union like this:
union Engine {
StringTheoryEngine ste;
ImpuseEngine ie;
};and it's inside a Spaceship like:
struct Spaceship {
Engine engine;
};The StringTheoryEngine and ImpulseEngine live inside the Spaceship's memory.
Other languages such as Java don't do this, they instead make Engine into an interface, and make Spaceship contain a Engine pointer instead.
Pointers are slow. Unions are fast. Ante is like C here.
uniq means "exclusive mutable reference".
If a variable contains a uniq Spaceship, then it's the only usable reference to that Spaceship. 14
set_fuel (engine: uniq Engine) (other: mut Engine) =
// In here, we know nothing else points to `engine` This is generally not useful on its own, but it does allow us to point into the contents of unions.
Ante's uniq Spaceship is similar to a Rust &mut Spaceship.
Because there may be other aliases to the same data, it would not be safe to allow arbitrary mutation of union fields.
For example, one user may be holding a String from a Maybe String while another user mutates it to None.
Or, like we saw in the above example, someone destroyed the String's container while someone else held a reference to one of its characters.
Languages generally patch this issue either via reference counting so the String lives on (Swift), or by banning shared mutability altogether (Rust).
But even though we want to prevent the above unsafe program, we want to allow programs that safely have mutable references into unions' contents:
type Engine =
| StringTheoryEngine (str: String)
| ImpulseEngine (fuel: I32)
type Spaceship =
engine: Engine
name: String
launch (var ship: Rc Spaceship) =
match uniq ship.engine // match statements require uniq references
| StringTheoryEngine str -> // Get uniq reference to StringTheoryEngine
str.[0] := 'z'
| ImpulseEngine fuel ->
()The equivalent programs in e.g. Swift and Rust allow this safe program by, unfortunately, adding extra run-time overhead/checks.
Fortunately, Ante doesn't need extra run-time overhead/checks because it understands that nobody is changing ship.engine while we're in this function.
Ante knows that because of its temporary uniq conversion mechanism.
Ante's insight is that we can temporarily get a uniq reference to something, as long as in that scope we don't access anything else that might reference it.
For example, here's a program with a uniq conversion, with comments showing where that scope begins and ends:
type Engine =
| StringTheoryEngine (str: String)
| ImpulseEngine (fuel: I32)
type Spaceship =
engine: Engine
name: String
launch (var ship: Rc Spaceship) =
// Start scope where nobody can access any other var that might contain a Spaceship
match uniq ship.engine
| StringTheoryEngine str ->
str.[0] := 'z'
| ImpulseEngine fuel ->
()
// End scope where nobody can access any other var that might contain a SpaceshipThe uniq reference exists in scope between the // Start scope and // End scope comments (more specifically, everything in between ship's declaration and its last use).
While the uniq reference exists, Ante prevents us from using any other pre-existing variable that might indirectly contain a Spaceship.
Whereas Rust prevents the uniq from existing "because other references might exist elsewhere", Ante says that we can make the uniq as long as we don't use those references in this scope.
However, there are some limitations.
If we used another local variable inside that scope (such as another Rc Spaceship) that might indirectly refer to a Spaceship, we'd get a compile error:
type Engine =
| StringTheoryEngine (str: String)
| ImpulseEngine (fuel: I32)
type Spaceship =
engine: Engine
name: String
launch (var ship: Rc Spaceship) (var other_ship: Rc Spaceship) =
// Start scope where nobody can access any other var that might contain a Spaceship
match uniq ship.engine
| StringTheoryEngine str ->
// error: Mutating `other_ship.engine` may cause `ship.engine` to be dropped while still in use
// note: `other_ship.engine` is an `Engine` which may alias with `ship.engine`
other_ship.engine := ImpulseEngine 0x42
str.[0] := 'z'
| ImpulseEngine fuel ->
()
// End scope where nobody can access any other var that might contain a SpaceshipThis is an error because we're accessing other_ship while ship is temporarily converted to a uniq Spaceship.
We can't use anything that even indirectly contains a Spaceship, 15 so this would be rejected too:
type Engine =
| StringTheoryEngine (str: String)
| ImpulseEngine (fuel: I32)
type Spaceship =
engine: Engine
name: String
type HasAShip =
ship: Rc Spaceship
launch (var ship: Rc Spaceship) (var other: HasAShip) =
// Start scope where nobody can access any other var that might contain a Spaceship
match uniq ship.engine
| StringTheoryEngine str ->
// error: Mutating `other.ship.engine` may cause `ship.engine` to be dropped while still in use
// note: `other.ship.engine` is an `Engine` which may alias with `ship.engine`
other.ship.engine := ImpulseEngine 0x42
str.[0] := 'z'
| ImpulseEngine fuel ->
()
// End scope where nobody can access any other var that might contain a SpaceshipNote that we can use anything else, for example an integer new_fuel:
type Engine =
| StringTheoryEngine (str: String)
| ImpulseEngine (fuel: I32)
type Spaceship =
engine: Engine
name: String
launch (var ship: Rc Spaceship) (new_fuel: I32) =
// Start scope where nobody can access any other var that might contain a Spaceship
match uniq ship.engine
| StringTheoryEngine str ->
str.[0] := 'z'
| ImpulseEngine fuel ->
fuel := new_fuel
// End scope where nobody can access any other var that might contain a SpaceshipWe can use new_fuel because it's just an I32, it can't contain any references to a Spaceship. It's just an integer.
Also, if Spaceship contained a field like follow_ship: Rc Spaceship it would be rejected, because then that uniq Spaceship is also reachable via that. So generally, one can't do a mut->uniq conversion on a recursive type.
Here's an example that does a mut->uniq conversion as part of a function call.
type Resonator =
resonance: I32
type Engine =
| ImpulseEngine (fuel: I32)
| WarpEngine (resonators: Vec Resonator)
type Spaceship =
engine: Engine
name: String
foo (var ship: Rc Spaceship) (new_res: Resonator) =
// Start scope where nobody can access any other var that might contain a Spaceship
maybe_use_resonator ship new_res // converts to `uniq` here
// End scope where nobody can access any other var that might contain a Spaceship
maybe_use_resonator (u_ship: uniq Spaceship) (new_res: Resonator) =
match u_ship.engine
| WarpEngine resonators ->
resonators.push new_res
| ImpulseEngine fuel ->
()Remember, the rule is that we can temporarily get a uniq reference to something, as long as in that scope we don't access anything else that might reference it.
As you can see from the comments, the compiler really just needs to check the maybe_use_resonator callsite, to check that none of the arguments contain anything that might have a reference to a Spaceship. And the only other argument (Resonator) does not, so we're good!
The main restriction with the mut to uniq conversion is that you cannot return converted uniq references from a function: 16
get_converted (foo: mut Foo): uniq Foo =
// Attempt to convert mut -> uniq
foo // error: `local uniq` refs cannot be returned as `uniq`Luckily, we can still get what we want by specifying the returned reference is only locally unique:
get_converted (foo: mut Foo): local uniq Foo =
// Convert mut -> local uniq
fooThis is actually always what is happening internally anyway, whenever we convert from a mut ref to a uniq ref, we only get a local uniq one back. Most of the time we can use this as a normal uniq ref, but when returning values we have to specify it explicitly.
If this were allowed, the returned uniq reference could be used without the compiler checks that ensure that no variable in scope can be used which may alias the converted reference.
Ante can temporarily turn an RC reference (Rc Spaceship) into a unique borrow reference (uniq Spaceship) without run-time errors, and that's a huge step forward. 17
It does have a downside however. As Jake (Ante's creator) emphasized to me, this does require some type analysis: answering the question "Can we reach a Spaceship from an Engine?" requires the compiler to recursively look through Engine and everything it contains, to make sure that nothing contains a Spaceship. This could be pretty brittle; adding fields to a struct can be a breaking API change.
And for that reason, Jake's looking for a better way to uphold that guarantee, with some promising options:
I think there could be other options as well:
Even with these possible angles, the hard part will be making it ergonomic. Jake's goal with Ante is to make something usable, readable, and simple. Doing that while offering maximum flexibility is always tricky.
This is, in a way, a compile-time RefCell, and is what C++ users have internalized since the dawn of time. Jake's found a way to build it into a memory safety approach.
I and a few others have been exploring this angle lately.
If you look closely, you'll see that something very interesting is happening in the realms of memory safety design.
We used to think that it was impossible to have "shared mutable borrowing", where we could have a borrowed reference to something, even though others can mutate it through their own references. Heck, Rust is basically built on that belief.
But we're starting to see a lot of exceptions pile up:
This isn't just a bag of tricks. This is the universe telling us, very strongly, that the unifying principle is right there, in front of us.
I'll mysteriously leave that unifying principle vague and unexplained for now. Leave a comment if you know what I'm talking about!
Let's get zen for a minute. We are like water, in a complex landscape full of mountains and valleys. It's easy to follow the path of least resistance and flow into a valley, where we can't see much. It's hard to climb to the top of the mountains and see farther.
And that's why we have articles like this! Every new technique is another tool to help us climb the mountains and see farther. All we need to do is keep adding tools, and we'll inevitably find the next big advances in memory safety.
If you enjoy articles like this, stay tuned and subscribe to the RSS feed, r/vale, twitter, and bluesky. To follow Ante’s development, check out its website and its discord.
Cheers!
- Evan
The savvy Rust user will ask, "how is this different from putting Cells in structs?"
To illustrate the question, here's a program in Ante, and the equivalent Rust one with Cells below it:
type Spaceship =
fuel: I32
status: String
// Example: changes "Enterprise" to "Enterprise (refueling)"
add_to_name (var ship: Rc Spaceship) =
status_ref: mut String = (ship.as_mut ()).status // Get reference to the status String itself
status_ref += " (refueling)"And the Rust version:
struct Spaceship {
fuel: Cell<i32>,
status: Cell<String>,
}
// Example: changes "Enterprise" to "Enterprise (refueling)"
fn add_to_name(ship: Rc<Spaceship>) {
let status_ref = &ship.status; // Can't get the &String, but can get &Cell<String>
let mut status = status_ref.replace(String::new()); // Temporarily put something in its place
status += " (refueling)";
status_ref.replace(status); // Swap the modified name back into place
}Rust has a limitation here: Given an Rc<Spaceship>, there's no way to get a &mut String that we can add to. So instead, Rust has to swap a default value in and remember to put it back.
This has a few downsides:
That last will sound familiar: this Cell is basically a RefCell!
Ante approaches this differently: it lets you temporarily get a reference to the status string, and the compiler enforces that nobody else can access it while you're doing that.