Skip to content

Use generativity pattern in types::Context #304

@apoelstra

Description

@apoelstra

Currently we use the types::Context object to hold type bounds. We provide an accessor to BoundRefs which index these bounds, but which internally hold a value uniquely tied to the Context it came from. We check consistency at runtime: if you try to use a boundref with a context it didn't come from, you'll get a types::InferenceContextMismatch error.

However, in Rust it is possible to do this check at compile time, by abusing invariant lifetimes to local variables to create types with unique lifetimes that cannot be unified.

Basically, instead of users calling

let ctx = Context::new();
...

they would write

let _unused = ();
// SAFETY: we are calling `unsafe fn new` with a unique lifetime, and `Context` has an invariant-lifetime PhantomData preventing this unique lifetime from being unified with any other lifetime
let ctx = unsafe { Context::new(&_unused) }

(where ofc we would wrap this up in a macro so the user doesn't need to write the dummy variable or the unsafe marker themselves).

A consequence of this construction is that Context (and anything else containing a Context) will be unable to escape the scope in which it is defined. I think this is fine for this type; the "standard usage" is for users to create a context, build a program, then throw away the context, all within some function.

See https://arhan.sh/blog/the-generativity-pattern-in-rust/ for a long blog post which expands this issue into a self-contained blog post which can be understood without having memorized tons of Rust arcana.

The blog post argues that the "Context cannot escape its scope" limitation is inherent to Rust because otherwise you could create a runtime-sized Vec containing a runtime-determined number of unique types, which (almost by definition) requires dependent types. I'm not totally convinced by this argument. It seems like you should be able to create an arbitrary number of generative types and the compiler shouldn't need to care "how many" of them there are. If they don't unify they can't be used together without giving them all distinct names.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions