Neat!
I have a question about immutability. In Rust, if I have a shared reference to T (an &T a variable or a parameter), then I have a restriction that I can't modify T or anything in it (which Valen thinks is annoyingly restrictive, and I tend to agree), but I also have a promise that no one else will modify it. The latter is quite nice: it makes the optimizer happier (improves aliasing analysis), makes threading happier (nothing descended from the reference can have data races while the reference is alive), and makes me happier (I don't need to think about descendent values being mutated).
Valen can call into Rust, and I think I can see how, at the site of any particular call, Valen can tell that no one is mutating the referent or its descendents: in a single-threaded world, the only thing executing is the current line of code or a maybe a few consecutive lines of code, and the compiler can see the function's signature and any mutable references therein, and if there is no permission to modify a descendent, then it doesn't get modified.
But in a multithreaded world, especially if calling into Rust in a thread, doesn't there need to be a way to guarantee the immutability of an object across an entire region of code? How does that work in Valen?
And for making immutability more comprehensible to people and to local analysis in general, would a special type of reference meaning "yes, this one really is fully frozen and there are no mutable paths into it for the entire lifetime of this reference" be a nice feature?
(Aside: I've occasionally contemplated whether Rust would benefit from another flavor of reference: no-access. A no-access reference would guarantee the referent's existence but could coexist with shared and with mutable references. Safe code would be unable to read or write through such a reference. Other than making some cell-like types mildly less mind-bending, I'm not convinced I have an actual justification for this thing. This would give Rust three flavors of references.
But I can imagine a Valen-like language having three flavors of references: frozen references (cannot use them to mutate and there's a promise that no one else can either), exclusive references (fully mutable, etc, just like Rust's &mut) and flexible references (the kind of reference in the blog post).)
I've occasionally contemplated whether Rust would benefit from another flavor of reference: no-access.
Most of the uses for this I can think of are best solved by opaque pointers for FFI. Having a rust-native reference just seems incongruous. Like, does it have size and alignment info? How would it interact with NLL? The only way I can imagine it working is if it extended referent lifetime throughout the lexical lifetime of the reference, but that defeats the purpose of NLL.Rust solves a similar problem in closures with unique immutable references, but they're not quite the same.
Awesome question, you're getting at the good stuff.
Short answer: Valen would have something similar to Fn and FnMut (but phrased in terms of effects rather than Fn vs FnMut). In other words, we would be able to express "a closure that does not modify anything it captures", or rather, "a closure that has no mut effects".
That closure, because it doesn't modify anything it captures, would be safe to share among multiple threads in a structured-concurrency-like / std::thread::scope-ish way.
The key here is that one _can_ express immutable references in Valen; an immutable reference is a reference that the containing function doesn't express a `mut` effect for. And once we have immutable references, we get all of the nice concurrency benefits that Rust trailblazed.
I'd also like to make a way to do the above without a function call, perhaps using something like the `parallel` keyword I described in [0].
A no-access reference is an interesting idea. That could be a more powerful way to express may_dangle. In Valen, I hope to have an "opaque" group to express something like that.
I don't know whether it's a good idea, but in Valen I'm trying to decouple access capabilities away from the reference types as much as possible. We'll see if that bet pays off.
[0] https://verdagon.dev/blog/seamless-fearless-structured-concu...