c# - C# 类型系统是否可靠且可判定？

Question

我知道 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# 使用声明站点差异注释(使用 in 和 out 关键字)。众所周知，声明站点差异比使用站点差异弱(使用站点差异可以表达声明站点差异可以表达的所有内容，而且更多 - 在不利方面，它更加冗长)。

所以我的问题是:C# 类型系统是否合理且可判定？如果不是，为什么？

Answer 1

Is C# type system decidable?

如果编译器理论上总是能够在有限的时间内决定程序类型是否检查，则类型系统是“可判定的”。
C# 类型系统是不可判定的。
C# 有“名义”子类型——也就是说，当你声明一个类时，你给出类和接口(interface)的名称，并通过名称说明基类和接口(interface)是什么。
C# 也有泛型类型，从 C# 4 开始，泛型接口(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 ;一位研究人员注意到了那个帖子中提到的问题并解决了它；我们现在知道，如果混合中存在通用逆变，则名义子类型通常是不可判定的。您可以将图灵机编码到类型系统中并强制编译器模拟其操作，并且由于问题“此 TM 是否停止？”是不可判定的，所以类型检查必须是不可判定的。
见 https://arxiv.org/abs/1605.05274详情。

Is the C# type system sound?

如果我们保证在编译时进行类型检查的程序在运行时没有类型错误，那么类型系统就是“健全的”。
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 类型的等效值”。这些通常是安全的。)因为这是开发人员特别说明的地方他们比类型系统更了解，很难将导致的崩溃归咎于类型系统。

即使代码中没有强制转换，也有一些特性会生成类似强制转换的行为。例如，如果你有一个动物列表，你可以说

foreach(Giraffe g in animals)

如果里面有一只老虎，你的程序就会崩溃。正如规范所指出的，编译器只是代表您插入一个强制转换。 (如果你想遍历所有的长颈鹿而忽略老虎，那就是 foreach(Giraffe g in animals.OfType<Giraffe>()) 。)

unsafe C# 的子集让所有赌注都输了；你可以用它随意打破运行时的规则。关闭安全系统 关闭安全系统 ，所以当您关闭健全性检查时，C# 不健全也就不足为奇了。