类型擦除很好

让我们坚持事实

到目前为止，很多答案都过于关注Twitter用户。专注于信息而不是信使是有帮助的。到目前为止，甚至只是提到的摘录，都有一个相当一致的信息：

当Java用户抱怨类型擦除时，这很有趣，这是Java唯一正确的事情，而忽略了它做错的所有事情。

我得到了巨大的好处（例如参数化）和零成本（所谓的成本是想象力的极限）。

新的T是一个破碎的程序。它与“所有命题都是正确的”的说法同构。我对此并不感兴趣。

目标：合理的程序

这些推文反映了一种观点，即我们感兴趣的是我们是否能让机器做某事，而是我们是否能推理出机器会做我们真正想要的事情。好的推理就是一个证明。证明可以用形式符号或不太正式的东西来指定。无论规范语言如何，它们都必须清晰而严格。非正式规范并非不可能正确构建，但在实际编程中往往存在缺陷。我们最终得到了自动化和探索性测试等补救措施，以弥补我们在非正式推理方面遇到的问题。这并不是说测试本质上是一个坏主意，但引用的Twitter用户暗示有一个更好的方法。

因此，我们的目标是拥有正确的程序，我们可以以与机器实际执行程序的方式相对应的方式清晰，严格地推理。然而，这并不是唯一的目标。我们也希望我们的逻辑具有一定程度的表现力。例如，我们只能用命题逻辑来表达很多东西。从一阶逻辑中拥有普遍（∀）和存在（∃）量化是很好的。

使用类型系统进行推理

类型系统可以很好地实现这些目标。由于库里-霍华德的通信，这一点尤其明显。这种对应关系通常用以下类比来表示：类型之于程序，就像定理之于证明一样。

这种对应关系有些深刻。我们可以采用逻辑表达式，并通过与类型的对应关系来翻译它们。然后，如果我们有一个具有编译的相同类型签名的程序，我们已经证明逻辑表达式是普遍正确的（重言式）。这是因为对应是双向的。类型/程序和定理/证明世界之间的转换是机械的，在许多情况下可以自动化。

库里-霍华德很好地运用了我们想要对程序规范做的事情。

类型系统在Java中有用吗？

即使了解了库里-霍华德，有些人也很容易忽视类型系统的价值，当它

1. 非常难以合作
2. 对应于（通过库里-霍华德）具有有限表现力的逻辑
3. 被破坏（这将导致系统表征为“弱”或“强”）。

关于第一点，也许IDE使Java的类型系统足够容易使用（这是非常主观的）。

关于第二点，Java恰好几乎对应于一阶逻辑。泛型给出了与通用量化等效的类型系统。不幸的是，通配符只给了我们存在量化的一小部分。但通用量化是一个很好的开始。能够说函数对于所有可能的列表都是通用的，这很好，因为A是完全不受约束的。这导致了Twitter用户在谈论“参数化”方面的内容。List<A>

一篇关于参数化的经常被引用的论文是免费的Philip Wadler定理！这篇论文的有趣之处在于，仅从类型签名，我们就可以证明一些非常有趣的不变量。如果我们要为这些不变量编写自动测试，我们将非常浪费时间。例如，对于 ，仅从 类型签名中List<A>flatten

<A> List<A> flatten(List<List<A>> nestedLists);

我们可以推理

flatten(nestedList.map(l -> l.map(any_function)))
    ≡ flatten(nestList).map(any_function)

这是一个简单的例子，你可以非正式地推理它，但是当我们从类型系统中免费正式获得这样的证明并由编译器检查时，它就更好了。

不擦除可能会导致滥用

从语言实现的角度来看，Java的泛型（对应于通用类型）在用于证明我们程序所做工作的参数化中发挥了重要作用。这就到了提到的第三个问题。所有这些证明和正确性的收益都需要一个没有缺陷的声音类型系统。Java肯定有一些语言特性，可以让我们打破我们的推理。这些包括但不限于：

• 外部系统的副作用
• 反射

未擦除的泛型在许多方面都与反射相关。如果不进行擦除，则实现中携带了运行时信息，我们可以使用它来设计算法。这意味着，静态地，当我们对程序进行推理时，我们并不了解全貌。反思严重威胁到我们静态推理的任何证明的正确性。这不是巧合，反射也会导致各种棘手的缺陷。

那么，非擦除的泛型可能“有用”的方式是什么呢？让我们考虑一下推文中提到的用法：

<T> T broken { return new T(); }

如果 T 没有无 arg 构造函数会发生什么情况？在某些语言中，您得到的是 null。或者，您可能跳过 null 值并直接引发异常（无论如何，null 值似乎会导致异常）。因为我们的语言是图灵完备的，所以不可能推断哪些调用将涉及具有无arg构造函数的“安全”类型，哪些不会。我们已经失去了我们的程序普遍有效的确定性。broken

擦除意味着我们已经推理了（所以让我们擦除）

因此，如果我们想对我们的程序进行推理，强烈建议我们不要使用强烈威胁我们推理的语言功能。一旦我们这样做了，那么为什么不在运行时删除类型呢？它们不是必需的。我们可以获得一些效率和简单性，并满足于没有强制转换会失败，或者在调用时可能会缺少方法。

擦除鼓励推理。

类型是一种用于编写程序的构造，其方式允许编译器检查程序的正确性。类型是对值的命题 - 编译器验证此命题是否为真。

在程序执行期间，应该不需要类型信息 - 这已经由编译器验证。编译器应该可以自由地丢弃这些信息，以便对代码进行优化 - 使其运行得更快，生成更小的二进制文件等。类型参数的擦除有助于实现这一点。

Java通过允许在运行时查询类型信息来打破静态类型 - 反射，实例等。这允许您构造无法静态验证的程序 - 它们绕过类型系统。它还错过了静态优化的机会。

擦除类型参数这一事实可以防止构造这些不正确程序的某些实例，但是，如果擦除了更多类型信息并删除了工具的反射和实例，则将不允许使用更多不正确的程序。

擦除对于维护数据类型的“参数化”属性非常重要。假设我有一个类型“List”，参数化于组件类型T，即List<T>。该类型是一个命题，即此列表类型对于任何类型 T 的工作方式相同。T 是一个抽象的、无界的类型参数，这意味着我们对这个类型一无所知，因此无法对 T 的特殊情况执行任何特殊操作。

例如，假设我有一个List xs = asList（“3”）。我添加一个元素：xs.add（“q”）。我最终得到[“3”，“q”]。由于这是参数化的，我可以假设List xs = asList（7）;xs.add（8） 最终得到 [7，8] 我从类型中知道它不会对 String 做一件事，对 Int 做一件事。

此外，我知道List.add函数不能凭空发明T的值。我知道，如果我的asList（“3”）添加了一个“7”，那么唯一可能的答案将从值“3”和“7”中构造出来。不可能将“2”或“z”添加到列表中，因为该函数无法构造它。添加这些其他值都不明智，并且参数性可以防止构造这些不正确的程序。

基本上，擦除可以防止某些违反参数性的方法，从而消除不正确程序的可能性，这是静态类型化的目标。