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

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

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

擦除类型参数的事实可以防止构造这些错误程序的某些实例,但是,如果删除了更多类型信息并且删除了反射和实例设施,则将不允许更多不正确的程序.

擦除对于维护数据类型的"参数化"属性很重要.假设我在组件类型T上有一个参数类型"List",即List <T>.该类型是一个命题,这个List类型对于任何类型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",因为该函数无法构造它.这些其他值都不适合添加,并且参数化可以防止构造这些不正确的程序.

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

类型擦除是好的

让我们坚持事实

到目前为止,很多答案都过分关注Twitter用户.保持专注于消息而不是信使是有帮助的.即使只是到目前为止提到的摘录,也有一个相当一致的信息:

当Java用户抱怨类型擦除时,这很有趣,这是Java唯一正确的做法,而忽略了所有错误的东西.

我获得了巨大的收益(例如参数)和零成本(所谓的成本是想象力的极限).

新T是一个破碎的程序.这与"所有命题都是真实的"主张是同构的.我对此并不陌生.

目标:合理的计划

这些推文反映了一个观点,它对我们是否可以让机器做某事不感兴趣,但更多的是我们是否可以推断机器会做我们真正想要的事情.良好的推理是一个证明.证明可以用正式表示法或不太正式的表示.无论规范语言如何,它们都必须清晰严谨.非正式规范并非不可能正确构造,但在实际编程中通常存在缺陷.我们最终采用自动化和探索性测试等补救措施来弥补我们在非正式推理中遇到的问题.这并不是说测试本质上是一个坏主意,但引用的Twitter用户建议有更好的方法.

因此,我们的目标是拥有正确的程序,我们可以通过与机器实际执行程序的方式相对应的方式明确而严谨地进行推理.不过,这不是唯一的目标.我们也希望我们的逻辑具有一定程度的表达能力.例如,我们只能用命题逻辑表达这么多.从一阶逻辑中得到通用(∀)和存在(∃)量化是很好的.

使用类型系统进行推理

类型系统可以非常好地解决这些目标.由于库里 - 霍华德的对应,这一点尤为明显.这种对应关系通常用以下类比来表达:类型是程序,因为定理是证明.

这种对应有点深刻.我们可以采用逻辑表达式,并通过对应的类型转换它们.然后,如果我们有一个具有相同类型签名的程序,我们已经证明逻辑表达式是普遍正确的(重言式).这是因为通信是双向的.类型/程序与定理/证明世界之间的转换是机械的,并且在许多情况下可以是自动化的.

库里 - 霍华德很好地完成了我们想要对程序规范做的事情.

类型系统在Java中有用吗？

即使对Curry-Howard有所了解,有些人也会发现很容易忽略类型系统的价值

非常难以使用

对应(通过Curry-Howard)具有有限表现力的逻辑

被破坏了(它将系统的特征描述为"弱"或"强").

关于第一点,也许IDE可以使Java的类型系统足够容易使用(这是非常主观的).

关于第二点,Java碰巧几乎对应于一阶逻辑.泛型使用类型系统相当于通用量化.不幸的是,通配符只给我们一小部分存在量化.但普遍量化是一个很好的开端.很高兴能够List<A>为所有可能的列表普遍使用函数,因为A完全不受约束.这导致了Twitter用户在"参数化"方面所谈论的内容.

一篇经常被引用的关于参数化的论文是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没有no-arg构造函数会发生什么？在某些语言中,你得到的是null.或者你可能会跳过null值并直接引发异常(无论如何都会导致null值).因为我们的语言是图灵完整的,所以不可能推断哪些调用broken将涉及具有无参数构造函数的"安全"类型,哪些不会.我们已经失去了我们的计划普遍适用的确定性.

擦除意味着我们已经推理过(所以让我们擦除)

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

擦除鼓励推理.

_{(虽然我已经在这里写了一个答案,两年后重新审视这个问题,我意识到还有另一种完全不同的方式来回答它,所以我将完整的答案完整地保留下来并加上这个答案.)}

在Java Generics上完成的过程是否值得称之为"类型擦除",这是非常有争议的.由于通用类型没有被删除,而是被原始类型替换,更好的选择似乎是"类型残割".

在其通常理解的意义上,类型擦除的典型特征是迫使运行时通过使其对其访问的数据的结构"盲目"而保持在静态类型系统的边界内.这为编译器提供了全部功能,并允许它仅基于静态类型来证明定理.它还通过约束代码的自由度来帮助程序员,从而为简单推理提供更多功能.

Java的类型擦除没有达到这一点 - 它使编译器瘫痪,就像在这个例子中一样:

void doStuff(List<Integer> collection) { 
}

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

(上述两个声明在擦除后会折叠成相同的方法签名.)

另一方面,运行时仍然可以检查对象的类型并对其进行推理,但由于其对真实类型的洞察力因擦除而瘫痪,因此静态类型违规很难实现且难以防止.

为了使事情更复杂,原始和擦除类型签名共存并在编译期间并行考虑.这是因为整个过程不是从运行时删除类型信息,而是关于将泛型类型系统转换为传统原始类型系统以保持向后兼容性.这个宝石是一个经典的例子:

public static <T extends Object & Comparable<? super T>> T max(Collection<? extends T> coll)

(extends Object必须添加冗余以保留已擦除签名的向后兼容性.)

现在,考虑到这一点,让我们重温一下这句话:

当Java用户抱怨类型擦除时,这很有趣,这是Java唯一正确的选择

Java 究竟做了什么？这个词本身,无论含义如何？相比之下,请看一下简单的int类型:没有执行任何运行时类型检查,甚至可能执行,执行始终是完全类型安全的.这就是正确完成时类型擦除的样子:你甚至都不知道它就在那里.

我在这里看不到的一件事就是OOP的运行时多态性从根本上依赖于运行时类型的具体化.当一种语言的骨干由重新定义的类型保持到位时,它引入了类型系统的重大扩展并以类型擦除为基础,认知失调是不可避免的结果.这恰恰是Java社区发生的事情; 这就是为什么类型擦除已经吸引了如此多的争议,并最终为什么有计划在未来的Java版本中撤消它.在Java用户的抱怨中找到一些有趣的东西,可能会对Java的精神产生诚实的误解,或者有意识地贬低笑话.

声称"擦除是Java唯一正确的东西"意味着声称"所有基于动态调度的语言都违反了运行时类型的函数参数,从根本上说是有缺陷的".虽然它本身就是一个合法的主张,甚至可以被认为是对所有OOP语言(包括Java)的有效批评,但它不能作为评估和批评Java上下文中的特性的关键点,其中运行时多态性是公理的.

总而言之,虽然人们可以有效地说"类型擦除是语言设计的方式",但Java中支持类型擦除的位置是错误的,因为它已经太晚了,甚至在历史时刻已经如此当Oak被Sun拥抱并重命名为Java时.

至于静态类型本身是否是编程语言设计的正确方向,这适用于我们认为构成编程活动的更广泛的哲学背景.一个学派,显然源于古典数学传统,将程序视为一个数学概念或其他(命题,函数等)的实例,但是有一种完全不同的方法,它将编程视为一种方式与机器交谈并解释我们想要的东西.在这种观点中,该计划是一个充满活力,有机增长的实体,与静态打造的静态类型计划的戏剧性相反.

将动态语言看作是朝着这个方向迈出的一步似乎很自然:程序的一致性从下到上出现,没有先验的限制,这会以自上而下的方式强加它.这种范式可以被视为迈向我们人类通过发展和学习成为我们所处过程的过程的一步.

同一用户在同一对话中的后续帖子:

新T是一个破碎的程序.这与"所有命题都是真实的"主张是同构的.我对此并不陌生.

(这是对另一个用户的声明的回应,即"在某些情况下似乎'新的T'会更好",这个想法new T()因为类型擦除而不可能.(这是有争议的 - 即使T可以在运行时,它可能是一个抽象类或接口,或者它可能是Void,或者它可能缺少一个无参数构造函数,或者它的无参数构造函数可能是私有的(例如,因为它应该是一个单例类),或者它的no-arg构造函数可以指定泛型方法不捕获或指定的已检查异常 - 但这是前提.无论如何,如果没有擦除,您至少可以编写T.class.newInstance(),处理这些问题.))

这种类型与命题同构的观点表明,用户具有形式类型理论的背景.(S)他很可能不喜欢"动态类型"或"运行时类型",并且更喜欢没有向下转换instanceof和反射等的Java .(想想像Standard ML这样的语言,它有一个非常丰富的(静态)类型系统,其动态语义不依赖于任何类型的信息.)

顺便说一句,值得记住的是,用户正在拖钓:虽然他可能真诚地喜欢(静态)打字的语言,但他并没有真诚地试图说服其他人这种观点.更确切地说,原始推文的主要目的是嘲笑那些不同意的人,并且在其中一些不同意见之后,用户发布了后续推文,例如"java有类型擦除的原因是Wadler等人知道什么他们正在做,不像java的用户".不幸的是,这使得很难找出他实际在想的是什么; 但幸运的是,它也可能意味着这样做并不是很重要.对他们的观点有实际深度的人通常不会使用非常内容的巨魔.

一件好事是,在引入泛型时不需要更改JVM.Java仅在编译器级别实现泛型.

类型擦除是一件好事的原因是它使不可能的事情是有害的.防止在运行时检查类型参数使得对程序的理解和推理更容易.

我发现有些反直觉的观察是,当函数签名更通用时,它们变得更容易理解.这是因为减少了可能的实现的数量.考虑一个带有此签名的方法,我们知道它没有副作用:

public List<Integer> XXX(final List<Integer> l);

这个函数有哪些可能的实现？非常多.你可以很清楚地知道这个功能是做什么的.它可能会颠倒输入列表.它可能是将int整合在一起,将它们相加并返回一半大小的列表.还有许多其他可能的想法.现在考虑:

public <T> List<T> XXX(final List<T> l);

有多少这个功能的实现？由于实现无法知道元素的类型,一个巨大的实现方式的数目,现在可以排除:元素不能被组合,或添加到列表或过滤掉,等人.我们仅限于:身份(不更改列表),删除元素或撤消列表.此功能仅基于其签名更容易推理.

除了...在Java中你总是可以欺骗类型系统.正因为如此泛型方法的实现可以使用的东西像instanceof检查和/或石膏任意类型的基础上,类型签名我们的推理可以很容易地变得无用.该函数可以检查元素的类型,并根据结果执行任意数量的操作.如果允许这些运行时hacks,参数化方法签名对我们来说就变得不那么有用了.

如果Java没有类型擦除(即,类型参数在运行时被确定),那么这将简单地允许更多推理损害这种类型的恶作剧.在上面的例子中,如果列表至少有一个元素,则实现只能违反类型签名设置的期望; 但如果T被确定,即使清单是空的,也可以这样做.改进的类型只会增加(已经很多)阻碍我们理解代码的可能性.

类型擦除使语言不那么"强大".但某些形式的"权力"实际上是有害的.