Erasing Existentials

Summary

Recently, I got nerd-sniped hard by a post made by Alice (@welltypedwit.ch). In it, she asks: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<B> 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!What Is An Existential Quantifier?A hint can be found in the first part of her question:dyn Trait means ∃s.Trait(s)∧s\exists s. \text{Trait}(s) \land s∃s.Trait(s)∧sLet'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:∃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 somewh...