问题描述
今天我读了说：
因此我的问题是：
推荐答案
类型擦除是好的
让我们坚持事实
很多到目前为止，答案过于关注Twitter用户。保持专注于消息而不是信使是有帮助的。即使只是到目前为止提到的摘录，也有一个相当一致的信息：
Type Erasure Is Good
Let's stick to the facts
A lot of the answers thus far are overly concerned with the Twitter user. It's helpful to keep focused on the messages and not the messenger. There is a fairly consistent message with even just the excerpts mentioned thus far:
我获得了巨大的利益（例如参数）和零成本（所谓的成本是想象力的极限） 。
I get huge benefits (e.g. parametricity) and nil cost (alleged cost is a limit of imagination).
新T是一个破碎的程序。这与所有命题都是真实的主张是同构的。我对此并不大感。
new T is a broken program. It is isomorphic to the claim "all propositions are true." I am not big into this.
目标：合理的计划
这些推文反映了一个视角，我们不知道我们是否可以让机器做某事，但更多的是我们是否可以推断机器会做我们真正想要的事情。好的推理就是证据。证明可以用正式表示法或不太正式的表示。无论规范语言如何，它们都必须清晰严谨。非正式规范并非不可能正确地构造，但在实际编程中通常是有缺陷的。我们最终采用自动化和探索性测试等补救措施来弥补我们在非正式推理中遇到的问题。这并不是说测试本质上是一个坏主意，但引用的Twitter用户建议有更好的方法。
A goal: reasonable programs
These tweets reflect a perspective that is not interested in whether we can make the machine do something, but more whether we can reason that the machine will do something we actually want. Good reasoning is a proof. Proofs can be specified in formal notation or something less formal. Regardless of the specification language, they must be clear and rigorous. Informal specifications are not impossible to structure correctly, but are often flawed in practical programming. We end up with remediations like automated and exploratory tests to make up for the problems we have with informal reasoning. This is not to say that testing is intrinsically a bad idea, but the quoted Twitter user is suggesting that there is a much better way.
所以我们的目标是要有正确的我们能够以与机器实际执行程序的方式相对应的方式清楚而严谨地推理的程序。但是，这不是唯一的目标。我们也希望我们的逻辑具有一定程度的表达能力。例如，我们只能用命题逻辑表达这么多。从一阶逻辑中得到通用（∀）和存在（∃）量化是很好的。
So our goal is to have correct programs that we can reason about clearly and rigorously in a way that corresponds with how the machine will actually execute the program. This, though, is not the only goal. We also want our logic to have a degree of expressivity. For example, there's only so much we can express with propositional logic. It's nice to have universal (∀) and existential (∃) quantification from something like first-order logic.
类型系统可以非常好地解决这些目标。由于，这一点尤为明显。这种对应关系通常用以下类比来表达：类型是程序，因为定理是证明。
These goals can be very nicely addressed by type systems. This is especially clear because of the Curry-Howard correspondence. This correspondence is often expressed with the following analogy: types are to programs as theorems are to proofs.
这种对应有点深刻。我们可以采用逻辑表达式，并通过对应的类型转换它们。然后，如果我们有一个具有相同类型签名的程序，我们已经证明逻辑表达式是普遍正确的（重言式）。这是因为通信是双向的。类型/程序与定理/证明世界之间的转换是机械的，并且在许多情况下可以自动化。
This correspondence is somewhat profound. We can take logical expressions, and translate them through the correspondence to types. Then if we have a program with the same type signature that compiles, we have proven that the logical expression is universally true (a tautology). This is because the correspondence is two-way. The transformation between the type/program and the theorem/proof worlds are mechanical, and can in many cases be automated.
Curry-Howard非常适合我们想要的与程序规范有关。
Curry-Howard plays nicely into what we'd like to do with specifications for a program.
即使了解Curry-Howard，有些人发现很容易忽略类型系统的价值，当它
Even with an understanding of Curry-Howard, some people find it easy to dismiss the value of a type system, when it
- 非常难以使用
- 对应（通过Curry-Howard）具有有限表现力的逻辑
- 被破坏（这使系统的特征变为弱或强 ）。
关于第一点，也许IDE可以使Java的类型系统易于使用（这是非常主观的）。
Regarding the first point, perhaps IDEs make Java's type system easy enough to work with (that's highly subjective).
关于第二点，Java碰巧几乎对应于一阶逻辑。泛型使用类型系统相当于通用量化。不幸的是，通配符只给我们一小部分存在量化。但普遍量化是一个很好的开端。很高兴能够说 List< A> 的功能普遍用于所有可能的列表，因为A完全不受约束。这导致了Twitter用户在参数化方面所谈论的内容。
Regarding the second point, Java happens to almost correspond to a first-order logic. Generics give use the type system equivalent of universal quantification. Unfortunately, wildcards only give us a small fraction of existential quantification. But universal quantification is pretty good start. It's nice to be able to say that functions for List<A> work universally for all possible lists because A is completely unconstrained. This leads to what the Twitter user is talking about with respect to "parametricity."
一篇经常被引用的关于参数化的论文是Philip Wadler的。这篇论文的有趣之处在于，仅从类型签名，我们就可以证明一些非常有趣的不变量。如果我们要为这些不变量编写自动化测试，我们将非常浪费时间。例如，对于列表< A> ，仅从类型签名中为展平
An often-cited paper about parametricity is Philip Wadler's Theorems for free!. What's interesting about this paper is that from just the type signature alone, we can prove some very interesting invariants. If we were to write automated tests for these invariants we would be very much wasting our time. For example, for List<A>, from the type signature alone for flatten
<A> List<A> flatten(List<List<A>> nestedLists);
我们可以推理
flatten(nestedList.map(l -> l.map(any_function)))
≡ flatten(nestList).map(any_function)
这是一个简单的例子，你可以非正式地推理它，但是当我们从类型系统正式免费获得这样的证据并检查时它更好编译器。
That's a simple example, and you can probably reason about it informally, but it's even nicer when we get such proofs formally for free from the type system and checked by the compiler.
从语言实现的角度来看，Java的泛型（对应于通用类型）非常重视参数，用于获取我们的程序所做的证明。这就到了提到的第三个问题。所有这些证明和正确性的提高都需要一个没有缺陷的声音类型系统。 Java绝对有一些语言功能，可以让我们打破我们的推理。这些包括但不限于：
From the perspective of language implementation, Java's generics (which correspond to universal types) play very heavily into the parametricity used to get proofs about what our programs do. This gets to the third problem mentioned. All these gains of proof and correctness require a sound type system implemented without defects. Java definitely has some language features that allow us to shatter our reasoning. These include but are not limited to:
- 使用外部系统的副作用
- reflection
未擦除的泛型在许多方面与反射有关。没有擦除，就会有我们可以用来设计算法的实现带来的运行时信息。这意味着静态地说，当我们推理程序时，我们没有完整的图片。反思严重威胁我们静态推理的任何证据的正确性。这并非巧合反映也会导致各种棘手的缺陷。
Non-erased generics are in many ways related to reflection. Without erasure there's runtime information that's carried with the implementation that we can use to design our algorithms. What this means is that statically, when we reason about programs, we don't have the full picture. Reflection severely threatens the correctness of any proofs we reason about statically. It's no coincidence reflection also leads to a variety of tricky defects.
那么，非擦除仿制药可能有什么用处呢？让我们考虑一下推文中提到的用法：
So what are ways that non-erased generics might be "useful?" Let's consider the usage mentioned in the tweet:
<T> T broken { return new T(); }
如果T没有no-arg构造函数会怎样？在某些语言中，你得到的是null。或者也许你跳过null值并直接引发异常（无论如何都会导致null值）。因为我们的语言是图灵完整的，所以不可能推断哪些对已破坏的调用将涉及带有无参数构造函数的安全类型，哪些不会。我们已经失去了我们的程序普遍适用的确定性。
What happens if T doesn't have a no-arg constructor? In some languages what you get is null. Or perhaps you skip the null value and go straight to raising an exception (which null values seem to lead to anyway). Because our language is Turing complete, it's impossible to reason about which calls to broken will involve "safe" types with no-arg constructors and which ones won't. We've lost the certainty that our program works universally.
因此，如果我们想要推理我们的课程，我们强烈建议不要使用强烈威胁我们推理的语言功能。一旦我们这样做，为什么不在运行时删除类型？他们不需要。我们可以获得一些效率和简单性，满意的是没有强制转换会失败或者调用时可能会丢失方法。
So if we want to reason about our programs, we're strongly advised to not employ language features that strongly threaten our reasoning. Once we do that, then why not just drop the types at runtime? They're not needed. We can get some efficiency and simplicity with the satisfaction that no casts will fail or that methods might be missing upon invocation.
擦除鼓励推理。
这篇关于Java类型擦除有什么好处？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！