ELI5 "existential"

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 "callee-chosen", whereas a universal type is caller-chosen.

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 implements Fn(),

  • 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 prevents1 leaking properties that stem from implementation details that could change, and which thus prevent making such changes within semver-compatible changes.

    1 I don't know exactly about type_alias_impl_trait, but for the "classic" -> impl Trait in return position (thus, existential), the auto_traits such as Send and Sync do leak… EDIT: it turns out that for min_type_alias_impl_trait auto-traits cause a weird type error

3 Likes

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

2 Likes

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.

2 Likes

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 compile-time with type-level generics and static dispatch, or be it at runtime with virtual-method-based 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 :slightly_smiling_face:


Hmm, there is some meta-level 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 parameters1, 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.

3 Likes

The trick might boil down to

  1. First ask, what can I say about the quantity of x?
  2. Test the following first: Can I describe it as "always" or "all"? => universal, if not...
  3. 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...
  4. 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...".

3 Likes

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 {}) :upside_down_face:

3 Likes

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.

1 Like

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.

1 Like

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 non-1 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 :crazy_face:... 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 caller-chosen and existential types being callee-chosen 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 Rust-ish 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.

5 Likes

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!