I’d also like to make a more higher-level comment:
You seem to be worried that we have a combinatorial explosion of references. I fully sympathize with that! This combinatorial explosion of references is paralleled by a combinatorial explosion of “typestates” and invariants, and that worries me very much. It’s why I was opposed to shared pinned references. So I very much agree there is a problem here with Pin that I’d like to see solved some day. I just think that sizedness is not the solution.
On the formal model side, I actually have some thoughts for how to reduce the number of invariants. At some level it’s just a mathematical trick, but I think it could actually be nice. Instead of having four of them (T.own, T.shr, T.pin and T.shrpin), we could have just two of them, with types like
enum PinState { Unpinned, Pinned }
// This trait defines which invariants make up a Rust type.
// It's an unsafe trait because the invariants actually have to satisfy some axioms, as discussed in my blog posts.
unsafe trait Type {
fn own(self, pin: PinState, ptr: Pointer);
fn shr(self, pin: PinState, ptr: Pointer, lft: Lifetime);
}
(I am using you as a guinea pig for an even more Rust-y syntax for all this math. Let’s see how that goes
)
So, it wouldn’t actually be four invariants, it’d just be two parameterized invariants. That will probably be much more convenient to work with.
Now, I said this is just a mathematical trick because the amount of information is still exactly the same – instead of two functions, I have one function taking a two-element type. That’s the same thing. But it may be informative, and it may even feed back into language design. This approach invites us to think of pin not as a reference type, but as a reference modifier. So, there wouldn’t be &pin, there would be &[list of modifiers]. We could have &pin, &mut pin and &move pin (assuming &move ever becomes a thing). Maybe even mut and move could become a modifier, so a reference is determined by
-
mut,moveor shared (with no keyword) -
pinor not
There could be some kind of modifier polymorphism as well—something we anyway want to shared and mutable references, to avoid writing every function on slices twice.
Given that the invariants of the owned and pinned are meaningfully different, I don’t think we want to conflate concepts here. But It would be nice indeed to to be able to talk about references in a more general way, without stating the exact typestate the referent is in.
. This could at least be mitigated by adding a warning recommending these instances migrate to having explicit