?Size types and my own variant of GhostCell

[jonleivent]

Recently, I developed very similar mechanism to GhostCell:

https://github.com/jonleivent/tin_ref/blob/main/src/lib.rs

The major difference is that instead of a cell type wrapping values, TinRef is a reference type replacing normal & references.

One advantage I can see is that TinRef supports ?Sized targets, while GhostCell requires Sized values. Do you have any feel for how valuable the ability to support ?Sized types might be in typical use cases? I do not yet have enough Rust experience to do so.

[wackbyte]

GhostCell supports ?Sized values. They can be constructed with GhostCell::from_mut.

let mut slice: &mut [i32] = &mut [1, 2, 3];
let cell: &mut GhostCell<[i32]> = GhostCell::from_mut(slice);

let mut debug: &mut dyn Debug = &mut 7;
let cell: &mut GhostCell<dyn Debug> = GhostCell::from_mut(debug);

[jonleivent]

GhostCell supports ?Sized values. They can be constructed with GhostCell::from_mut.

let mut slice: &mut [i32] = &mut [1, 2, 3];
let cell: &mut GhostCell<[i32]> = GhostCell::from_mut(slice);

let mut debug: &mut dyn Debug = &mut 7;
let cell: &mut GhostCell<dyn Debug> = GhostCell::from_mut(debug);

Thanks for that correction. I should have noticed the ?Sized in the GhostCell definition.

[matthieu-m]

There is actually a disadvantage in using TinRef: GhostCell can embed both owned types and references, while TinRef is limited to references for now.

[jonleivent]

I think there is an isomorphism: &'r GhostCell<'brand, T> <-> TinRef<'brand, 'r, T>. This requires a different structuring of the user's types - using TinRef instead of normal shared '&' references to GhostCell, but I think otherwise they support all the same target types and all the same functionality.

Unless you mean something like vectors: [GhostCell<'brand,T>] - yes I guess that is a benefit. I was considering a way to construct a vector of TinRefs when given a mutable reference to a vector of targets, which would close that gap a bit, but probably not all the way.

BTW: can there be an impl Index for GhostCell<'brand, [T]> and like vector types that doesn't require the GhostToken and returns a & GhostCell<'brand, T>? Maybe similarly an impl Deref? I was considering similar additions for TinRefs.

BTW part 2: syntactic sugar macros - I've yet to learn how to define Rust macros. I was wondering if the excessive .get(tok) and .get_mut(tok) calls (ghost_cell would have .borrow(&tok) and .borrow_mut(&mut tok)) could be removed with some macro that would allow comprehension-style syntax:

  let x.borrow_mut(&mut tok).y = a.borrow(&tok).b.borrow(&tok).c;
  ...

could be shortened to:

ghost!{tok |
  let x+.y = a-.b-.c;
  ...
}

BTW part 3 - I'm not going to publish tin_ref at all. I see no point, considering the above isomorphism. There are very minor differences that are probably due to my limited knowledge of potential Rust use cases. For instance, ghost_cell's closure function uses a GhostToken<'brand> value as its parameter, while tin_ref uses a &mut TinTok<'i>. I though making the closure arg a &mut would save usages from having to repeatedly mention & or &mut, but maybe there is an advantage to using the value directly? Another difference is that tin_ref attempts to unify the "brand" (it's 'i lifetime) immediately at the point of declaration of a TinRef, while ghost_cell lets the corresponding 'brand float at the point of creation of a GhostCell. I think I can see advantages and disadvantages to both, but again, I'm not sure. I also equipped TinTok with a public subfield Tin which can be copied and used to pass around the "brand" lifetime easily without needing a reference to the TinTok (which might interfere with its operation).

BTW part 4: I am a former Coq'er. I don't know how much that experience went into TinRef, probably some. I don't recall ever reading the GhostCell paper. I was using Coq in an different manner: generating verified programs from specifications instead of verifying existing programs. I am somewhat familiar with iris in Coq.

[matthieu-m]

BTW: can there be an impl Index for GhostCell<'brand, [T]> and like vector types that doesn't require the GhostToken and returns a & GhostCell<'brand, T>? Maybe similarly an impl Deref? I was considering similar additions for TinRefs.

I would expect this is sound, seeing as it's possible to go from GhostCell<'_, [T]> to &[GhostCell<'_, T>] and vice-versa.

Of course, given the above conversion, it'd just be syntactic sugar, since you can already just go to a slice of cells and then use all the slice functions.

BTW part 2: syntactic sugar macros

Possibly... but you'd need a syntax which is unambiguous enough not to intersect on Rust syntax. And then you'd need to create a macro for it and it may not be simple: declarative macros are pretty locked down, and re-parsing Rust yourself seems complicated.