short take on this: to be honest, using the word existential for
type_alias_impl_trait or for
-> impl Trait alone is not really required, since it boils down to a convoluted way to express a much simpler thing.
Let's take a simpler example: say you want me to write down a number between 1 and 10 on a piece of paper. So I do that, and write "some such number". That's the clearer way to put it. But another way to put it, which, granted, does sound a bit weird out of context (but which is technically correct), is that there exists a number between 1 and 10 such that that number equals the one I wrote down.
That is, some unknown but fixed thing is equivalent to "there exists an element [upholding the mentioned properties] that is that thing". So besides playing with words / terminology, nothing complicated going on.
That being said, you may notice that word of fixed I have just introduced. Indeed, in mathematics (in the broader sense, that is, one that involves any form of logical reasoning, it doesn't have to be numerical) we like to express how a given state depends on some parameters / inputs, and then study the changes that occur (or the changes that do not occur / the invariants) when that parameter changes / moves.
Back to Rust, the parameter that may definitely move are type parameters, here: despite being constrained to upholding some property (the trait bound applied to the type), depending on the usage, there may be multiple possible types used there, or not.
And this is where the
impl Trait notation, in and of itself, comes into play. As of today's Rust, that notation can be used in two (three on nightly) places:
in a function's argument / parameter (type) position;
fn foo(f: impl Fn(), …) -> …
in a function's return (type) position;
-> impl Fn()
nightly, within a
type alias definition.
type Bar = impl Fn();
In all these cases, we know the type described by the
impl … syntax is:
… that implements / meets the given (trait, lifetime) bounds.
But from that
1. line, "a type", stems a legitimate question:
Does "a type" refer to some type, or to any type ?
In other words, is there freeway to move / change that type (generic type parameter), or is it a fixed (but still potentially unknown) type?
- In mathematical terms, this question refers to the quantification of this parameter.
And it turns out that
impl Trait can mean either one (depending on where it is used)! Thus, one has to be very explicit about the quantification of the
impl Trait type.
in a function's argument / parameter (type) position,
impl Trait is sugar for a generic type parameter: "(for) any type that
Fn(), we can take a parameter called
f of that type"
So in argument position,
impl Trait stands for a generic type parameter, i.e., any arbitrary type that the caller of the function may choose, thus, the function's body must be able to handle any type implementing that
Trait: it must thus be able to handle all the types implementing that
Trait: it is thus a universal quantification.
whereas in a function's return (type) position and a
type alias definition,
impl Trait stands for a fixed (but potentially unknown) type:
So, in return position (or in
type alias definition), it stands for one single fixed type, and as I mentioned at the beginning of this post, this can be mathematically expressed with the property that there must exist an actual concrete type that "is" / matches the type used there.
While that phrasing looks weird on its own, existential and universal are "duals" / "opposites" of each other; and the universal terminology fits very well that of a generic parameter. Thus, existential is used to mark an opposition, to explicit a semantic distinction with the universal