Borrow Checking Zero-Cost Cyclic Mutability

(antelang.org)

23 points | by jfecher 1 day ago

2 comments

  • Animats 2 minutes ago
    Hm. One example from the article:

        match map.get_mut(&key) {
        //    --- first mutable borrow occurs here
            Some(value) => value,
            None => {
                map.insert(key, V::default());
                //  ^~~~~~ error[E0499]: cannot borrow `*map` as mutable more than once at a time
                map.get_mut(&key).unwrap()
            }
        }
    
    That's a limitation of the current Rust borrow checker. The problem is that the argument of match is never used again on the None path, which should end the range of the borrow before the None branch starts. But, currently, it doesn't. The range of the borrow is too closely tied to scope.

    This is supposed to be fixed with the Polonius borrow checker. It doesn't require a new language, just something that ends the lifetime of a borrow at the last use.

    Wasn't this covered yesterday with the article about the Vale language? It seems related.

    Regarding cycles, that looks interesting. GhostCell dates from 2021 but got stuck at "alpha quality". The usual approach to cycles in Rust, or at least backlinks, involves Rc, RefCell, and Weak. Forward links are strong, back links are weak.

    I've suggested creating OwnerRc, which is like Rc but not cloneable. That's a single owner Rc. If you drop an OwnerRc, it panics if there are any outstanding weak links. This is useful because you no longer have to check when upgrading a Weak - it always works.

    So these are fixable language problems without the need for a new language and new terminology.

  • nathanwh 48 minutes ago
    “ 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.”

    From an application programmers standpoint, isn’t this much weaker? Part of the appeal of not having shared mutability is not having to worry about data races in general, while this shape stability approach prevents some classes of data races it requires others to be enforced by the programmer, as far as I can tell.

    It’s hard for me to tell the net effect of this, maybe preventing reference errors is enough, but I suspect that once you start having to enforce other invariants manually, it will feel like the savings from the automatic shape stability enforcement are not enough of an improvement over languages without any significant compile time memory safety checks.