类型系统经常被批评为限制性的，即限制编程语言并禁止程序员编写有趣的程序。
克里斯·史密斯claims:
We get assurance that the program is correct (in the properties checked by this type checker), but in turn we must reject some interesting programs.
和
Furthermore, there is an ironclad mathematical proof that a type checker of any interest at all is always conservative. Building a type checker that doesn't reject any correct programs isn't just difficult; it's impossible.
有人可以概述一下这可能是什么有趣的程序吗？在哪里证明类型检查器必须保守？
更笼统:类型检查和类型系统的限制是什么？
最佳答案
我认为第一个陈述在技术上是错误的，尽管实际上是正确的。
静态类型本质上与证明程序的属性相同，并且通过使用足够强大的逻辑，您可以证明所有有趣的程序都是正确的。
问题在于，对于强大的逻辑而言，类型推断不再起作用，您必须在程序中提供证明，以便类型检查器可以执行其工作。一个具体的例子是高阶证明，例如Coq。 Coq使用非常强大的逻辑，但是用Coq完成任何事情也非常繁琐，因为您必须提供详细的证明。
会给您带来最大麻烦的有趣程序是解释器，因为它们的行为完全取决于输入。本质上，您将需要反射(reflection)性地证明该输入的类型检查的正确性。
至于第二种说法，他可能是指哥德尔斯不完全性定理。它指出，对于任何给定的证明系统，都有无法在证明系统中证明的真实的算术陈述(自然数的加法和乘法逻辑)。转换为静态类型系统后，您将拥有一个不会做任何坏事的程序，但静态类型系统无法证明这一点。
这些反例是通过引用证明系统的定义而构造的，基本上说“我无法证明”被翻译成算术，这不是很有趣。恕我直言，类似构造的程序也不会很有趣。
关于types - 类型检查和类型系统的限制是什么？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/1251791/