C＃类型系统是否合理？ [英] Is C# type system sound and decidable?

问题描述

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

I know that Java's type system is unsound (it fails to type check constructs that are semantically legal) and undecidable (it fails to type check some construct).

例如，如果您将以下代码段复制/粘贴到类中并对其进行编译，则编译器将崩溃，并出现 StackOverflowException （如此）的情况。

For instance, if you copy/paste the following snippet in a class and compile it, the compiler will crash with a StackOverflowException (how apt). This is undecidability.

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 关键字）。众所周知，声明站点方差要弱于使用站点方差（使用站点方差可以表示声明站点方差可以表达的所有信息，并且在更多方面，更糟糕的是，）。

Java uses wildcards with type bounds, which are a form of use-site variance. C# on the other hand, uses declaration site variance annotation (with the in and out keywords). It is known that declaration-site variance is weaker than use-site variance (use-site variance can express everything declaration-site variance can, and more -- on the down side, it's much more verbose).

所以我的问题是：C＃类型系统是否合理？如果不是，为什么？

So my question is: Is C# type system sound and decidable? If not, why?

推荐答案

C＃类型系统是否可确定？

Is C# type system decidable?

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

A type system is "decidable" if the compiler is in theory always able to decide whether the program type checks or not in finite time.

C＃类型系统不可确定。

C＃具有标称子类型化-即，给类和接口名称，并在声明类时说出基类和接口的名称​​ 。

C# has "nominal" subtyping -- that is, you give classes and interfaces names and say what the base classes and interfaces are by name when you declare a class.

C＃也具有泛型类型，并且从C＃开始，具有泛型接口的协方差和协变。

C# also has generic types, and, as of C# 4, covariance and contravariance of generic interfaces.

这三件事-名义子类型化，泛型接口和协变-足以使类型系统变得不可预测（在对子类型彼此提及的方式没有其他限制的情况下。）

Those three things -- nominal subtyping, generic interfaces, and contravariance -- are sufficient to make a type system undecidable (in the absence of other restrictions on the ways that subtypes may mention each other.)

此答案最初于2014年撰写时，有人怀疑但未知。这个发现的历史很有趣。

When this answer was originally written in 2014, that was suspected but not known. The history of this discovery is interesting.

首先，C＃泛型类型系统的设计师想知道同一件事，并在2007年写了一篇论文，描述了类型检查可能出错的不同方式。 ，以及可以对可判定的名义子类型系统施加哪些限制。

First, the designers of the C# generic type system wondered the same thing, and wrote a paper in 2007 describing different ways in which type checking can go wrong, and what restrictions one can put on a nominal subtyping system that make it decidable.

> https://www.microsoft.com/zh-cn/research/publication/on-decidability-of-nominal-subtyping- with-variance /

可以在我的博客上找到关于该问题的更为温和的介绍，

A more gentle introduction to the problem can be found on my blog, here:

https://ericlippert.com/ 2008/05/07 / covariance-and-contravariance-part-11-to-infinity-but-not-beyond /

我之前曾在SE网站上撰写过有关此主题的文章；研究人员注意到帖子中提到的问题并解决了；我们现在知道，如果将通用的协方差放入组合中，则通常无法确定名义子类型化。您可以将Turing Machine编码为类型系统，并强制编译器模拟其操作，并且由于问题此TM是否停止？是不可确定的，因此类型检查必须不可确定。

I have written about this subject on SE sites before; a researcher noticed the problem mentioned in that posting and solved it; we now know that nominal subtyping is in general undecidable if there is generic contravariance thrown into the mix. You can encode a Turing Machine into the type system and force the compiler to emulate its operation, and since the question "does this TM halt?" is undecidable, so must type checking be undecidable.

请参见 https：// arxiv有关详细信息，请参见.org / abs / 1605.05274 。

C＃类型的系统声音吗？

Is the C# type system sound?

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

A type system is "sound" if we are guaranteed that a program which type checks at compile time has no type errors at runtime.

C＃类型系统不健全。

有很多原因，但我最不喜欢的是数组协方差：

There are many reasons why it is not, but my least favourite is array covariance:

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允许它。结果是每次将任何内容写入基类的数组时，运行时都必须进行检查以确认该数组不是不兼容的派生类的数组。普通情况会变慢，以便罕见的错误情况会出现异常。

The idea here is that most methods that takes arrays only read the array, they do not write it, and it is safe to read an animal out of an array of giraffes. Java allows this, and so the CLR allows it because the CLR designers wanted to be able to implement variations on Java. C# allows it because the CLR allows it. The consequence is that every time you write anything into an array of a base class, the runtime must do a check to verify that the array is not an array of an incompatible derived class. The common case gets slower so that the rare error case can get an exception.

这带来了一个好处：C＃至少对类型错误的后果有明确的定义。 。运行时的类型错误会以异常形式产生理智的行为。不像C或C ++那样，编译器可以并且会灵活地生成执行任意疯狂事情的​​代码。

That brings up a good point though: C# is at least well-defined as to the consequences of a type error. Type errors at runtime produce sane behaviour in the form of exceptions. It's not like C or C++ where the compiler can and will blithely generate code that does arbitrarily crazy things.

还有其他一些方法可以使C＃类型系统在设计上不合理。

There are a few other ways in which the C# type system is unsound by design.

• 如果您认为获取空引用异常是一种运行时类型错误，则C＃pre C＃8非常不完善，因为它几乎可以没有什么可以防止这种错误。 C＃8在支持静态检测空错误方面有很多改进，但是空引用类型检查并不完善。它既有误报也有误报。这个想法是，即使不是100％可靠的，某些编译时检查总比没有好。

• If you consider getting a null reference exception to be a kind of runtime type error, then C# pre C# 8 is very unsound in that it does almost nothing to prevent this kind of error. C# 8 has many improvements in support for detecting nullity errors statically, but the null reference type checking is not sound; it has both false positives and false negatives. The idea is that some compile-time checking is better than none, even if it is not 100% reliable.

许多强制转换表达式允许用户覆盖类型系统并声明我知道该表达式在运行时将是更特定的类型，如果我错了，则抛出异常。 （某些强制转换的意思相反：我知道此表达式的类型为X，请生成代码以将其转换为类型Y的等效值。通常是安全的。）因为这是开发人员专门说的地方他们比类型系统更了解，所以几乎不应该将导致崩溃的原因归咎于类型系统。

Many cast expressions allow the user to override the type system and declare "I know this expression will be of a more specific type at runtime, and if I'm wrong, throw an exception". (Some casts mean the opposite: "I know this expression is of type X, please generate code to convert it to an equivalent value of type Y". Those are generally safe.) Since this is a place where the developer is specifically saying that they know better than the type system, one can hardly blame the type system for the resulting crash.

有即使代码中没有强制转换，也有少数功能会产生类似强制转换的行为。例如，如果您有动物列表，则可以说

There are also a handful of features that generate cast-like behaviour even though there is no cast in the code. For example, if you have a list of animals you can say

foreach(Giraffe g in animals)

，如果那里有老虎，您的程序将崩溃。如规范所述，编译器只是代表您插入一个强制类型转换。 （如果您要遍历所有长颈鹿而忽略老虎，则 foreach（动物中的长颈鹿g.OfType<< Giraffe>（））。）

and if there is a tiger in there, your program will crash. As the specification notes, the compiler simply inserts a cast on your behalf. (If you want to loop over all the giraffes and ignore the tigers, that's foreach(Giraffe g in animals.OfType<Giraffe>()).)

• C＃的不安全子集使所有赌注无效；您可以使用它任意违反运行时规则。关闭安全系统会关闭安全系统，因此在关闭健全性检查时C＃不发声也就不足为奇了。

• The unsafe subset of C# makes all bets off; you can break the rules of the runtime arbitrarily with it. Turning off a safety system turns a safety system off, so it should not be surprising that C# is not sound when you turn off soundness checking.

这篇关于C＃类型系统是否合理？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！