jfecher

You generally don't have to enforce any invariants manually unless you're implementing your own abstractions from unsafe primitives like raw pointers.

Multi-threading in general is made safe by separate mechanisms which don't permit shared mutability, but there's little reason to restrict it on a single thread when it can be verified to be safe. You still cannot mutate a collection while iterating over it for example, but you can easily mutate disjoint parts of it which is something I commonly encounter in Rust.

It should be fixed with Polonius, that's why it is mentioned in the paragraph after the example. Polonius reframes borrowing from lifetimes to places similarly to Ante so this is meant to show some advantages of this approach even without adding extra rules for unstable places, etc.

Ante shares parts of its approach with Valen - both having been based on the group borrowing concept. I'm in contact with its author and we share ideas every now and then. Ante is mentioned at the end of that article too. There are actually several upcoming languages using group borrowing (or something similar) as a base now - Ante, Valen, Carbon, Zeta, Fang, Mojo, and likely more.

There are a few parts of this overall approach that'd be difficult to fix in Rust without making it an entirely different language I think. The first would be separation of use vs reference, so users can pass around mutable references without the language thinking they may be mutated, and the second would be changing Rust's core semantics to allow shared mutability in general. With internal mutability like GhostCell this is allowed via UnsafeCell but I'd imagine making every reference UnsafeCell by default wouldn't be optimal and quite a few internal changes would be required.

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.

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.

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.

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.

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.

> I'm actually hoping to find a way to blend Nick's approach seamlessly with reference counting (preferably without risking panics or deadlocks) to get the best of both worlds, so that we can consider it for Mojo. I consider that the holy grail of memory safety, and some recent developments give me some hope for that!

Ante's approach manages to blend a similar scheme for safe, shared mutability with Rc. There are some examples on the most recent blog post on its website of it. IMO combined with its shared types it emulates high-level GC'd code very well.

Right, compared to explicitly passing the parameter, with effects:

- You wouldn't have to edit the body of the function to thread through the parameter. - The `can Use Strings` part can be inferred (and in Ante's case, it is my goal to have the compiler write in inferred types for you so that top-level definitions can be inferred if desired but still annotated when committed for code review). - Most notably, the `can Use Strings` can be included in a type alias. You could have an alias `MyEffects = can Use Strings, Throw FooError`, etc for the effects commonly used in your program. If your state type is used pervasively throughout, this could be a good option. When you have such an alias it also means you'd just be editing the alias rather than every function individually.

Generally though, while I think the passing around of state through effects can be useful it isn't the most convincing use of effects. I mention it more for "here's another benefit they can have" rather than "here's this amazing reason you should definitely use them for"

> As I understand it, AE on low level is implemented as a longjmp instruction with register handling (so you can resume).

Not quite. setjmp/lonjmp as they exist in C at least can jump up the call stack but not back down. I mention this at the end of the article but each language implements algebraic effects differently, and efficiency has improved in recent years. Languages can also optimize the effect differently based on how the handler is defined:

- Handlers which are tail-resumptive can implement the effect as a normal closure call.

- Handlers which don't call resume can be implemented as an exception or just return an error value at every step until the function exits the handler.

- Handlers which perform work after resume is called (e.g. `| my_effect x -> foo (); resume (); bar ()` can be implemented with e.g. segmented call stacks.

- Handlers where resume is called multiple times need an equivalent of a delimited continuation.

Another way to implement these generally is to transform the effects into monads. For any set of effects you can translate it into a monad transformer where each effect is its own monad, or the free monad can be used as well. The cost in this approach is often from boxing closures passed to the bind function.

Koka has its own approach where it translates effects to capability passing then bubbles them up to the handler (returns an error value until it gets to the handler).

With just a few restrictions you can even specialize effects & handlers out of the program completely. This is what Effekt does.

There really are a lot of options here. I have some links at the end of the article in the foot notes on papers for Koka and Effekt that implement the approaches above if you're interested.

If the database effect wrote to a file it'd require the `IO` effect and code using it would need that effect as well. A compiler can generally show a function to be free of most side effects if it uses no effects. The exceptions to this are things like divergence. As long as the language is Turing complete you can't prove it won't loop forever of course. Another exception could be extern functions which the compiler can't verify the correctness of the type signature. Different languages handle these differently but if users are allowed to write any (and the language doesn't force them to have an IO effect) then they can be a source of unsafety. Languages like Koka and Effekt are considered pure though and enforce this through their effect systems.