Create a gist now

Instantly share code, notes, and snippets.

What would you like to do?

impl Trait is Always Existential

Recently, Rust 1.26 was released, and with it came stable access to a heavily desired feature: impl Trait. For those unfamiliar, impl Trait lets you write something like this:

fn foo<'a, A, B>(x: &'a mut A) -> impl Bar<'a, B> { ... }

and have it be translated to something like this:

// imaginary syntax; not in the language yet
abstract type R<'a, A, B>: Bar<'a, B>
fn foo<'a, A, B, R>(x: &'a mut A) -> R<'a, A, B> { ... }

This is the usual use case cited, but you can also use it in parameters, like so:

fn baz<'a, A>(y: impl Bar<'a, A>) -> &'a A { ... }

which will be translated into something like this:

fn baz<'a, A, P: Bar<'a, A>>(y: P) -> &'a A { ... }

This second use case is often referred to as “universal impl Trait,” since it appears to induce universal quantification (generic type parameters) rather than existential quantification (a type alias held abstract).

I'm here to say that this impression is fundamentally incorrect: impl Trait is always existential!

Wait, What?

You heard me!

In order to understand why this is the case, we have to take a closer look at what “universal” and “existential” really mean here. A “universally quantified type” is one that takes other things (usually types) as parameters; for example, the type for<X> (fn() -> Vec<X>) is a vector of any type, and the user of the type gets to choose what X is, while the producer has to be able deal with whatever is requested of it. (This is nearly, but not quite, valid Rust syntax.) Similarly, an “existentially quantified type” is one that carries other things (usually types) as hidden outputs of some kind; for example some<X> (fn() -> Vec<X>) is a vector of some particular type, and the producer of the type gets to choose what X is, while the user of the type has to be able to deal with whatever is handed to it.

There is a close relationship between the two forms of quantification, and there is a lot of literature on the subject, but we just need one particular mathematical law:

∀ P, Q: (∀ x: P(x) → Q) ⇔ ((∃ x: P(x)) → Q)

When rewritten in pseudo-Rust syntax, this says that, for any types P and Q (where P takes a single type parameter and Q takes none), the following two types are exactly equivalent:

for<X> fn(P<X>) -> Q
fn(some<X> P<X>) -> Q

In prose, this says that taking a type parameter that is only used in the arguments is exactly the same as scoping that type parameter over the arguments alone as an existential.

So…what does this have to do with impl Trait?

This means that impl Trait is actually always existential! The most naïve possible tranlation—taking impl Bar<'a, A> and turning it into some<X: Bar<'a, A>> X—will always work. Of course, the Rust compiler may not choose to physically implement impl Trait in this particular way, but it shows that the whole purported inconsistency of the “universal” versus “existential” use cases is nonexistent. In fact, the “traditional” translations given above are arguably not being consistent about how the translation works, since in one case a hidden type name is added by including it in the function signature (as a generic parameter) and in the other case a hidden type name is added by including it in the whole module (as an abstract type).

If the Rust compiler does choose—as it appears to—to implement the “traditional” translations internally, it only works because the above mathematical law holds.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment