Erasing Existentials

Recently, I got nerd-sniped hard by a post made by Alice (@welltypedwit.ch). In it, she asks:

So, in Rust, dyn Trait means $\exists s. \text{Trait}(s) \land s$ , and fn f() -> impl Trait means $f: \exists s. \text{Trait}(s) \land (() \rightarrow s)$ , but what if I want an existential over something other than the Self parameter? Like, what if I have Trait<B> and I want an $\exists s, b. \text{Trait}(s, b) \land s$ ?

That is a lot of fancy math symbols, but I hope by the end of this you will understand both what they mean and my answer to this question!

What Is An Existential Quantifier?

A hint can be found in the first part of her question:

dyn Trait means $\exists s. \text{Trait}(s) \land s$

Let's think about what it means to have a value of type dyn Trait¹. We know there is some underlying type, but we don't have a way of getting at that type. All we can do is call methods from Trait.

That's pretty much exactly what that formula says! "There exists ( $\exists$ ) some type s, such that ( $.$ ) s conforms to Trait, and ( $\land$ ) you can use s right now". The scary math symbols are just a concise way of writing that. Math also helps us formalize the fact that, given just this $\exists$ statement, we have no way of knowing what s will be ahead of time, so in constructing a "proof" that the program is well-typed, we can only assume things about s that come from it conforming to Trait².

Alice also points out another place Rust has something that looks like an existential quantifier:

fn f() -> impl Trait means $f: \exists s. \text{Trait}(s) \land (() \rightarrow s)$

This "return-position impl trait" syntax is indeed another way of specifying a type such that callers of f only know about the fact that the return type conforms to Trait. Unlike with dyn Trait, these are fixed at compile time, but type-theoretically they're somewhat similar.

So! Now that we have a bit of understanding, let's get started on the real question:

What if I have Trait<B> and I want an $\exists s,b. \text{Trait}(s, b) \land s$ ?

That is, is it possible to have an existentially quantified type S that itself has another existentially quantified type variable B, such that S: Trait<B>?

Attempt 1: For-Exists Conversion

A classic way of dealing with any existentials is something I call "for-exists conversion". Basically, it relies on the following identity:

$((\exists x.P(x)) \rightarrow Q) \Longleftrightarrow (\forall x.(P(x) \rightarrow Q))$

In Rust, this can be stated as:

fn f_left(x: impl P) -> Q {
    x.foobar()
}

fn f_right<X: P>(x: X) -> Q {
    x.foobar()
}

"But PolyWolf!" I hear you say, "You've just written the same function twice??" And that, dear reader, is exactly what's so sneaky about this identity. It seems obvious, but it's actually saying something pretty profound.

f_left really does use an existential quantifier for its argument (all you know about x is that it has a type conforming to P), while f_right first quantifies over all possible types for X, then restricts to those that satisfy the trait P. In Rust, you might think the former is "just sugar for" the latter, but that doesn't change the fact these are different mathematical statements.

To see this more clearly, let's think about what happens when we use those argument types as return types instead:

fn g1() -> impl P { SpecificX::proof() }

fn g2<X: P>() -> X { X::proof() }

Here, we can more clearly see that impl P and X: P are saying different things. The former, like $\exists$ , only requires you to demonstrate a SpecificX that satisfies the trait P, while the latter, like $\forall$ , requires you to produce valid values for all possible X: P.

So! Getting back to our original problem, we want to describe a type of the form:

$\exists s, b. \text{Trait}(s, b) \land s$ For the rest of this post, we're going to assume that $\text{Trait(s, b)}$ is some S: Generic<B> (renamed to avoid confusion w/ other traits introduced later), and that we can only build new types/traits that reference it, never modifying it or the following impls:

pub trait Generic<B> {
    fn name(&self) -> &'static str;
}
impl Generic<f32> for i32 {
    fn name(&self) -> &'static str { "f32" }
}
impl Generic<f64> for i32 {
    fn name(&self) -> &'static str { "f64" }
}

Restricting ourselves first to functions that take in such a type, we get:

$(\exists s, b. \text{Trait}(s, b) \land s) \rightarrow ()$

Then, using our identity, we can rewrite it as:

$\forall s, b. (\text{Trait}(s, b) \land s) \rightarrow ()$

This results in the following function (playground link):

fn use_generic<B, S: Generic<B>>(s: &S) -> &'static str {
    s.name()
}

Easy peasy! This is a very standard way of dealing with the problem, and imo the most clean. However, Alice was not satisfied:

You couldn't e.g. put this one in a data structure (behind a Box) though, could you?

And that's entirely true! Due to the way we rephrased the problem in terms of $\forall$ , once we return a Box<dyn Generic<B>>, we'd have to keep a $\forall b$ clause around on everything that uses it, which sort of defeats the purpose of having $\exists$ types in the first place (playground link):

fn put_in_box<B, S: Generic<B> + 'static>(s: S) -> Box<dyn Generic<B>> {
    Box::new(s)
}

fn use_box<B>(s: &Box<dyn Generic<B>>) -> &'static str {
    s.name()
}

This solution may be satisfactory for some usecases, but we'll have to try a bit harder to get things to only use $\exists$ .

Attempt 2: Associated Types

My next idea was to "smuggle" the $\exists s, b.$ quantifier behind a single $\exists t.$ quantifier that Rust gives when using trait objects. A first crack at it might look something like (playground link):

trait SingleAssociated {
    type B;
}

impl<B, S: Generic<B>> SingleAssociated for S {
    type B = B;
}

However, we quickly run into a problem:

error[E0207]: the type parameter `B` is not constrained by the impl trait, self type, or predicates
  --> src/main.rs:15:6
   |
15 | impl<B, S: Generic<B>> SingleAssociated for S {
   |      ^ unconstrained type parameter

The E0207 docs do an excellent job explaining this (you should try rustc --explain if you haven't already!), but the short version is, whenever we're implementing traits, Rust wants there to be at most one concrete trait implementation for every concrete type. This restriction is called "coherence", because it would be "incoherent" if we could choose between multiple possible trait implementations for a single type⁴. When we write impl<B, S: Generic<B>>, Rust considers all possible B and S that fit the criteria before moving onto the rest of the code. However, "all possible B" could result in more than one SingleAssociated for S implementations, so we are not allowed to do that.

To get around this, we'll have to put B in either the trait or type, to "constrain" it. We can't put it in the SingleAssociated trait definition (that would make it the same as Generic<B>!), and we can't put it in S (it's already generic), so what can we possibly do? PhantomData :)

PhantomData is a zero-sized type that lets us to implement the SingleAssociated trait for something that, at runtime, is basically the same as a normal S, just with extra type-level information:

use std::marker::PhantomData;

impl<B, S: Generic<B>> SingleAssociated for (S, PhantomData<B>) {
    type B = B;
}

fn mk_existential<B, S: Generic<B>>(s: S) -> impl SingleAssociated {
    (s, PhantomData)
}

Great, mission accomplished, right? Except wait... how do we actually use it?? (playground link)

fn use_existential(_s: &impl SingleAssociated) -> &'static str {
    todo!()
}

The whole point of our existential type is to carry a proof about how we can do stuff with the Generic trait. But on its own, the SingleAssociated trait doesn't let us get at anything that implements Generic<B>. We know that it is only implemented for our special tuple type, but Rust doesn't, so we have to help it along by adding a second associated type + a function to get at it:

trait DoubleAssociated {
    type S: Generic<Self::B>;
    type B;
    fn as_ref(&self) -> &Self::S;
}

impl<S, B> DoubleAssociated for (S, PhantomData<B>)
where
    S: Generic<B>,
{
    type S = S;
    type B = B;
    fn as_ref(&self) -> &Self::S { &self.0 }
}

This lets us use functions from Generic<B>⁵ (playground link):

fn mk_existential<B, S: Generic<B>>(s: S) -> impl DoubleAssociated {
    (s, PhantomData)
}

fn use_existential(s: &impl DoubleAssociated) -> &'static str {
    s.as_ref().name()
}

Great! If we were satisfied with using $\exists$ types as returned from functions, we could stop here.

...However, to satisfy Alice's request, we'd also like to be able to "erase" that type by putting it in a Box<dyn Trait>, giving it a consistent representation; otherwise, two functions that both return impl DoubleAssociated could actually be returning different types, and e.g. couldn't be put inside the same Vec. We should able to do Box<dyn DoubleAssociated>, so let's try that, shall we? (playground link):

fn mk_box<B: 'static, S: Generic<B> + 'static>(s: S) -> Box<dyn DoubleAssociated<S=S, B=B>> {
    Box::new((s, PhantomData))
}

fn use_box(s: &Box<dyn DoubleAssociated>) -> &'static str {
    DoubleAssociated::as_ref(Box::as_ref(s)).name()
}

Whuh oh

error[E0191]: the value of the associated types `S` and `B` in `DoubleAssociated` must be specified
  --> src/main.rs:44:24
   |
14 |     type S: Generic<Self::B>;
   |     ------------------------ `S` defined here
15 |     type B;
   |     ------ `B` defined here
...
44 | fn use_box(s: &Box<dyn DoubleAssociated>) -> &'static str {
   |                        ^^^^^^^^^^^^^^^^
   |
help: specify the associated types
   |
44 | fn use_box(s: &Box<dyn DoubleAssociated<S = /* Type */, B = /* Type */>>) -> &'static str {
   |                                        ++++++++++++++++++++++++++++++++

It wants us to use $\forall$ again... to be honest, I totally did not expect this. I thought the fact that Rust enforces "at most one concrete trait implementation per concrete type" meant associated types could be stored in the trait object vtable somehow, but my intuition was way wrong on that.

Thinking on it further, the fact that we return things type Associated::S means that, at runtime, different DoubleAssociated impls will necessarily have different vtables, because return types will have different layouts, so the trait objects with different associated types MUST be different. Rust 1 – Me 0

So, what can we take away from this? That it's impossible to fully automatically erase multiple existential bounds in Rust in the same type, because it only supports one at a time with dyn Trait? Unfortunately yes, that is my takeaway here :(

Still, if we're willing to put in a little bit more legwork, it is possible to manually collapse multiple existential bounds into one.

Attempt 3: Manual Erasing

Forget trying to use functions from Generic<B> directly, let's instead create a trait that manually, for each function we care about, passes thru to the function from the trait:

trait Erased {
    fn name(&self) -> &'static str;
}

impl<B, S: Generic<B>> Erased for (S, PhantomData<B>) {
    fn name(&self) -> &'static str {
        self.0.name()
    }
}

This works!! We can even box it, hooray (playground link):

fn mk_box<B: 'static, S: Generic<B> + 'static>(s: S) -> Box<dyn Erased> {
    Box::new((s, PhantomData))
}

fn use_box(b: &Box<dyn Erased>) -> &'static str {
    b.name()
}

Alice has one last request for us here:

hmmm but now this one doesn't work if the trait actually uses the B parameter right? (because you can't use it in Erased)

And that is true: Erased intentionally has no way for it to vary what types it cares about, everything needs to be concrete so it can be put inside a dyn without issues. If we want to deal with multiple types, we'll have to use std::any::Any to handle them at runtime. Here's an example (playground link):

use std::any::Any;
use std::marker::PhantomData;

trait Generic<B> {
    fn input(b: &B);
    fn output(&self) -> B;
}
impl Generic<f32> for i32 {
    fn input(b: &f32) { println!("f32: {b}") }
    fn output(&self) -> f32 { *self as f32 }
}
impl Generic<f64> for i32 {
    fn input(b: &f64) { println!("f64: {b}") }
    fn output(&self) -> f64 { *self as f64 }
}

trait Erased {
    fn input(&self, b: &Box<dyn Any>);
    fn output(&self) -> Box<dyn Any>;
}

impl<B: 'static, S: Generic<B>> Erased for (S, PhantomData<B>) {
    fn input(&self, b: &Box<dyn Any>) {
        S::input(b.downcast_ref().unwrap())
    }
    fn output(&self) -> Box<dyn Any> {
        Box::new(self.0.output())
    }
}

This compiles & runs successfully! Unfortunately, as you can see, manual erasure has a few drawbacks besides just dyn-compatibility.

This process, as I've outlined above, is very manual: you have to rewrite every function signature to include Box<dyn Any> instead of B, and make a decision for each about whether to .unwrap() or propagate the error up somehow. If there are enough functions to do this conversion on, you could write a macro_rules! to define a Generic<B> and Erased trait at the same time, but that seems very finnicky and I have been nerd-sniped enough already so I will not attempt that here :P

Anyways that's it, thanks for reading, hope you learned a little something in the process!