Creator of Ante here, Ante inherits Rust's Send/Sync for thread-safety. `mut` refs and `Rc` which provides shared mutability don't implement either and thus can't be shared across threads. So shared mutability is only within a single thread.
OOI why did you go with RC at the lattice bottom rather than generational refs? Not sure how in touch you are with the author of Vale?
What would be good is if effects are used to discharge the ownership obligations, that should dovetail well in Ante. BTW I appreciate the clear effects handling in Ante, very nice!
Given their "shape stability" design, not necessarily. The three ways that multithreaded access can cause UB are:
* changing the type of the underlying memory (e.g. because it's part of an enum variant and you changed the tag, or because you changed the length of a vector)
* data races (can be defined away by making [effectively] every access Relaxed, as Java does
* use after free (resolved here by reference counting)
In Rust, any type specified like this (all accesses are Relaxed, "shape stable", and reference counted) can already be used in safe code using & references. In theory. But the first property (forcing all accesses to be Relaxed) is very annoying to achieve for arbitrary user data types--even if those types are Copy or other kinds of plain old data--which is a problem e.g. for specifying stuff like sequence locking. The example they give here with bare unions is also very annoying to use in Rust even though this mode of use is safe, because the type system doesn't track which variant is active. So I definitely think there's room to innovate ergonomically here.
(It does seem from the text like this is intended for a single-threaded context, where I think the arguments against Cell are a little less persuasive, but it's still true that it's very awkward to try to figure out how to safely project a Cell down to the exact fields you need to mutate, even though something like LambdaRust will tell you it's safe to do so).
By accepting semantics like this you are, of course, opting out of a lot of potential optimizations around both shared and unique accesses, but you are already doing this in most langauges anyway, so if you're willing to eat the performance cost this can be quite acceptable. The bigger problem (briefly noted in the post) is that the kind of recursive analysis they're proposing doesn't necessarily compose well. Rust explicitly opted out of most types of analysis that can't be efficiently summarized at the function signature level to improve compilation speed. Historically, not being able to efficiently summarize functions that do this kind of stuff has been a big thing that killed attempts to automatically add borrow checking like facilities onto existing C++ code, too. But maybe a language designed for it from the ground up will avoid this problem.
Jake has already mentioned how the type system enforces single-threading (using similar mechanisms as Rc in Rust), but it's not necessarily the case that read-write races from multiple threads are UB.
In particular, Java allows aggressive multithreaded access, and the memory model has some pretty strong guarantees. Informally stated, if a read and a write race, then the read is guaranteed to observe either the old or new value.
Go is something of a middle ground [1]. Races on simple scalar values are not UB, but "fat pointers" (slices and interfaces) can tear and can lead to "arbitrary memory corruption."
When I was reading about "stable shape" I was wondering if it might be something similar. You easily get the same UB problems when dealing with sum types, as a tear across tag and variant payload can cause all kinds of things to go wrong.
Not if you define the behavior. Many programming languages have robust memory models ranging from "happens before" style systems like those in Java or Modern C++ to the Software Transactional Memory system in GHC/Haskell.
Correct, shared mutation is an extremely well-understood problem in the sense that there are points in the programming language design space that admit it with present technology.
I am pretty skeptical about the whole idea about adding such exceptions to the single mutable reference rule. It may be safe to share references to simple structs in terms of raw bytes access, but as long as some non-trivial invariants are involved, it can be a source of nasty bugs.
In my programming language I generally don't allow having more than one mutable reference to a variable. The only exception is when two references point to different elements of structs/tuples. This gives some flexibility without sacrificing correctness.
Interesting but I wonder how useful this is in practice. It doesn't work with unions/enums, I presume it also doesn't work with heap allocated containers, like vectors, hash maps, etc? Wouldn't that rule out like 90% of typical data structures?
Also, there's definitely something to be said for Rust's ownership rules improving code quality. I wonder if that would be affected if you relax them like this?
> Because of this, Ante code can safely have multiple mutable borrow references to the same struct at the same time.
I doubt it can work in multithreaded code. Allowing sharing mutable references (even to simple structs) means race conditions, temporal inconsistency between different struct fields and even incorrect read results for basic integer types (if the target CPU can't atomically read/write values of types like u64).
I'm really looking forward to the next generation of languages. Not only are the old 90's languages like Java, PHP, and JavaScript now actually doing things correctly. The new languages like Zig, Go, Swift and Rust continue to figure out new ways of trying things like generics. Spinoffs like V, Ante, and others are perfect testing grounds.
What would your ideal version look like? I recommend reading the C++ or Rust equivalent code in the article. I like the example because it is copied 1:1 with example code from a textbook with only some keywords changed and a Copy constraint. Any other language without a GC and with unboxed types today represents it far more verbosely to the point where the meaning becomes obscured and a typo becomes more likely to survive code review.
surprised to see that, I've long held tree balancing up as practically the poster child for ML syntax being the best way to express certain algorithms. it directly says what shape of nodes goes to what other shape.
Most uses of `uniq` in the article aren't necessary and are just included for explicitness. Anywhere a `uniq` ref is required but you only have a `mut` ref, Ante will convert it to a `local uniq` ref with the various rules required while it is still in scope. So you'll still be protected and will get the same compile errors if you try to access an alias while the locally unique reference is still alive.
Creator of Ante here. It's just a term I made up for mutation which does not change the "shape" of data in a way that can invalidate any of that data. Mutating a struct or tuple field, even if nested, is stable for example, but mutating an optional string to None is not because you may be dropping a string which there may be a reference to somewhere.
I see, so would it would only be relevant to unions, or would adding a new node to a linked list or pushing another element in a dynamic array or setting a pointer to null also count?
As far as I understand, every change to indirections (pointers) is “shape unstable”, as it the update invalidates the old value, which causes every reference into that to be dangling (rather than merely modified).
Adding a new node at the end of a linked list, or more generally setting an unset pointer, would technically be shape-stable as you can’t have a reference into nothing. Generally pushing an element in a dynamic array is not shape-stable (the array can need to reallocate), although there would be workarounds e.g. a push which fails on lack of capacity would be shape-stable. Some sort of hybrid (e.g. rrb) would also work as extension consists of adding new node (possibly re-rooting the tree) but does not invalidate existing nodes.
The interesting bit here is treating Rc<T> and &T as compatible via a shared representation, so you can hand an Rc to a function expecting a borrow without bumping the count. Swift already does something adjacent with its guaranteed vs owned parameter conventions eliding retain/release pairs, but that's an optimization pass, not a type-level guarantee. Making it explicit in the signature is nicer because you can reason about when a clone actually happens.
The part I'm skeptical about is cycles. Once you lean on RC as the escape hatch for graph-shaped data, you inherit the weak-reference discipline problem that Rust users hit with Rc<RefCell<T>>. Ante doesn't seem to address that directly, and region inference has historically been fragile at scale (see the ML region work that got abandoned for tracing GC). Also, if a borrowed T is really a pointer into an Rc allocation, you need to guarantee the count can't hit zero during the borrow, which either requires the caller to hold the Rc live across the call or some form of stack pinning. Curious how they handle re-entrancy through a callback that drops the last strong ref.
Creator of Ante here, passing `Rc<T>` as `&T` or `&Rc<T>` is a somewhat standard practice Ante inherits from Rust and C++ here.
As for cycles, `Rc t` in Ante isn't magic and when used in cycles it will leak. Ante does not use region inference, just the related, derived field of borrow-checking. The family tree there roughly resembles MLKit -> Cyclone -> Rust -> Ante in that regard.
When borrowing the inner element of an `Rc t`, the type system ensures that the resulting `ref t` cannot be dropped while it is still held. In particular, dereferencing an `Rc t` requires a unique value, but only gives you a shared value to the element: `Rc.as_mut: fn (uniq Rc t) -> mut t`. In practice, this means if you only have a shared ref to an Rc but need a reference to the element inside, you either need to clone the outer Rc (guaranteeing it won't be dropped while the borrow is alive), or use the local uniqueness conversion and avoid using any possible aliases while using the reference.
I can see how multiple mutable references is fine in a single-threaded context, but surely this would cause UB in the multi-thread context?
Creator of Ante here, Ante inherits Rust's Send/Sync for thread-safety. `mut` refs and `Rc` which provides shared mutability don't implement either and thus can't be shared across threads. So shared mutability is only within a single thread.
OOI why did you go with RC at the lattice bottom rather than generational refs? Not sure how in touch you are with the author of Vale?
What would be good is if effects are used to discharge the ownership obligations, that should dovetail well in Ante. BTW I appreciate the clear effects handling in Ante, very nice!
> Not sure how in touch you are with the author of Vale?
FYI - this article is written by the author of Vale
Given their "shape stability" design, not necessarily. The three ways that multithreaded access can cause UB are:
* changing the type of the underlying memory (e.g. because it's part of an enum variant and you changed the tag, or because you changed the length of a vector) * data races (can be defined away by making [effectively] every access Relaxed, as Java does * use after free (resolved here by reference counting)
In Rust, any type specified like this (all accesses are Relaxed, "shape stable", and reference counted) can already be used in safe code using & references. In theory. But the first property (forcing all accesses to be Relaxed) is very annoying to achieve for arbitrary user data types--even if those types are Copy or other kinds of plain old data--which is a problem e.g. for specifying stuff like sequence locking. The example they give here with bare unions is also very annoying to use in Rust even though this mode of use is safe, because the type system doesn't track which variant is active. So I definitely think there's room to innovate ergonomically here.
(It does seem from the text like this is intended for a single-threaded context, where I think the arguments against Cell are a little less persuasive, but it's still true that it's very awkward to try to figure out how to safely project a Cell down to the exact fields you need to mutate, even though something like LambdaRust will tell you it's safe to do so).
By accepting semantics like this you are, of course, opting out of a lot of potential optimizations around both shared and unique accesses, but you are already doing this in most langauges anyway, so if you're willing to eat the performance cost this can be quite acceptable. The bigger problem (briefly noted in the post) is that the kind of recursive analysis they're proposing doesn't necessarily compose well. Rust explicitly opted out of most types of analysis that can't be efficiently summarized at the function signature level to improve compilation speed. Historically, not being able to efficiently summarize functions that do this kind of stuff has been a big thing that killed attempts to automatically add borrow checking like facilities onto existing C++ code, too. But maybe a language designed for it from the ground up will avoid this problem.
I was thinking of the data race case, and I was unaware of relaxed access used by other languages. Thanks for sharing!
Jake has already mentioned how the type system enforces single-threading (using similar mechanisms as Rc in Rust), but it's not necessarily the case that read-write races from multiple threads are UB.
In particular, Java allows aggressive multithreaded access, and the memory model has some pretty strong guarantees. Informally stated, if a read and a write race, then the read is guaranteed to observe either the old or new value.
Go is something of a middle ground [1]. Races on simple scalar values are not UB, but "fat pointers" (slices and interfaces) can tear and can lead to "arbitrary memory corruption."
When I was reading about "stable shape" I was wondering if it might be something similar. You easily get the same UB problems when dealing with sum types, as a tear across tag and variant payload can cause all kinds of things to go wrong.
[1]: https://go.dev/ref/mem
Not if you define the behavior. Many programming languages have robust memory models ranging from "happens before" style systems like those in Java or Modern C++ to the Software Transactional Memory system in GHC/Haskell.
Correct, shared mutation is an extremely well-understood problem in the sense that there are points in the programming language design space that admit it with present technology.
As always, there are tradeoffs.
I am pretty skeptical about the whole idea about adding such exceptions to the single mutable reference rule. It may be safe to share references to simple structs in terms of raw bytes access, but as long as some non-trivial invariants are involved, it can be a source of nasty bugs.
In my programming language I generally don't allow having more than one mutable reference to a variable. The only exception is when two references point to different elements of structs/tuples. This gives some flexibility without sacrificing correctness.
Interesting but I wonder how useful this is in practice. It doesn't work with unions/enums, I presume it also doesn't work with heap allocated containers, like vectors, hash maps, etc? Wouldn't that rule out like 90% of typical data structures?
Also, there's definitely something to be said for Rust's ownership rules improving code quality. I wonder if that would be affected if you relax them like this?
Very interesting anyway!
> Because of this, Ante code can safely have multiple mutable borrow references to the same struct at the same time.
I doubt it can work in multithreaded code. Allowing sharing mutable references (even to simple structs) means race conditions, temporal inconsistency between different struct fields and even incorrect read results for basic integer types (if the target CPU can't atomically read/write values of types like u64).
What about Vale? Is this a rename of it or something new?
Hi, article's author here (Verdagon, Vale's creator), and no, I'm just writing about someone else's language (Ante) that I thought was interesting.
Ante is making some very intriguing steps forward in memory safety design and I thought others would find it interesting too.
Thank you for clarifying!
I'm really looking forward to the next generation of languages. Not only are the old 90's languages like Java, PHP, and JavaScript now actually doing things correctly. The new languages like Zig, Go, Swift and Rust continue to figure out new ways of trying things like generics. Spinoffs like V, Ante, and others are perfect testing grounds.
>I'm really looking forward to the next generation of languages.
me too!
>"I have to admit, this is beautiful"
Terse it is, beautiful it is not (well my version of beautiful that is - easy to read and understand). this is not to diminish the language.
What would your ideal version look like? I recommend reading the C++ or Rust equivalent code in the article. I like the example because it is copied 1:1 with example code from a textbook with only some keywords changed and a Copy constraint. Any other language without a GC and with unboxed types today represents it far more verbosely to the point where the meaning becomes obscured and a typo becomes more likely to survive code review.
That's what I thought too when I first saw it. But then I actually took a moment to read it and eventually changed my mind.
surprised to see that, I've long held tree balancing up as practically the poster child for ML syntax being the best way to express certain algorithms. it directly says what shape of nodes goes to what other shape.
What if I omit the "uniq" keyword? Is it still valid code, just not protected by the compiler from union types changing underneath?
Most uses of `uniq` in the article aren't necessary and are just included for explicitness. Anywhere a `uniq` ref is required but you only have a `mut` ref, Ante will convert it to a `local uniq` ref with the various rules required while it is still in scope. So you'll still be protected and will get the same compile errors if you try to access an alias while the locally unique reference is still alive.
Highly interesting. I hope this language reaches a production release some time.
What is "stable shape"?
Creator of Ante here. It's just a term I made up for mutation which does not change the "shape" of data in a way that can invalidate any of that data. Mutating a struct or tuple field, even if nested, is stable for example, but mutating an optional string to None is not because you may be dropping a string which there may be a reference to somewhere.
I see, so would it would only be relevant to unions, or would adding a new node to a linked list or pushing another element in a dynamic array or setting a pointer to null also count?
As far as I understand, every change to indirections (pointers) is “shape unstable”, as it the update invalidates the old value, which causes every reference into that to be dangling (rather than merely modified).
Adding a new node at the end of a linked list, or more generally setting an unset pointer, would technically be shape-stable as you can’t have a reference into nothing. Generally pushing an element in a dynamic array is not shape-stable (the array can need to reallocate), although there would be workarounds e.g. a push which fails on lack of capacity would be shape-stable. Some sort of hybrid (e.g. rrb) would also work as extension consists of adding new node (possibly re-rooting the tree) but does not invalidate existing nodes.
The interesting bit here is treating Rc<T> and &T as compatible via a shared representation, so you can hand an Rc to a function expecting a borrow without bumping the count. Swift already does something adjacent with its guaranteed vs owned parameter conventions eliding retain/release pairs, but that's an optimization pass, not a type-level guarantee. Making it explicit in the signature is nicer because you can reason about when a clone actually happens.
The part I'm skeptical about is cycles. Once you lean on RC as the escape hatch for graph-shaped data, you inherit the weak-reference discipline problem that Rust users hit with Rc<RefCell<T>>. Ante doesn't seem to address that directly, and region inference has historically been fragile at scale (see the ML region work that got abandoned for tracing GC). Also, if a borrowed T is really a pointer into an Rc allocation, you need to guarantee the count can't hit zero during the borrow, which either requires the caller to hold the Rc live across the call or some form of stack pinning. Curious how they handle re-entrancy through a callback that drops the last strong ref.
Creator of Ante here, passing `Rc<T>` as `&T` or `&Rc<T>` is a somewhat standard practice Ante inherits from Rust and C++ here.
As for cycles, `Rc t` in Ante isn't magic and when used in cycles it will leak. Ante does not use region inference, just the related, derived field of borrow-checking. The family tree there roughly resembles MLKit -> Cyclone -> Rust -> Ante in that regard.
When borrowing the inner element of an `Rc t`, the type system ensures that the resulting `ref t` cannot be dropped while it is still held. In particular, dereferencing an `Rc t` requires a unique value, but only gives you a shared value to the element: `Rc.as_mut: fn (uniq Rc t) -> mut t`. In practice, this means if you only have a shared ref to an Rc but need a reference to the element inside, you either need to clone the outer Rc (guaranteeing it won't be dropped while the borrow is alive), or use the local uniqueness conversion and avoid using any possible aliases while using the reference.