This (currently unpublished) draft paper shows how to use phantom types fluet:jfp:2006 together with Rust’s lifetime annotations to capture the idea that a data structure should be seen as a single data structure even though it is made up of multiple objects. This gives a zero-overhead, safe mechanism to create data structures with sharing and cycles like a doubly linked list.
The use of lifetimes in this way was originally developed in beingessner:msc:2015 but is still somewhat unusual so they prove that the GhostCell implementation is safe using RustBelt.
The idea is based on the idea of branded types
and Haskell’s runST function
and Beingessner’s BrandedVec beingessner:msc:2015.
The key idea of
GhostCellis to separate the permission to access a data structure from the data itself. As such,GhostCellintroduces two types:GhostToken<'id>andGhostCell<'id, T>.
GhostCell<'id, T>describes data of type T that is marked with the brand ‘id. When this “cell” type is shared, the data it contains can only be accessed by whoever holds the corresponding GhostToken<’id>.
GhostToken<'id>represents the permission to access all data in GhostCells marked with the brand ‘id.
The key operation that makes it all work is GhostToken::new(k)
that takes a continuation k of type FnOnce(GhostToken<'new_id>) -> R,
and runs k on a fresh, unique GhostToken (made unique by the 'new_id brand).
This token gives permission to borrow or borrow_mut any GhostCells
with the same brand — typically all the other objects in the data structure.
Using a continuation is a key part of restricting the 'new_id brand
to the execution of the continuation.