问类型检查和类型系统的限制是什么？

EN

我认为第一个说法在技术上是错误的，尽管在实践中是正确的。

静态类型与证明程序的属性本质上是一样的，通过使用足够强大的逻辑，您可以证明所有有趣的程序都是正确的。

问题在于，对于强大的逻辑，类型推断不再有效，您必须在程序中提供证据，以便类型检查器能够完成其工作。一个具体的例子是像Coq这样的高阶证明器。Coq使用非常强大的逻辑，但是在Coq中完成任何事情也是非常繁琐的，因为您必须提供非常详细的证据。

给你带来最大麻烦的有趣的程序将是口译员，因为他们的行为完全取决于输入。本质上，您需要反思性地证明输入类型检查的正确性。

至于第二种说法，他可能指的是G dels不完备定理。它指出，对于任何给定的证明系统，都有在证明系统中无法证明的算术真语句(自然数的加法和乘法逻辑)。转换为静态类型系统，您将有一个程序不会做任何坏事，但静态类型系统不能证明这一点。

这些反例是通过引用证明系统的定义来构造的，从本质上说，“我不能被证明”被翻译成算术，这不是很有趣。IMHO，一个类似构造的程序也不会很有趣。

您可以用静态和动态语言表达一切。证明==，您可以用任何图灵完整语言编写任何语言编译器。因此，无论语言是什么，您都可以创建执行X的静态语言。

动态打字有什么有趣的？有了足够好的鸭子类型，您就可以在不知道对象类型的情况下通过网络与对象交互，并将它们的结果(您不知道的类型)作为参数传递给本地函数，这实际上可能会做一些有用的事情。

解决这个问题的静态方法是将所有内容都封装在“可导出接口”中，提供.call()和.provides?()来处理文本名称，但这肯定会更加困难。

这是我所知道的最“限制”的情况，它确实有点牵强(只对模拟对象非常有用？)。至于理论上的限制，没有-你只是需要一些额外的代码来克服实际问题。

一个有趣的例子是本篇论文，它可能是在静态和动态类型上所做的唯一的苹果对苹果之间的比较。他们使用类型推断(静态)和类型反馈(动态)实现了self (一种像smalltalk这样的语言，但是使用原型而不是类)。

最有趣的结果是，类型推理机在机器整数和任意精确整数之间有很大的困难--它们是在一般的self中自动提升的，因此类型系统无法将它们分开，这意味着编译器必须包括代码，以便在每个整数操作中提升到BigInt。

它们遇到了其类型系统的限制:它无法检查整数的实际值。

我认为在一般情况下，类型系统没有理论上的限制，但是任何给定的类型检查器都只能处理特定的、有限的类型系统，并且会有程序无法确定正在发生的事情。因为self类型推断器允许一组类型，所以它只是编译了这两条路径。需要在单个类型上收敛的类型检查器必须拒绝该程序。(尽管在这种情况下可能会有特殊的代码。)