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 idea is based on the idea of branded types
The key idea of
GhostCellis to separate the permission to access a data structure from the data itself. As such,
GhostCellintroduces two types:
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
that takes a continuation
k of type
FnOnce(GhostToken<'new_id>) -> R,
k on a fresh, unique
GhostToken (made unique by the
This token gives permission to
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
to the execution of the continuation.