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

最近，我被 Alice (@welltypedwit.ch) 的一篇文章深深地“极客狙击”了。她在文中问道：在 Rust 中，dyn Trait 意味着 $\exists s. \text{Trait}(s) \land s$，而 fn f() -> impl Trait 意味着 $f: \exists s. \text{Trait}(s) \land (() \rightarrow s)$。但如果我想对 Self 参数以外的东西进行存在量化（existential）该怎么办？比如，如果我有一个 Trait，而我想要一个 $\exists s, b. \text{Trait}(s, b) \land s$ 呢？这些数学符号看起来很花哨，但我希望读完本文后，你不仅能理解它们的含义，还能明白我对这个问题的回答！

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.

什么是存在量化（Existential Quantifier）？

答案的线索就在她问题的开头：dyn Trait 意味着 $\exists s. \text{Trait}(s) \land s$。让我们思考一下，拥有一个 dyn Trait 类型的值意味着什么。我们知道存在某种底层类型，但我们无法获取该类型本身。我们唯一能做的就是调用 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.

这正是那个公式所表达的含义！“存在（$\exists$）某种类型 $s$，使得（…）$s$ 符合 Trait，并且（$\land$）你现在可以使用 $s$”。那些吓人的数学符号只是表达这一点的简洁方式。数学还有助于我们将这一事实形式化：仅凭这个 $\exists$ 语句，我们无法预先知道 $s$ 是什么。因此，在构建程序类型合法的“证明”时，我们只能假设 $s$ 具备那些源自它符合 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.

Alice 还指出了 Rust 中另一个看起来像存在量化的地方：fn f() -> impl Trait 意味着 $f: \exists s. \text{Trait}(s) \land (() \rightarrow s)$。这种“返回位置的 impl trait”语法确实是指定类型的另一种方式，使得 f 的调用者只知道返回类型符合 Trait 这一事实。与 dyn Trait 不同，这些类型在编译时是固定的，但在类型理论上它们有相似之处。

So! Now that we have a bit of understanding, let’s get started on the real question: What if I have Trait 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: \text{Trait}$?

那么！既然我们有了一些了解，让我们开始探讨真正的问题：如果我有一个 Trait，而我想要一个 $\exists s, b. \text{Trait}(s, b) \land s$ 该怎么办？也就是说，是否可能存在一个被存在量化的类型 $S$，它本身又包含另一个被存在量化的类型变量 $B$，使得 $S: \text{Trait}$？

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))$

尝试 1：全称-存在转换（For-Exists Conversion）

处理任何存在量化的一种经典方法是我所称的“全称-存在转换”。基本上，它依赖于以下恒等式： $((\exists x.P(x)) \rightarrow Q) \Longleftrightarrow (\forall x.(P(x) \rightarrow Q))$

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 $(\langle a, b \rangle \rightarrow c) \Longleftrightarrow (a \rightarrow b \rightarrow c)$. 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.

我的类型理论朋友说“这不就是柯里化（currying）吗，哈哈”，我感到非常困惑，因为我熟悉的柯里化定义是 $(\langle a, b \rangle \rightarrow c) \Longleftrightarrow (a \rightarrow b \rightarrow c)$。也就是说，给定一个接收元组的函数，你可以把它变成一个返回函数的函数，这乍一看与上面提到的存在/全称定理毫无关系。

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 identity: $((\Sigma_\alpha \beta(\alpha)) \rightarrow C) \Longleftrightarrow (\Pi_\alpha \beta(\alpha) \rightarrow C)$

然而！如果你有一个“依赖和”（dependent sum）$\Sigma_\alpha \beta(\alpha)$（第二个元素 $\beta$ 的类型取决于第一个元素 $\alpha$ 的值）和一个“依赖积”（dependent product）$\Pi_\alpha \beta(\alpha)$（返回类型 $\beta$ 取决于输入 $\alpha$ 值的函数），那么你会得到一个看起来非常相似的恒等式： $((\Sigma_\alpha \beta(\alpha)) \rightarrow C) \Longleftrightarrow (\Pi_\alpha \beta(\alpha) \rightarrow C)$

You can interpret both sides either way: 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$.

你可以从两个角度解释这两边：在“类型即命题”的解释中，$\Sigma$ 有点像 $\exists$，因为要使其被填充（inhabited），你只需要一个 $\langle \alpha, \beta(\alpha) \rangle$ 对；而 $\Pi$ 有点像 $\forall$，因为要使其被填充，你需要展示如何为每一个可能的 $\alpha$ 得到一个 $\beta(\alpha)$。

Interpreting them as datastructures, $\Sigma$ is just a tuple, and $\Pi$ is just a function, which is exactly what our original currying looks like. 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!

如果将它们解释为数据结构，$\Sigma$ 只是一个元组，而 $\Pi$ 只是一个函数，这正是我们最初的柯里化所表现的样子。所以，我的类型理论朋友认为“你应该称之为‘柯里化’，而不是编造一个新名字”。但我不同意这一点，因为这种联系并不明显，为了清晰起见，我还是坚持用我自己的名字 :) 学无止境！

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.

在 Rust 中，这可以表示为： fn f_left(x: impl P) -> Q { x.foobar() } fn f_right<X: P>(x: X) -> Q { x.foobar() } “但是 PolyWolf！”我听到你说，“你不是写了两次相同的函数吗？？”亲爱的读者，这正是这个恒等式狡猾的地方。它看起来显而易见，但实际上它表达了一些非常深刻的东西。

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.

f_left 确实为其参数使用了存在量化（关于 x 你所知道的全部就是它的类型符合 P），而 f_right 首先对 X 的所有可能类型进行量化，然后限制为那些满足 trait P 的类型。在 Rust 中，你可能认为前者只是后者的“语法糖”，但这并不能改变它们是不同数学陈述的事实。

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.

为了更清楚地看到这一点，让我们思考一下当我们将这些参数类型用作返回类型时会发生什么： fn g1() -> impl P { SpecificX::proof() } fn g2<X: P>() -> X { X::proof() } 在这里，我们可以更清楚地看到 impl P 和 X: P 表达了不同的含义。前者像 $\exists$ 一样，只要求你展示一个满足 trait P 的 SpecificX；而后者像 $\forall$ 一样，要求你为所有可能的 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 Trait(s, b) is some S: Generic (renamed to avoid confusion w/ other traits introduced later), and that we can only build new types/traits that refe…

那么！回到我们最初的问题，我们想要描述一种形式为 $\exists s, b. \text{Trait}(s, b) \land s$ 的类型。在本文的剩余部分，我们将假设 Trait(s, b) 是某种 S: Generic（为了避免与稍后引入的其他 trait 混淆而重命名），并且我们只能构建引用…的新类型/trait。