wolfgirl.dev - Erasing Existentials<br>Erasing Existentials<br>Published on 2026-05-20 at 09:43:32<br>Recently, I got nerd-sniped hard by a post made by Alice (@welltypedwit.ch). In it, she asks:<br>So, in Rust, dyn Trait means ∃s.Trait(s)∧s\exists s. \text{Trait}(s) \land s∃s.Trait(s)∧s , and fn f() -> impl Trait means f:∃s.Trait(s)∧(()→s)f: \exists s. \text{Trait}(s) \land (() \rightarrow s)f:∃s.Trait(s)∧(()→s) , but what if I want an existential over something other than the Self parameter? Like, what if I have Trait and I want an ∃s,b.Trait(s,b)∧s\exists s, b. \text{Trait}(s, b) \land s∃s,b.Trait(s,b)∧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!<br>What Is An Existential Quantifier?<br>A hint can be found in the first part of her question:<br>dyn Trait means ∃s.Trait(s)∧s\exists s. \text{Trait}(s) \land s∃s.Trait(s)∧s

Let's think about what it means to have a value of type dyn Trait1. 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.<br>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 Trait2.<br>Alice also points out another place Rust has something that looks like an existential quantifier:<br>fn f() -> impl Trait means f:∃s.Trait(s)∧(()→s)f: \exists s. \text{Trait}(s) \land (() \rightarrow s)f:∃s.Trait(s)∧(()→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.<br>So! Now that we have a bit of understanding, let's get started on the real question:<br>What if I have Trait and I want an ∃s,b.Trait(s,b)∧s\exists s,b. \text{Trait}(s, b) \land s∃s,b.Trait(s,b)∧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?<br>Attempt 1: For-Exists Conversion<br>A classic way of dealing with any existentials is something I call "for-exists conversion". Basically, it relies on the following identity:<br>((∃x.P(x))→Q)⟺(∀x.(P(x)→Q)) ((\exists x.P(x)) \rightarrow Q) \Longleftrightarrow (\forall x.(P(x) \rightarrow Q)) ((∃x.P(x))→Q)⟺(∀x.(P(x)→Q))<br>Type theory friend My type theory friend said "this is just currying lol" and I was very confused, because the definition for currying I'm familiar with is<br>(⟨a,b⟩→c)⟺(a→b→c) (\langle a, b \rangle \rightarrow c) \Longleftrightarrow (a \rightarrow b \rightarrow c) (⟨a,b⟩→c)⟺(a→b→c)<br>That is, given a function taking a tuple, you can make it into a function returning a function, which at first glance looks nothing like the exists/forall theorem stated above.<br>However! If you have a "dependent sum" Σαβ(α)\Sigma_\alpha \beta(\alpha)Σα​β(α) (type of second element β\betaβ depends on value of first element α\alphaα ) and a "dependent product" Παβ(α)\Pi_\alpha \beta(\alpha)Πα​β(α) (function where the return type β\betaβ depends on the value of the input α\alphaα ), then you get a very similar-looking identity3:<br>((Σαβ(α))→C)⟺(Παβ(α)→C) ((\Sigma_\alpha \beta(\alpha)) \rightarrow C) \Longleftrightarrow (\Pi_\alpha \beta(\alpha) \rightarrow C) ((Σα​β(α))→C)⟺(Πα​β(α)→C)<br>You can interpret both sides either way:<br>In the "types as propositions" interpretation, Σ\SigmaΣ is kind of like ∃\exists∃ in that, for it to be inhabited, you only need a single ⟨α,β(α)⟩\langle \alpha, \beta(\alpha) \rangle⟨α,β(α)⟩ pair, and Π\PiΠ is kind of like ∀\forall∀ in that, for it to be inhabited, you need to show how to get a β(α)\beta(\alpha)β(α) for every possible α\alphaα .<br>Interpreting them as datastructures, Σ\SigmaΣ is just a tuple, and Π\PiΠ is just a function, which is exactly what our original currying looks like.<br>So, my type theory friend argues "you should call this 'currying' instead of making up a new name". But I don't agree with that since the connection is not obvious, so I will stick with my own name for the sake of clarity :) The more you know!<br>In Rust, this can be stated as:<br>fn f_left(x: impl P) -> Q {<br>x.foobar()

fn f_rightX: P>(x: X) -> Q {<br>x.foobar()<br>}"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.<br>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),...