java - Java 的类型删除有什么好处？

Question

我读了 tweet今天说:

It's funny when Java users complain about type erasure, which is the only thing Java got right, while ignoring all the things it got wrong.

因此我的问题是:
Java 的类型删除有什么好处吗？除了 JVM 实现对向后兼容性和运行时性能的偏好之外，它(可能)提供哪些技术或编程风格的好处？

Answer 1

类型删除是好的
让我们坚持事实
到目前为止，很多答案都过度关注 Twitter 用户。专注于消息而不是信使是有帮助的。即使只是到目前为止提到的摘录，也有一个相当一致的信息:

It's funny when Java users complain about type erasure, which is the only thing Java got right, while ignoring all the things it got wrong.

I get huge benefits (e.g. parametricity) and nil cost (alleged cost is a limit of imagination).

new T is a broken program. It is isomorphic to the claim "all propositions are true." I am not big into this.

一个目标:合理的方案
这些推文反射(reflect)的观点不是我们是否可以让机器做某事，而是我们是否可以推理机器会做我们真正想做的事情。好的推理是一个证明。证明可以用正式的符号或不太正式的东西来指定。无论使用何种规范语言，它们都必须清晰、严谨。非正式规范并非不可能正确构建，但在实际编程中往往存在缺陷。我们最终通过自动化和探索性测试等补救措施来弥补我们在非正式推理方面遇到的问题。这并不是说测试本质上是一个坏主意，但引用的 Twitter 用户表示有更好的方法。
因此，我们的目标是拥有正确的程序，我们可以以与机器实际执行程序的方式相对应的方式清晰而严格地推理这些程序。然而，这并不是唯一的目标。我们还希望我们的逻辑具有一定程度的表现力。例如，我们只能用命题逻辑表达这么多。从一阶逻辑之类的东西中获得通用 (∀) 和存在 (∃) 量化是很好的。
使用类型系统进行推理
类型系统可以很好地解决这些目标。这一点尤其明显，因为 Curry-Howard correspondence .这种对应关系通常用以下类比来表示:类型之于程序，正如定理之于证明。
这个对应有点深刻。我们可以把逻辑表达式，通过类型的对应关系来翻译。然后，如果我们有一个具有相同类型签名的程序可以编译，我们就证明了逻辑表达式是普遍正确的(重言式)。这是因为对应是双向的。类型/程序和定理/证明世界之间的转换是机械的，并且在许多情况下可以自动化。
库里-霍华德(Curry-Howard)很好地满足了我们对程序规范的要求。
类型系统在 Java 中有用吗？
即使了解 Curry-Howard，有些人也发现很容易忽视类型系统的值(value)，当它

与

一起工作非常困难

对应(通过 Curry-Howard)一个表达能力有限的逻辑

被破坏(这可以将系统描述为“弱”或“强”)。

关于第一点，也许 IDE 使 Java 的类型系统易于使用(这是非常主观的)。
关于第二点，Java 恰好对应于一阶逻辑。泛型使用等同于通用量化的类型系统。不幸的是，通配符只给了我们存在量化的一小部分。但普遍量化是一个很好的开始。很高兴能够说 List<A> 的功能普遍适用于所有可能的列表，因为 A 是完全不受约束的。这导致了 Twitter 用户所谈论的“参数化”。
一篇经常被引用的关于参数化的论文是 Philip Wadler 的 Theorems for free! .这篇论文的有趣之处在于，仅从类型签名，我们就可以证明一些非常有趣的不变量。如果我们要为这些不变量编写自动化测试，我们将非常浪费时间。例如，对于 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 的泛型(对应于通用类型)在参数化中扮演着非常重要的角色，用于获得我们的程序所做的证明。这就涉及到第三个问题。所有这些证明和正确性的 yield 都需要一个健全的类型系统，没有缺陷。 Java 肯定有一些语言特性可以让我们打破我们的推理。这些包括但不限于:

外部系统的副作用

反射

非删除泛型在很多方面都与反射有关。在没有删除的情况下，我们可以用来设计算法的实现会携带运行时信息。这意味着静态地，当我们对程序进行推理时，我们并没有全面了解。反射严重威胁我们静态推理的任何证明的正确性。并非巧合，反射也会导致各种棘手的缺陷。
那么，非删除泛型可能“有用”的方式有哪些？让我们考虑一下推文中提到的用法:

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

如果 T 没有无参数构造函数会发生什么？在某些语言中，您得到的是空值。或者您可能跳过空值并直接引发异常(空值似乎无论如何都会导致)。因为我们的语言是图灵完备的，所以无法推断对 broken 的哪些调用将涉及带有无参数构造函数的“安全”类型，哪些不会。我们已经失去了我们的程序普遍适用的确定性。
删除意味着我们已经推理(所以让我们删除)
因此，如果我们想对我们的程序进行推理，我们强烈建议不要使用严重威胁我们推理的语言特性。一旦我们这样做了，那为什么不直接在运行时删除类型呢？他们不需要。我们可以获得一些效率和简单性，满意的是没有强制转换会失败或者调用时可能会丢失方法。
删除鼓励推理。