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
,move
or shared (with no keyword) -
pin
or 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.