C#型系统是否合理且可判定？

C#型系统是否可判定？

如果编译器在理论上始终能够在有限时间内确定程序类型是否检查,则类型系统是"可判定的".

这取决于您对类型系统的限制.一些C#类型系统的设计师有一篇关于这个主题的论文,你可能会觉得有趣:

https://www.microsoft.com/en-us/research/publication/on-decidability-of-nominal-subtyping-with-variance/

实际上,C#4.0和5.0编译器没有实现本文所述的无限型检测器; 相反,他们进入无限的递归和崩溃.

我考虑过将这样的代码添加到Roslyn但不记得这次是否进入; 我下周回到办公室时会查看源代码.

在我的文章中可以找到更温和的问题介绍:

http://blogs.msdn.com/b/ericlippert/archive/2008/05/07/covariance-and-contravariance-part-twelve-to-infinity-but-not-beyond.aspx

更新:安德鲁在原始论文中提出的问题 - 在一个具有名义子类型和逆变泛型的世界中的可兑换性检查通常是可判定的吗？ - 最近得到了答复.它不是.请参阅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#类型系统(尚未!)跟踪引用类型的无效性.如果您考虑将空引用异常作为一种运行时类型错误,那么C#非常不健全,因为它几乎不会阻止此类错误.可能会在C#8中完成这项工作,但这听起来并不合适.

许多强制转换表达式允许用户覆盖类型系统并声明"我知道这个表达式在运行时将是更具体的类型,如果我错了,抛出异常".(有些演员的意思相反:"我知道这个表达式是X型,请生成代码将其转换为类型Y的等价值."这些通常是安全的.)因为这是开发人员特别说的那个地方他们比类型系统知道得更好,人们很难责怪类型系统造成的崩溃.

即使代码中没有强制转换,也有一些特性可以生成类似强制转换的行为.例如,如果你有动物清单,你可以说

foreach(Giraffe g in animals)

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

unsafeC#的子集会关闭所有赌注; 你可以随意破坏运行时的规则.关闭安全系统会关闭安全系统,因此当您关闭健全性检查时,C#不会发出声音也就不足为奇了.