Instantly share code, notes, and snippets.

Embed
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.

@phaazon

This comment has been minimized.

Show comment
Hide comment
@phaazon

phaazon Jul 4, 2018

You’re confusing (∃ x: P(x)) → Q with ∃ x: P(x) → Q. impl Trait in argument position is akin to the latter. The former doesn’t exist in Rust at all. However, it exists in Haskell:

-- these two exist in Rust with generics or impl Trait in arg position and those are universals.
foo :: a -> String
foo :: forall a. a -> String

-- this is an existential in argument position, which Rust doesn’t have (and could have if impl Trait was correctly used):
bar :: (forall a. String -> (a, Int)) -> String -> Int

phaazon commented Jul 4, 2018

You’re confusing (∃ x: P(x)) → Q with ∃ x: P(x) → Q. impl Trait in argument position is akin to the latter. The former doesn’t exist in Rust at all. However, it exists in Haskell:

-- these two exist in Rust with generics or impl Trait in arg position and those are universals.
foo :: a -> String
foo :: forall a. a -> String

-- this is an existential in argument position, which Rust doesn’t have (and could have if impl Trait was correctly used):
bar :: (forall a. String -> (a, Int)) -> String -> Int
@earthengine

This comment has been minimized.

Show comment
Hide comment
@earthengine

earthengine Jul 11, 2018

The same thing can be viewed in different angles.

If looking from the position of the function, "universal" means the caller will choose what the type is, and "existential" is the callee to choose. With this, impl Trait sometimes is universal (in parameter position), sometimes is existential (in return position).

On the other hand, your post was from the position of the type, so you can conclude that it is always existential (the provider choose).

Both are correct in theory, an should not be conflicting.

However, for new language users there is a much easier explaination to them: impl Trait is simply anonymous type: there is a value that your code will not know what the type is (only the compiler can figure out), and all you can conclude is it implements a specific set of traits.

This is also consistant on all cases, and highlights the difference between impl Trait in parameter and the previous generic grammar: you simply don't have to name a type parameter, just specify its constraint.

earthengine commented Jul 11, 2018

The same thing can be viewed in different angles.

If looking from the position of the function, "universal" means the caller will choose what the type is, and "existential" is the callee to choose. With this, impl Trait sometimes is universal (in parameter position), sometimes is existential (in return position).

On the other hand, your post was from the position of the type, so you can conclude that it is always existential (the provider choose).

Both are correct in theory, an should not be conflicting.

However, for new language users there is a much easier explaination to them: impl Trait is simply anonymous type: there is a value that your code will not know what the type is (only the compiler can figure out), and all you can conclude is it implements a specific set of traits.

This is also consistant on all cases, and highlights the difference between impl Trait in parameter and the previous generic grammar: you simply don't have to name a type parameter, just specify its constraint.

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