ELI5 "existential"

Just to note - in my foo there was not enough information about B so the compiler can't figure out what the function returns. In yours, B is somewhat defined, albeit via A.

Not sure if this is veering too far off-topic, but with min_type_alias_impl_trait I'm not sure why the callback defined in new() isn't enough and the compiler needs a separate function call to get it?

playground

#![feature(min_type_alias_impl_trait)]

type CallbackFn = impl Fn();

struct Foo {
    cb: CallbackFn
}

impl Foo {
    pub fn new() -> Self {
        Self {
            //This doesn't work
            //cb: || {}
            
            //This does:
            cb: Self::make_callback()
        }
    }
    
    fn make_callback() -> CallbackFn {
        || {}
    }
}

The compiler has a fixed list of possible defining uses, and cb: || {} isn't one of them. :shrug:

1 Like

My own 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()

  • and on nightly, within a type alias definition.
    type Bar = impl Fn();

In all these cases, we know the type described by the impl … syntax is:

  1. a type…

  2. … 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 implements Fn(), we can take a parameter called f of that type"

    • //         +--------------+
      //         |              |
      //         |          ↓↓↓↓↓↓↓↓↓
      fn foo  ↓↓↓↓↓↓↓↓  (f: impl Fn(), …) -> …
      fn foo <F : Fn()> (f: F        , …) -> …
      

    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:

    • //               +-----------------------------+
      //               |                             |
      //           vvvvvvvvvv                        |
      fn baz () -> impl Trait                     // |
      {                                           // |
          struct UnnameableOutside { … }          // |
          impl Trait for UnnameableOutside { … }  // |
          …                                       // |
          return UnnameableOutside { … };         // | fixed type
      } //       ^^^^^^^^^^^^^^^^^                   | but unnameable
        //               |                           | and thus "unknown"
        //               +---------------------------+ to the caller
      

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

6 Likes

Thanks for that awesome explanation @Yandros ! :smiley:

1 Like

As already mentioned, it comes from existential quantification which is related to predicate logic.

It can be described in many ways.

Relating it to generics, one can think of an existential (∃) as a fixed but unknown constant type parameter while all-quantified (∀) type parameters (what we see in rust as normal type parameters) are still volatile given the scope they are declared in, s.t.

fn fun<∃S:Trait,∀T>(s:S,t:T){...}

is equal to f<S>: //of type: Type=>(S,T)=>() (f is applied to type S)

where f is

fn f<S>{return fn fun<T>(s:S,t:T){...}} // of type: Type=>Type=>(S,T)=>()

In return, an existentially quantified type parameter was an all-quantified type parameter before which got bounded by a previous function application (yielded by monomorphization), see post.
So, an existential type parameter is some captured closure parameter, but we don't know what it is because we don't know which closure (in our case f) captured that type parameter and to which type it was set to.

A more set theoretic view of existential types is given in another post.

1 Like

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.