Static path-dependent types and deferred borrows

[hgomersall]

@atagunov

It should be possible to design a different language or extend Rust with more features so that the compiler would be able to do better. Ocaml can apply functors at module level level generatively.

Is there any serious proposal to do this?

[atagunov]

@hgomersall

Is there any serious proposal to do this?

Disclaimer: I'm not (hopefully yet) strong enough to fully appreciate:

• 1ML - core and modules united
• crude proof of concept

P.S. my answer is a sort of a joke, but I'm answering the question as posed

P.P.S. it also may also be worth mentioning Pikelet - this time it's done by Rusticeans, small seeds of possible implementation are done in Rust and the set of ideas (Pikelet is just a set of ideas at the moment, while Rossberg's papers are indeed as far as I understand a "serious proposal") is inspired by both Rust and 1ML as well as some other languages

[quinedot]

@hgomersall

The solution I proposed works around this by consuming self, which immediately prevents the loop case you highlight. The broader question then is there a way to make this more ergonomic that doesn't break the compiler model?

Seems like a classic run-time solution to the singleton pattern. I don't know of any better solutions than what already looks to exist (libraries with macros to help you out). More discussion from URLO.

You could make this run-time approach more generic by having a HashSet of TypeIds or similar.

What you're highlighting is the broader conclusion I'd reached on this issue, which is that you can't express a mutating type in any generally useful way.

I played with using the borrow checker to prevent the loop case at compile time, which works, but it also prevents going up the call stack as well. If you just need to create your singleton in main() or something and pass it everywhere, it may be sufficient, but that might be too limiting.

That's the closest I got to manipulating types in a way useful to solve this problem statically and ergonomically. Ultimately trying to solve the singleton pattern for a device using handles just means you solve the singleton pattern for the handle. It may be doable with enough compiler gymnastics, but I don't know that it's worth it. (If it was, the embedded community would probably already be using it.)

[hgomersall]

@quinedot

@hgomersall

The solution I proposed works around this by consuming self, which immediately prevents the loop case you highlight. The broader question then is there a way to make this more ergonomic that doesn't break the compiler model?

Seems like a classic run-time solution to the singleton pattern. I don't know of any better solutions than what already looks to exist (libraries with macros to help you out).

I guess it's more of a singletonton (or something - a single call to a singleton). My question about ergonomics was whether the type chain spawned from that could be made better.

[simmet]

does that seems like nim where macros rewrite the abstract syntax tree

[H2CO3]

Not sure what you mean by that — Rust macros also rewrite the AST. More precisely, they can rewrite arbitrary well-formed code, including valid Rust code, but the definition of a token tree is more relaxed than that.

[rpjohnst]

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.

[H2CO3]

That's a clever solution, but what do you mean by this?

@rpjohnst

[…] 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 […].