This might be related.
By the way, a very practical TL,DR / "application" of universal vs. existential, for functions, is that an existential type is "calleechosen", whereas a universal type is callerchosen.
This is what makes:
pub fn foo (_: impl Fn())
{}
and
pub fn bar (_: impl_Fn)
{}
// where
pub type impl_Fn = impl Fn();
// defined by:
pub fn make_impl_Fn () > impl_Fn {  () }
behave differently.
In the case of foo
, this is, as said, sugar for a generic type parameter that the caller is free to choose to their liking,
let caller_s_closure =  ();
foo(caller_s_closure);
// by type inference, the above is actually:
foo::<typeof(caller_s_closure)>(caller_s_closure);
let another_one = { let x = 42; move  drop(x) };
foo/*::<typeof(another_one)>*/(another_one);
whereas in the case of bar
, this is just sugar for a fixed and yet opaque type, about which we know only two things:

it
impl
ementsFn()
, 
the (defining) function
make_impl_Fn()
yields instances of that type.
// Note: each closure has its own unique type,
// so `typeof(make_impl_Fn()) β typeof(caller_s_closure)`
let caller_s_closure =  ();
bar(caller_s_closure); // Error, expected `impl_Fn` (= `typeof(make_impl_Fn())`)
// got `typeof(caller_s_closure)` instead.
bar(make_impl_Fn()); // OK
foo(make_impl_Fn()); // OK, we know this opaque type implements `Fn()`.

Aside:
Given,
fn makes_impl_Fn () > impl_Fn { let ret =  (); // This concrete closure type is `Copy`. drop(ret); drop(ret); return ret; }
then, outside the privacy boundary of the
type impl_Fn
definition, the following fails:fn is_Copy (_: impl Copy) {} is_Copy(makes_impl_Fn()); // Error, the only thing we _officially_ // know about `impl_Fn` is that it does // `impl Fn`. Any other `impl` of the actual // implementation of `make_impl_Fn` is // an implementation detail / coincidence // that cannot be relied upon.
Which shows one of the main usages of
type_alias_impl_trait
: it prevents^{1} leaking properties that stem from implementation details that could change, and which thus prevent making such changes within semvercompatible changes.^{1} I don't know exactly about
type_alias_impl_trait
, but for the "classic"> impl Trait
in return position (thus, existential), theauto_traits
such asSend
andSync
do leakβ¦ EDIT: it turns out that formin_type_alias_impl_trait
autotraits cause a weird type error
Fwiw, I was thinking more about some of the explanations here, and I was getting stuck on something with the theory side... if an existential type is one which denotes its existence, aren't all types existential?
The conclusion I came to (without having a proper background in this stuff, so, sorta guessing) is it's rather a relative term, not absolute... i.e., existential types are only "existential" in the sense that they are not, "universal" (as @Yandros pointed out) combined with the fact that they are not "concrete". Outside of that context there's not really such a thing as an existential type...
If that's correct then I think it also clarifies where I'll need it  when I don't have a concrete type, and it can only be defined a set number of times, like 1 for a function return. It's a bit easier for me to grok for now in that sense of defining it by its constraints rather than a direct definition...
Are associated trait types, compared to generics, the same sort of "dual/opposites" or is that a totally different relationship?
Associated types in traits are also interesting. A single type can implement both AsRef<i32>
and AsRef<u32>
, but it can't implement both Iterator<Item = i32>
and Iterator<Item = u32>
, because the latter uses associated types.
So it's a many vs one distinction.
Yes, I actually think that is a correct way to put it: existential is indeed used to signify lack of universality, mainly, so technically even concrete types could be seen as "existential". But, indeed, the denomination makes actual sense / most sense once the type is opaque: if you don't know the exact type involved, you technically can't use it much; so usually such a fixed / existential but opaque type is not totally opaque: it carries trait bounds expressing parts of its usability which remain visible through the opaque alias.
And since trait bounds are usually involved with polymorphism (be it at compiletime with typelevel generics and static dispatch, or be it at runtime with virtualmethodbased dyn
type erasure (cc @EdmundsEcho)), specifying that this usage of impl Trait
(in return position or type alias) is not polymorphic / universal becomes especially important
Hmm, there is some metalevel common pattern here, possibly.
I guess an interesting way to illustrate that is to compare it to the Fnβ¦
traits (the trait is generic in the parameters, so that a single type can admit parameters of different types β could have generic parameters^{1}, whereas for a given set of parameter types the return type is an associated type: it is unique):
impl Trait  FnOnce  

arguments  universal  <Args> 
return  existential  (associated)type Output;

^{1} But it should be noted that the similarity does end in that a trait's generic parameter allows for multiple instantiations (specific choices of the generic parameter), but a specific type does not necessarily implement the trait with all the possible instantiations (=> not necessarily universal), whereas impl Trait
in argument position does yield a function which is fully generic over that parameter.
The trick might boil down to
 First ask, what can I say about the quantity of x?
 Test the following first: Can I describe it as "always" or "all"? => universal, if not...
 Can I at least say it exists even if I don't know how often? => existential (all I can say is that it exists), if not...
 There isn't anything we can say. This does not mean anything per se. We just can't make any conclusions about how much/often etc. the subject exists.
So for example:
A. Every Rust programmer loves their borrow checker
B. Most Rust programmer at least appreciate the borrow checker
If A is true, how would you describe the quantity of Rust programmers? universal
If B is true, how would you describe the quantity of Rust programmers? existential
Another example taken directly from "Computational Semantics with FP" by Jan van Eijk and Christina Unger:
Every prince saw a lady
What can you conclude about the quantity of
 Prince? universal
 Lady? existential
The following statement captures the two possible interpretations depending on the meaning of "a lady".
If it is just "some" lady every prince saw:
βx (Prince x > βy(Lady y β Saw x y))
Alternatively, if it is the same lady every prince saw:
βy (Lady y β βx (Prince x > Saw x y))
Finally, in a situation where you are thinking of using a function
fn uses_trait_foo<T: TraitFoo>(input: T) {...}
...what do you know about T? As a potential user of the function, is there a way to describe T in toto, i.e., universally quantify T?
Yes there is. βx(Tx β TraitFoo β fn(T))
Contrast this with another function you might be thinking of using:
fn produces_T(input: u32) > T {...}
There is no way to universally quantify T. However, if someone were able to implement this function, then I would have to conclude "T must exist"... existential.
βx(Tx β fn produces_T)
There is a twist to this story: is it possible to implement a function that returns T "for all T"? i.e., could such a function exist?
... Thus, a function that one might actually encounter
fn produces_T(input: u32) > impl FooTrait {...} // or
fn produces_T(input: u32) > Box<dyn FooTrait> {...}
FYI: Link to a post describing how the functions are the same but different
The logic to quantify T is the same as the previous example, I have no idea what type to expect, but again, if the function exists, whatever T is, it has to exist. Unlike the previous example, this is a function that can actually exist*.
βx(Tx β TraitFoo β fn produces_T)
The contrast between universal input and existential output links to a hook that seems to be a popular way to describe who has control of the type in generic functions; it goes something like:
Universal input => caller has control over the type
Existential output => callee has control over the type
* Note
Whether the scenario is believable is a separate point and beside the point. For instance, the perhaps unbelievable statement made about the Rust borrow checker (A) did not prevent me from making concrete irrefutable observations about it. Just because in reality "it's not so", does not stop me from quantifying it in a mental model where I say: "if it were so...".
just for fun  if it's a unique lady every prince saw, then according to the rules lady is also universal?
Note that the second one is stronger than the first one. In Rust terms:
trait IsPrince {} // marker trait that describes the set of princes.
trait IsLady {} // ditto, but for ladies
/// If A sees B, we then have `A : Saw<B>` β `impl Saw<B> for A {}`
trait Saw<Seen> {}

it is just "some" lady every prince saw / princes may have seen different ladies:
type LadySeenByPrince<P : IsPrince> = impl IsLady; // ^^^^^^^^^^^^ ^^^^^^^^^^^ // 1. For all/ each `P : IsPrince`β¦  // 2. β¦there exists a `Lady` each saw. impl<P : IsPrince> Saw<LadySeenByPrince<P>> for P {}

it is the same lady every prince saw:
type TheOneLady = impl IsLady; impl<P : IsPrince> Saw<TheOneLady> for P {}
Universality is a quantification over a set; but the set can be of one! Considering:
// Classic `Into` / `From` inversion:
trait SeenBy<Seer> {}
impl<Seen, Seer : Saw<Seen>> SeenBy<Seer> for Seen {}
then you could envision the following universal quantification:
<Lady : IsLady + for<P : IsPrince> SeenBy<P>>
but if we consider my second Rust snippet where there was one Lady
which had been seen by all princes, the set described by IsLady + for<P : IsPrince> SeenBy<P>>
was seemingly a set of one: only TheOneLady
fit these bounds (but given how my Saw
trait was generic over Seen
rather than having it as an associated type, at any point we could also have a second lady all the princes have also seen (enum AnotherLady {} impl IsLady for AnotherLady {} impl<P : IsPrince> Saw<AnotherLady> for P {}
)
The set of unique ladies, elements in the set because they were seen by a prince, remains a subset of all ladies. So, because I know about "all ladies", I have to say the ladies seen by a prince remains "existential". Does that make sense?
Actually, I think the above is a bit of trap. The statement says nothing about "all ladies", and thus is existential because I know at least one lady has to exist.
However, to your point, I don't see a reason why you could not specify the set of ladies in universal terms:
βx (Lady x β SeenByPrince β something you care about)
The thing we care about is the contrast between the quantity of ladies vs princes. So, the choice to start with a set of all women just like we started with the set of all princes, is useful to explain the differences between universal and existential.
The impl Trait
in return position is a specific type. However, the function/crate maintainer can change it at their leisure. From keyword trait documentation.
The use of the
impl
keyword in this position allows the function writer to hide the concrete type as an implementation detail which can change without breaking user's code.
Indeed this is more about hiding implementation details and making the caller avoid making assumptions than about existence. We can for example compare it with existential types in the Coq language for example. A type can be said to be inhabited
Inductive inhabited (A:Type) : Prop := inhabits : A > inhabited A.
There, inhabited Lady
means there is some element of type Lady
. And its constructor is just a function whose argument is a Lady
. If something is able to call inhabits
with any argument then it is effectively giving a existence proof.
There is also an existential about whether there is an element satisfying a given Proposition.
Inductive ex (A:Type) (P:A > Prop) : Prop :=
ex_intro : forall x:A, P x > ex (A:=A) P.
We could have a type Human
and a proposition IsLady:Human>Prop
. Then ex _ IsLady
would sate there is some lady.
Furthermore, in Coq the type A>B
is actually a shorthand for forall x:A, B
. Thus the type forall x:A, B
or A>B
is the type of a typical function with concrete types. And forall x:A, inhabited B
is a function that converts an element of type A into a guarantee of existence of elements of type B. But neither reflects the meaning of the impl Trait
, since in these the return type is perfectly known to all parties.
The mistake I made, I think, is assuming that "every prince"/"universal" means not just "potentially infinite" but "actually infinite", and therefore the number of ladies are infinite, and they are equal in number.
Also  what you're saying makes sense on a fundamental level... like, why wouldn't it be possible for there to be ladies that aren't seen by a prince.
Note that infinities behave weirdly, so you canβt necessarily draw that conclusion. Even if there really are an infinite number of princes.
Being precise often requires imagining what is not being said. In Math, it's often the case that more of what is being described, is what is not included in the specification. e.g., not 1 is infinitely large (you have to imagine all non1 values, which could include cars if the rules don't specify otherwise).
I think inferring what you have is precisely useful and implied by "Every prince saw a lady". It's correct to say βx (Lady x β seenByPrince)
but is it useful given the story we are trying to tell?
When I was working through why using the universal quantifier to describe input T as βx (Tx β Trait)
, was in fact useful compared to βx(Tx β Trait)
, it took me awhile to find the constant reference required to highlight the contrast between input and output. In this case, the constant was "what I know about T from the fn signature". So, while I could choose to express βx(x β Trait)
to describe the input, it's not the same reference point used in the comparison with T as output. In the latter, the only thing I can say about T is βx(Tx β Trait)
. This points to a more useful contrast for describing the input: T β Trait
is universal; the fact that T β Trait
could also be seen as existential is missing the point and false given the reference point "what I know about T from the signature".
In the prince example, the constant reference point is stating what we know about "all" for prince and ladies.
tangent: I don't understand the math, but I did once read a book on Georg Cantor's life. iirc he went mad contemplating this stuff, despite his success...
at the risk of such madness ... do we have enough info here to say if the set of infinite ladies is not equal in number (or cardinality or whatever makes infinite sets equal...) to the set of infinite princes?
don't think I'm going to spend my time really digging in on this angle, just random layman's curiosity
Note that (confusingly) "existential" is not a property of a type. It's not like some types are existential types and others are regular types. Rather, there are existential quantifiers, and we use "existential types" as a shorthand for either a syntactic device that denotes an existential quantifier, or the types involved in such a syntax. Similarly for universal quantifiers.
Since Rust's syntax is not complete for predicate logic, which is to say, you can't just arbitrarily nest quantifiers, this can get confusing since there are only a few specific patterns available, and by and large the actual quantifier structure is only implicitly declared, which is not helpful when you are first learning this stuff. So let's use a more predicate logic looking syntax instead, for the moment.
Most types in Rust are universally quantified. So for example, given a function signature like this:
fn foo<A: TraitA, B: TraitB>(t: A) > B
The type of foo
is:
foo: β A B. A β TraitA β B β TraitB β A β B
As written, foo
takes 5 arguments: two types A
and B
, two proofs that A β TraitA
and B β TraitB
, and a value of type A
, and returns a value of type B
. By contrast, with impl Trait
we can express a type signature with existential quantifiers:
fn foo<A: TraitA>(t: A) > impl TraitB
means
foo: β A. A β TraitA β β B. B β TraitA β§ (A β B)
There is some interesting ordering of quantifiers going on here. The idea you mentioned earlier of universal types being callerchosen and existential types being calleechosen is completely correct and can help guide the reading here. First we give this function two arguments, a type A
and a proof that A β TraitA
. Let's say we instantiate it with u8
:
foo(u8, u8_impls_TraitA): β B. B β TraitA β§ (u8 β B)
(In Rust we would use pointy brackets for type arguments and we don't have to explicitly provide the proof u8_impls_TraitA
, it gets automatically derived.) Now what we have now is a sort of "existential pack", it's not yet a regular function we can use to get a value. To destructure this we need some kind of unpacking construct:
let (B, B_impls_TraitB, f: u8 β B) = foo(u8, u8_impls_TraitA)
When you unpack this existential pack, you get a type B
, a proof of B β TraitB
, and a function f: u8 β B
. Finally, we can call this function:
let (B, B_impls_TraitB, f: u8 β B) = foo(u8, u8_impls_TraitA);
f(42): B
We have to supply a value of type u8
, and get a value of type B
, since the type of f
says so.
Now of course Rust doesn't make you go through all these steps normally. Instead you would just write foo(42)
or perhaps foo::<u8>(42)
, and if you ask the compiler it will tell you this has type impl TraitB
, which is confusing because it's actually a particular type (that I'm calling B
here) that is bound somewhere and the syntax is ambiguous about exactly where.
To give some more examples of more exotic type signatures that full quantification would give you:
foo: β B. β A. A β B
This is a function that picks once and for all a type B
(what type it is is not communicated by this type signature) such that given any type A
maps values of type A
to B
. An example of such a function is:
(u8, A, x: A 0_u8)
That is, we take the type B
to be u8
, and the function ignores its argument x:A
and always returns 0u8
. (I'm using Rustish syntax for lambda calculus here, but you can't write polymorphic closures like this in today's Rust.)
Here's a function which doesn't determine the return type until after it receives its values:
foo: β A. A β β B. B
This function could return different types depending on whether you give it 0: u8
or 42: u8
, but you can't express something like this except in a dependent type theory. In a simple type theory like Rust, all the type quantifiers have to come before all the value types, as in:
foo: β A. β B. A β B
Here's a type which expresses a complicated communication between caller and callee:
foo: β A. β B. β C. (C β B) β§ ((A, B) β C)
You would call this function like so:
let (B, F: β C. (C β B) β§ ((u8, B) β C)) = foo(u8);
let (bar: Vec<B> β B, baz: (u8, B) β Vec<B>) = F(Vec<B>):
baz(0u8, bar(vec![])): Vec<B>
You can think of the quantifiers as saying who gets to pick what. Here, first the caller picks A = u8
, then the callee gets to see that u8
and picks something for B
, then the caller picks C = Vec<B>
(notice that C
it is allowed to depend on B
but A
isn't) and finally gets a pair of functions, one that turns a Vec<B>
into a B
and one that turns (u8, B)
into Vec<B>
.
All Rust type system features can be desugared into this kind of quantifier system. Let's desugar some examples from this thread:
fn f1<T: TraitFoo>(input: T) {...}
> f1: β T. T β TraitFoo β ()
fn f2(input: impl TraitFoo) {...}
> f2: (β T. T β TraitFoo) β ()
fn f3(input: u32) > impl FooTrait {...}
> f3: β T. T β FooTrait β§ (u32 β T)
These are all fairly easy from the rules seen thus far. In particular I want to call out the equivalence between f1
and f2
. The logical equivalence of (β x. (P x β Q)) β ((β x. P x) β Q)
is why it is natural for an existential pack in the function arguments (as in f2
) to be equivalent to a universally quantified type (as in f1
).
impl<Seen, Seer: Saw<Seen>> SeenBy<Seer> for Seen {}
> β Seen. β Seer. Seer β Saw(Seen) β Seen β SeenBy(Seer)
This one has to do with how proofs that a type implements a trait are represented as logical rules. Rust has a built in automated prover for theorems in this form based on prolog.
type CallbackFn = impl Fn();
struct Foo {
cb: CallbackFn
}
impl Foo {
pub fn new() > Self { Self { cb: Self::make_callback() } }
fn make_callback() > CallbackFn {  {} }
}
>
β CallbackFn.
CallbackFn β Fn() β§
Foo.cb: Foo > CallbackFn β§
Foo::new: () β Foo β§
Foo::make_callback: () β CallbackFn
This one is interesting. The existential pack here has to quantify over several function items. The things in the existential are the "defining uses" in rust lingo. All the things that need to reference CallbackFn
directly in the type are inside this existential.
fn foo<A, B>(arg: A) > B
where
A: Iterator,
B: FromIterator<A::Item>
>
β A B.
β (A_impl_Iterator: A β Iterator).
B β FromIterator(A_impl_Iterator.Item) β
A β B
In Rust, the Type β Trait
assertions can contain data. You can think of them as tuples containing types and functions; these are the associated types of the trait and the trait methods. Here I'm using the notation A_impl_Iterator.Item
to indicate the type Item
supplied by the proof A_impl_Iterator
of the assertion A β Iterator
, which is then used as an argument to another trait FromIterator(T)
; the proof B β FromIterator(A_impl_Iterator.Item)
might also contain more types, and so on. (Because of this, Rust is actually very near to supporting full quantification, using traits and associated types as a layer of indirection.)
fn filter_min<I>(iter: I, min: i32) > impl Iterator<Item=i32>
where I: IntoIterator<Item=i32>
>
filter_min:
β I. β (ii: I β IntoIterator). ii.Item = i32 β
β J. β (jj: J β IntoIterator). jj.Item = i32 β§
(I, i32) β J
This one is interesting because it includes type equality constraints. Rust will also do equational reasoning with type equalities like this.
The meaning of exists in all these examples is "at least one", but you have to be careful to distinguish between the type given to a function and the implementation of that function. For a simpler example:
fn foo() > u8 { 0 }
fn bar() > u8 { 1 }
Here foo
and bar
have different implementations, but they have the same type, namely () β u8
. That means that, at least from the perspective of the type system, these two functions are indistinguishable  either one can be used in place of the other. Compare that to this situation:
fn foo() > impl Copy { 0u8 }
fn bar() > impl Copy { 0u16 }
These functions have the same type, namely β A. A β Copy β§ (() β A)
. That means that you should not be able to tell the difference between them (at least in the type system; when you run the code you can see values, not just types). By contrast, this function has a different type:
fn foo2() > u8 { 0u8 }
This function has the type () β u8
. Despite the fact that foo
and foo2
have the same implementation, they have different types, and callers of foo2
know more about the return value than callers of foo
do, for instance:
fn takes_eq<A: Eq>(f: fn() > A) {}
takes_eq(foo2); // ok
takes_eq(foo); // fails
Using the more explicit destructuring syntax from before, this makes sense:
takes_eq: β A. A β Eq β (() β A) β ()
takes_eq(u8, u8_impl_Eq, foo2); // ok
let (A, A_impl_Copy, f: () β A) = foo;
takes_eq(A, ???: A β Eq, foo); // fails
In the call using foo2
, we supply u8
and a proof of u8 β Eq
in for the hidden arguments. But in the call with foo
, we know only that A
is some type, and we've been given a proof that A β Copy
, but this is of no use to prove A β Eq
, so we are stuck.
First, I want to observe that this is a perfectly well formed type even without the bounds.
fn foo<A, B>(a : A) > B {...}
> β A B. (A β B)
It's even implementable, because Rust has divergence  you can put loop {}
or panic!()
in the body and this will typecheck fine.
As for the reading, it's closer to: "For every combination of a type A
and a type B
, calling foo::<A, B>
with a value of type A
produces a value of type B
." You don't need the "every" in there because you have already quantified over B
at the beginning of the sentence.
This has ended up quite long, but I probably still missed some point of confusion, so let me know if there are better examples I can give. These really are tricky details that a lot of folks don't know, but it's really very valuable once you internalize it.
Thanks! I started reading through it, but couldn't really sit with it yet, will give it a proper read later. Must have taken some time to write that up  much appreciated!