类型擦除是好的

让我们坚持事实

到目前为止，很多答案都过于关注twitter用户。把注意力集中在信息上而不是信使上是有帮助的。有一个相当一致的信息，即使只是迄今为止提到的摘录：
有趣的是，当java用户抱怨类型擦除时，这是java唯一做对的事情，而忽略了所有出错的事情。
我得到了巨大的利益（如参数化）和零成本（所谓的成本是想象力的极限）。
新t是一个坏程序。这与“所有命题都是真的”的说法是同构的。我对这一点不感兴趣。

目标：合理的计划

这些推特反映了一种观点，即我们对是否能让机器做一些事情不感兴趣，而更感兴趣的是我们是否能推理机器会做我们真正想要的事情。好的推理就是证明。证明可以用正式的符号或不太正式的东西来指定。无论使用何种规范语言，它们都必须清晰、严格。非正式规范并非不可能正确构造，但在实际编程中常常存在缺陷。我们最终通过自动化和探索性测试等补救措施来弥补我们在非正式推理中遇到的问题。这并不是说测试本质上是一个坏主意，但这位被引用的推特用户表示，有一种更好的方法。
因此，我们的目标是拥有正确的程序，我们可以以一种与机器实际执行程序的方式进行清晰而严格的推理。然而，这并不是唯一的目标。我们也希望我们的逻辑有一定程度的表现力。例如，我们只能用命题逻辑表达这么多。很高兴有一个通用的(∀) 存在主义(∃) 一阶逻辑的量化。

使用类型系统进行推理

类型系统可以很好地实现这些目标。这一点尤其明显，因为咖喱霍华德的信件。这种对应关系通常用以下类比来表示：类型对于程序就像定理对于证明一样。
这种通信有点深奥。我们可以采用逻辑表达式，并通过对应关系将其转换为类型。然后，如果我们有一个具有相同编译类型签名的程序，我们已经证明了逻辑表达式是普遍正确的（重言式）。这是因为通信是双向的。类型/程序和定理/证明世界之间的转换是机械的，在许多情况下可以自动化。
库里·霍华德很好地解释了我们想对程序的规范做些什么。

类型系统在java中有用吗？

即使理解了curry howard，有些人发现当类型系统的值
非常难相处
（通过curry howard）对应于表达能力有限的逻辑
是坏的（这可以将系统描述为“弱”或“强”）。
关于第一点，也许IDE使java的类型系统足够容易使用（这是非常主观的）。
关于第二点，java几乎与一阶逻辑对应。泛型给出了通用量化的类型系统等价物。不幸的是，通配符只为我们提供了存在量化的一小部分。但通用量化是一个很好的开始。很高兴能够说，它的功能 List<A> 对所有可能的列表都通用，因为a完全不受约束。这就引出了twitter用户所谈论的“参数化”
一篇经常被引用的关于参数性的论文是菲利普·瓦德勒的自由定理！。本文有趣的是，仅从类型签名，我们就可以证明一些非常有趣的不变量。如果我们要为这些不变量编写自动化测试，我们将非常浪费时间。比如说, List<A> ，仅针对 flatten ```
List flatten(List<List> nestedLists);

我们可以推理

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

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

### 不擦除可能导致滥用

从语言实现的Angular 来看，java的泛型（对应于通用类型）在用于证明程序功能的参数方面发挥了重要作用。这就涉及到提到的第三个问题。所有这些证据和正确性的获得都需要一个没有缺陷的健全系统。java确实有一些语言特性，可以让我们破坏我们的推理。这些包括但不限于：
外部系统的副作用
反射
非擦除泛型在许多方面与反射相关。在没有擦除的情况下，我们可以使用实现中携带的运行时信息来设计算法。这意味着，静态地讲，当我们对程序进行推理时，我们并没有全面的了解。反射严重威胁着我们静态推理的任何证明的正确性。这不是巧合，反射也会导致各种棘手的缺陷。
那么什么是非擦除泛型可能是有用的呢？让我们考虑推特中提到的用法：

T broken { return new T(); }

如果t没有无参数构造函数会发生什么？在某些语言中，您得到的是空值。或者，您可以跳过空值，直接引发异常（空值似乎会导致异常）。因为我们的语言是图灵完备的，所以不可能对调用 `broken` 将涉及没有参数构造函数的“安全”类型，哪些类型不会。我们已经无法确定我们的程序是否能普遍运行。

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

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

类型是一种结构，用于以允许编译器检查程序正确性的方式编写程序。类型是值上的一个命题-编译器验证该命题是否为真。
在程序执行期间，应该不需要类型信息-这已经由编译器验证。编译器应该可以随意丢弃这些信息，以便对代码执行优化—使其运行更快，生成更小的二进制文件等。删除类型参数有助于实现这一点。
java通过允许在运行时查询类型信息（反射、instanceof等）来打破静态类型。这允许您构造无法静态验证的程序，它们绕过类型系统。它还错过了静态优化的机会。
类型参数被擦除的事实阻止了这些不正确程序的某些示例的构建，但是，如果删除了更多类型信息并删除了设施的反射和示例，则不允许使用更多不正确的程序。
擦除对于维护数据类型的“参数性”属性非常重要。假设我有一个类型“列表”参数化在组件类型t上。i、 e.列表。该类型是一个命题，即该列表类型对任何类型t的作用相同。事实上，t是一个抽象的、无界的类型参数，这意味着我们对这个类型一无所知，因此不能对t的特殊情况做任何特殊的事情。
e、 假设我有一个列表xs=aslist（“3”）。我添加了一个元素：xs.add（“q”）。我以[“3”，“q”]结尾。因为这是参数化的，所以我可以假设list xs=aslist（7）；add（8）以[7,8]结尾，我从类型中知道它对string和int不做一件事。
此外，我知道list.add函数不能凭空发明t的值。我知道如果我的aslist（“3”）中添加了一个“7”，那么唯一可能的答案将由值“3”和“7”构成。不可能将“2”或“z”添加到列表中，因为函数将无法构造它。添加这两个值都是不明智的，参数性可以防止构造这些错误的程序。
基本上，擦除可以防止某些违反参数性的方法，从而消除错误程序的可能性，这是静态键入的目标。

（虽然我已经在这里写了一个答案，但两年后重新审视这个问题时，我意识到还有另一个完全不同的答案，所以我将保留先前的答案，并添加此答案。）
在java泛型上完成的过程是否应该被命名为“类型擦除”，这是非常有争议的。由于泛型类型不会被删除，而是被原始类型替换，所以更好的选择似乎是“类型切割”。
在通常理解的意义上，类型擦除的典型特征是，通过使运行时对其访问的数据结构“盲”，迫使运行时停留在静态类型系统的边界内。这为编译器提供了充分的能力，并允许它仅基于静态类型来证明定理。它还通过限制代码的自由度来帮助程序员，为简单的推理提供更多的能力。
java的类型擦除并不能使编译器瘫痪，如本例所示：

void doStuff(List<Integer> collection) { 
}

void doStuff(List<String> collection) // ERROR: a method cannot have 
                   // overloads which only differ in type parameters

（上述tw