C# 类型系统是否健全且可判定？

Question

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

例如，如果您将以下 sn-p 复制/粘贴到一个类中并对其进行编译，编译器将崩溃并显示 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

C# 类型系统是可判定的吗？

如果编译器在理论上总是能够决定程序类型是否在有限时间内检查，则类型系统是“可确定的”。

C# 类型系统不可判定。

C# 有“名义”子类型——也就是说，当你声明一个类时，你给类和接口名称，并说明基类和接口是什么按名称 .

C# 还具有泛型类型，并且从 C# 4 开始，具有泛型接口的协变和逆变。

这三样东西——名义子类型、泛型接口和逆变——足以使类型系统不可判定（在子类型可能相互提及的方式上没有其他限制的情况下。）

当这个答案最初是在 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。

C#类型的系统好听吗？

如果我们保证在编译时进行类型检查的程序在运行时没有类型错误，则类型系统是“健全的”。

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>())。）

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

Answer 2

创建 C# 编译器无法在合理的时间内解决的问题并不是特别难。它提出的一些问题（通常与泛型/类型推断有关）是 NP-hard 问题。埃里克·利珀特describes one such example here:

class MainClass
{
    class T{}
    class F{}
    delegate void DT(T t);
    delegate void DF(F f);
    static void M(DT dt)
    {
        System.Console.WriteLine("true");
        dt(new T());
    }
    static void M(DF df)
    {
        System.Console.WriteLine("false");
        df(new F());
    }
    static T Or(T a1, T a2, T a3){return new T();}
    static T Or(T a1, T a2, F a3){return new T();}
    static T Or(T a1, F a2, T a3){return new T();}
    static T Or(T a1, F a2, F a3){return new T();}
    static T Or(F a1, T a2, T a3){return new T();}
    static T Or(F a1, T a2, F a3){return new T();}
    static T Or(F a1, F a2, T a3){return new T();}
    static F Or(F a1, F a2, F a3){return new F();}
    static T And(T a1, T a2){return new T();}
    static F And(T a1, F a2){return new F();}
    static F And(F a1, T a2){return new F();}
    static F And(F a1, F a2){return new F();}
    static F Not(T a){return new F();}
    static T Not(F a){return new T();}
    static void MustBeT(T t){}
    static void Main()
    {
        // Introduce enough variables and then encode any Boolean predicate:
        // eg, here we encode (!x3) & ((!x1) & ((x1 | x2 | x1) & (x2 | x3 | x2)))
        M(x1=>M(x2=>M(x3=>MustBeT(
          And(
            Not(x3), 
            And(
              Not(x1), 
              And(
                Or(x1, x2, x1), 
                Or(x2, x3, x2))))))));
    }
}

Answer 3

@Eric-Lippert 的回答当然是权威的。我想强调的是，上面的方差问题仅适用于数组。

使用泛型时它会消失，因为那时您只能拥有 Co-、Contra- 或 In-Variance。这不允许以下应用程序之一：成员分配、成员查询或集合分配：

InVariance 不允许集合分配：

IList<Giraffe> giraffes3 = new List<Giraffe>{new()};
IList<Animal> animals3 = giraffes3; // ! does NOT compile!

协方差不允许成员分配：

IReadOnlyList<Giraffe> giraffes1 = new List<Giraffe>{new()};
IReadOnlyList<Animal> animals1 = giraffes1; // This is legal!
animals1[0] = new Tiger(); // ! does NOT compile!

Contra-Variance 不允许传递其他子类型：

IObserver<Animal> animals2 = new MyObserver<Animal>(); 
IObserver<Giraffe> giraffes2 = animals2; // This is legal!
giraffes2.OnNext(new Giraffe());
animals2.OnNext(new Tiger());
giraffes2.OnNext(new Tiger()); // ! does NOT compile!

Full Variance 允许一切，但在运行时失败（这是最糟糕的）：

Giraffe[] giraffes = {new()};
Animal[] animals = giraffes; // This is legal!
animals[0] = new Tiger(); // ! Runtime Exception !

只要您尽量避免在 API 中使用数组并仅在内部使用它们，例如就性能而言，你应该很好。