Static path-dependent types and deferred borrows

language design
27

It is already possible today to build APIs that statically enforce that each OperationHandle is only used with the Device it was created from.

The key language feature is parametricity: the only things a generic function can ever know about its generic parameters come from their bounds. Rust doesn't quite have this for types (and it's missing another feature we would need there anyway), but it does have it for lifetimes.

Our goal, then, is to treat a function's lifetime parameter 'id as a unique token to tie OperationHandle<'id>s to their Device<'id>s. This does place one big restriction on our API: all OperationHandles for a particular Device must stay inside that function and its callees. Further, we need to pass the function around while keeping it generic over 'id. (This is the missing feature we would need to use a type as the token.)

Combined, these two requirements gives us an API like this:

fn with_device<F>(f: F) where
    F: for<'id> FnOnce(Device<'id>) // `f` remains generic over `'id`
{ .. }

impl<'id> Device<'id> {
    fn create_operation(&self) -> OperationHandle<'id> { .. }
    fn use_operation(&self, _: OperationHandle<'id>) { .. }
}

There is one more tricky aspect to this: Device and OperationHandle might inadvertently provide f with additional information about 'id. Generic types in Rust have subtyping relationships, based on their variance relative to their parameters. To forbid any relationships between distinct 'id parameters, Device and OperationHandle need to be invariant:

struct Device<'id> {
    ..
    // see the nomicon link for what on earth this means:
    _make_invariant: PhantomData<fn(&'id ()) -> &'id ()>,
}

Putting this together looks something like this: Rust Playground

This has been "known" for quite a while, but the restriction to a callback and unfortunate error messages limit its use somewhat. Some further reading:

  • Gankra's thesis You Can't Spell Trust Without Rust describes it as "generativity" in section 6.3, and uses it to tie pre-bounds-checked indices to their associated array.
  • The gc-arena library uses it to determine GC safepoints- outside of the callback, all 'id pointers into the GC heap are known to be dead, leaving only known roots.
  • The recent GhostCell paper includes a nice general-purpose factoring of the pattern, to enable safe pointer-graph-based data structures.
2 Likes