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

Question

类型系统经常受到批评,因为它是限制性的,即限制编程语言并禁止程序员编写有趣的程序.

Chris Smith 声称:

我们确保程序是正确的(在这种类型检查器检查的属性中),但反过来我们必须拒绝一些有趣的程序.

和

此外,还有一个铁定的数学证明,任何利益的类型检查器总是保守的.构建一个不拒绝任何正确程序的类型检查器并不困难; 不可能.

有人可以概述一下这可能是什么样的有趣程序吗？哪里证明类型检查器必须保守？

更一般:类型检查和类型系统的限制是什么？

Answer 1

我认为第一个陈述在技术上是错误的,尽管在实践中是正确的.

静态类型与证明程序属性基本相同,并且通过使用足够强大的逻辑,您可以证明所有有趣的程序都是正确的.

问题是,对于强大的逻辑类型推断不再有效,并且您必须提供证明作为程序的一部分,以便类型检查器可以完成其工作.一个具体的例子是更高阶的证明,例如Coq.Coq使用了非常强大的逻辑,但是在Coq中完成任何事情也非常繁琐,因为你必须提供非常详细的证明.

那些给你带来最多麻烦的有趣程序将是解释器,因为它们的行为完全取决于输入.基本上,您需要反思地证明该输入的类型检查的正确性.

至于第二个陈述,他可能指的是Gödels不完备性定理.它指出,对于任何给定的证明系统,都存在无法在证明系统中证明的算术的真实陈述(自然数的加法和乘法的逻辑).转换为静态类型系统你会有一个程序没有做任何坏事,但静态类型系统无法证明这一点.

这些反例是通过回顾证明系统的定义来构建的,基本上说"我不能被证明"被翻译成算术,这不是很有趣.恕我直言,类似地构建的程序也不会有趣.

Answer 2

您可以用静态和动态语言表达所有内容.证明==您可以用任何图灵完整语言编写任何语言编译器.因此无论语言是什么,您都可以创建执行X的静态语言.

动态类型有什么好处？...有足够好的鸭子打字,你可以通过网络与对象进行交互,而不知道他们的类型,并将结果(你不知道的类型)作为参数传递给本地函数,这可能实际上是有用的东西.

这个问题的静态答案是将所有内容包装在"可导出的接口"中,提供.call()和.provides？()处理文本名称,但这肯定会更难.

这是我所知道的最"限制"的情况,它实际上是在拉伸一些东西(只对模拟对象有用吗？).至于理论上的限制,没有 - 你只需要一些额外的代码来克服实际问题.

Answer 3

一个有趣的例子是本文,这可能是有史以来在静态与动态类型上所做的唯一比较.他们使用类型推断(静态)和类型反馈(动态)实现self(像smalltalk这样的语言,但使用原型而不是类).

最有趣的结果是类型推理引擎在机器整数和任意精度整数之间解决时遇到很多麻烦 - 它们在vanilla self中自动升级,因此不能被类型系统分开,这意味着编译器必须包含代码以在每个整数操作上提升BigInt.

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

我认为一般来说系统类型没有理论限制,但任何给定的类型检查器只能处理特定的有限类型系统,并且会有程序无法确定发生了什么.由于自我类型推断器允许类型集合,因此它只编译了两个路径.需要在单一类型上收敛的类型检查器必须拒绝该程序.(虽然它可能有这个案例的特殊代码.)

Answer 4

我认为这其中存在误会。确实，任何类型系统都会拒绝正确的程序（我不记得结果的确切名称，所以我现在无法查找它，抱歉）。同时，任何图灵完备语言都可以做与任何其他语言相同的事情，因此说有些动态类型语言中的程序无法重现（例如用 Haskell 语言）是错误的。

问题是，类型系统拒绝某个程序并不意味着它会拒绝所有与其等效的程序。因此，某些程序将被拒绝，但您可以用其他等效的程序替换它们。以下面的 Scala 程序为例

def foo: Int =
  if (1 > 0) 15 else "never happens"

类型检查器将拒绝它，因为表达式的形式if (1 > 0) 15 else "never happens"形式为 类型Any。当你运行它时，它肯定会返回一个整数，但如果不进行评估，1 > 0你无法确定它不会返回一个字符串。你可以用Python编写

def foo():
  if 1 > 0:
    return 15
  else:
    return "never happens"

Python 编译器不会关心。

当然，您可以用 Scala 编写与此等效的程序，最简单的是

def foo: Int = 15

Answer 5

人们发现，如果您首先以真正的 TDD 方式编写测试，那么您的测试通常比严格的类型检查系统在验证正确性方面做得更好。因此，对于衡量正确性来说，强类型系统并不能真正满足要求。

强类型通常可以为您带来一些速度，因为编译器可以轻松使用本机类型，而不必在运行时进行类型检查。举个例子：如果您正在进行大量整数数学运算，您会发现强类型实现可能会比弱类型实现运行得更快，因为您的数字通常可以立即被 CPU 使用，而不必在运行时验证。

“有趣”的节目？当然。用动态语言编写扩展会更容易。此外，在分布式系统中，拥有弱类型 UI 并且不必生成特定的数据传输对象确实很方便。例如，如果您有一个 JavaScript 前端和一个 C# 后端，则可以在 C# 端使用 LINQ 生成匿名类，并通过 JSON 将它们发送到您的 Javascript。从 JS 层，您可以像使用一流对象一样使用这些匿名类型，而不必经历显式编码所有数据契约的痛苦。