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