impl-trait-always-existential.md

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.

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

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.

There is not a single good example on internet about how to use impl Trait, all they do is blabber and blabber and blabber like in this thread

@pthariensflame
@phaazon
@earthengine

You are correct, more on this later, however, your presented logic is wrong, example:

P is a predicate which is true for P(1) and false otherwise ( forall x!=1: P(x)==false).
Assume further that P(x)==true implies Q

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

and we say that P is fixed:

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

Now, the left hand side evaluates to true and the right hand side to Q, we have:

∀ Q true ⇔ Q which isn't true for Q in {true,false}

So the rule above is false.

Nevertheless the statement is correct.

Why are impl Trait existentials?

fun(x:impl Trait)->Int can be lowered to fun(x:(exists T. T:Trait))->Int, then T is existentially quantified.

But why we sometimes think it is universal?

Because we can apply fun to any type T implementing Trait, but not because of all quantified polymorphism, but rather of subtyping.

Existentials always imply subtyping and therefore, Haskell has subtyping, too even if they don't wan't to hear that!!!

What is then the difference between impl Trait versus dyn Trait,

From the point of abstraction: There isn't

From the point of implementation:

An impl Trait is an existentials only at design time, where no type parameter binding occurs.
During compilation time, all type parameters get bound,e.g. the function fun<X,Y,Z> get applied to fun<Int,Float,String> and impl Trait is monomorphized at compile time.

A dyn Trait is an existential at design time and compile time and gets monomorphized at runtime.

Note 1:
You might wonder why the distinction must be made explicit by the user and cannot be inferred by the compiler, the closest reason I can think of is that impl Trait functions are saved as generic functions in libraries (crates) and are still monomorphizeable in application code while this doesn't hold for dyn Trait functions.

Note 2:
You can theoretically (but no yet) return multiple types for impl trait in the body, but they have to be statically resolveable, e.g.

fun<T>(a:T)->impl Trait 
{
    static if(T==Int)
    {
         return 2.0:Float
    }
    static else
    {
         return "Hello World":String
    }
}