我知道Java的类型系统是不健全的(它不能对从语义上合法的检查结构进行类型化)并且是不确定的(它不能对某些结构进行类型检查)。

例如,如果您将以下代码段复制/粘贴到类中并对其进行编译,则编译器将使用StackOverflowException(如何适配)崩溃。这是不确定的。

static class ListX<T> {}
static class C<P> extends ListX<ListX<? super C<C<P>>>> {}
ListX<? super C<Byte>> crash = new C<Byte>();

Java使用带类型限制的通配符,这是使用站点差异的一种形式。另一方面,C#使用声明站点差异注解(带有inout关键字)。众所周知,声明站点方差比使用站点方差弱(使用站点方差可以表示声明站点方差可以表达的所有信息,并且在更多方面-更为复杂)。

所以我的问题是:C#类型系统是否合理?如果没有,为什么?

最佳答案


如果编译器理论上总是能够确定程序类型是否在有限时间内进行检查,则类型系统是“可确定的”。
C#类型系统不可确定。
C#具有“标称”子类型-即,给类和接口(interface)命名,并在声明类时说出基类和接口(interface)的名称。
C#也具有泛型,从C#开始,C#具有泛型接口(interface)的协方差和协变。
这三件事-名义子类型化,通用接口(interface)和矛盾-足以使类型系统变得不确定(在对子类型彼此提及的方式没有其他限制的情况下)。
最初在2014年撰写此答案时,这是令人怀疑但未知的。这一发现的历史很有趣。
首先,C#泛型类型系统的设计者想知道同样的事情,并在2007年写了一篇论文,描述了类型检查可能出错的不同方式,以及可以对可判定的名义子类型系统施加哪些限制。
https://www.microsoft.com/en-us/research/publication/on-decidability-of-nominal-subtyping-with-variance/
可以在我的博客中找到关于该问题的更温和的介绍:
https://ericlippert.com/2008/05/07/covariance-and-contravariance-part-11-to-infinity-but-not-beyond/
I have written about this subject on SE sites before;研究人员注意到帖子中提到的问题并解决了;我们现在知道,如果将通用的协方差放入组合中,则通常无法确定名义子类型化。您可以将Turing Machine编码到类型系统中,并强制编译器模拟其操作,并且由于问题“此TM是否停止?”。是不可确定的,因此类型检查必须不可确定。
有关详细信息,请参见https://arxiv.org/abs/1605.05274

如果我们保证在编译时进行类型检查的程序在运行时没有类型错误,则类型系统是“健全的”。
C#类型系统不健全。
并非如此的原因很多,但我最不喜欢的是数组协方差:

Giraffe[] giraffes = new[] { new Giraffe() };
Animal[] animals = giraffes; // This is legal!
animals[0] = new Tiger(); // crashes at runtime with a type error
这里的想法是,大多数采用数组的方法只能读取数组,而不能写入数组,并且从长颈鹿数组中读取动物是安全的。 Java允许这样做,所以CLR允许这样做,因为CLR设计人员希望能够在Java上实现变体。 C#允许它,因为CLR允许它。结果是,每当您向基类的数组中写入任何内容时,运行时都必须进行检查以确认该数组不是不兼容的派生类的数组。常见情况变慢,因此罕见错误情况可能会发生异常。
但是,这带来了一个好处:C#对于类型错误的后果至少是定义明确的。运行时的类型错误会以异常形式产生理智的行为。它不像C或C++那样,编译器可以并且会巧妙地生成执行任意疯狂事情的​​代码。
还有其他几种方法可以使C#类型系统在设计上不健全。
  • 如果您认为获取空引用异常是一种运行时类型错误,则C#pre C#8非常不完善,因为它几乎无法防止此类错误。 C#8在支持静态检测空错误方面有很多改进,但是空引用类型检查并不完善。它既有误报也有误报。这个想法是,即使不是100%可靠的,某些编译时检查总比没有好。
  • 许多强制转换表达式允许用户重写类型系统,并声明“我知道此表达式在运行时将具有更特定的类型,如果我错了,则抛出异常”。 (某些强制转换的含义相反:“我知道此表达式的类型为X,请生成代码以将其转换为类型Y的等效值。”这些通常是安全的。)因为这是开发人员专门说的地方他们比类型系统更了解,几乎无法将导致崩溃的原因归咎于类型系统。

  • 即使代码中没有强制转换,也有少数功能会产生类似强制转换的行为。例如,如果您有动物 list ,您可以说
    foreach(Giraffe g in animals)
    
    并且如果那里有老虎,您的程序将崩溃。如规范所述,编译器只是代表您插入一个强制类型转换。 (如果您想遍历所有的长颈鹿而忽略老虎,那就是foreach(Giraffe g in animals.OfType<Giraffe>())。)
  • C#的unsafe子集使所有赌注无效。您可以使用它任意违反运行时规则。关闭安全系统会关闭安全系统,因此在关闭健全性检查时不会发出C#并不奇怪。
  • 08-04 13:51