6

GHC 发生检查可防止您构造无限类型。它的目的是防止代码中的常见错误还是防止类型检查器无限循环，或两者兼而有之？

它识别了哪些情况，恶意用户是否有可能欺骗它（如在 Safe Haskell 上下文中）进入循环？如果类型系统是图灵完备的（是吗？）我不明白 GHC 如何保证计算会停止。

4

4 回答 4

10

将类型推断视为求解方程组。让我们看一个例子：

f x = (x,2)

我们如何推断 的类型f？我们看到它是一个函数：

f :: a -> b

此外，从 的结构中f我们可以看出，以下方程同时成立：

b = (c,d)
d = Int
c = a

通过求解这个方程组，我们可以看到 的类型f是a -> (a, Int)。现在让我们看看下面的（错误的）函数：

f x = x : x

的类型(:)是a -> [a] -> [a]，因此这会生成以下方程组（简化）：

a = a
a = [a]

所以我们得到一个 equation a = [a]，从中我们可以得出结论，这个方程组没有解，因此代码不是很好的类型。如果我们不拒绝 equation a = [a]，我们确实会进入一个无限循环，将 equations a = [a]、a = [[a]]、a = [[[a]]]等添加到我们的系统中（或者，正如 Daniel 在他的回答中指出的那样，我们可以在我们的类型系统中允许无限类型，但这会使错误的程序，例如f x = x : x类型检查）。

你也可以在 ghci 中测试：

> let f x = x : x

<interactive>:2:15:
    Occurs check: cannot construct the infinite type: a0 = [a0]
    In the second argument of `(:)', namely `x'
    In the expression: x : x
    In an equation for `f': f x = x : x

至于您的其他问题：GHC Haskell 的类型系统不是图灵完备的，并且类型检查器保证会停止 - 除非您启用UndecidableInstances，在这种情况下，它理论上可以进入无限循环。然而，GHC 通过具有固定深度的递归堆栈来确保终止，因此不可能构建一个它从不停止的程序（编辑：根据 CAMcCann 的评论，这毕竟是可能的 - 在允许在不增加堆栈深度的情况下循环的类型级别）。

然而，有可能使编译花费任意长的时间，因为 Hindley-Milner 类型推断的复杂性在最坏的情况下是指数级的（但不是平均！）：

dup x = (x,x)

bad = dup . dup . dup . dup . dup . dup . dup . dup
      . dup . dup . dup . dup . dup . dup . dup . dup
      . dup . dup . dup . dup . dup . dup . dup . dup
      . dup . dup . dup . dup . dup . dup . dup . dup

Safe Haskell 不会保护您免受这种情况的影响 -如果您想允许潜在的恶意用户在您的系统上编译 Haskell 程序，请查看mueval 。

于 2012-09-19T13:43:18.833 回答
8

GHC 发生检查可防止您构造无限类型。

这仅在字面意义上是正确的，即防止语法上无限的类型。这里真正发生的只是一种递归类型，在某种意义上，统一算法需要内联递归。

总是可以通过显式递归来定义完全相同的类型。这甚至可以通用地完成，使用类型级别的版本fix：

newtype Fix f = Fix (f (Fix f))

例如，类型Fix ((->) a)等同于与b统一(a -> b)。

然而，在实践中，“无限类型”错误几乎总是表明代码中有错误（所以如果它坏了，你可能不应该这样Fix做）。通常的情况是混淆了参数顺序，或者在不使用显式类型签名的代码中将表达式放在错误的位置。

以正确方式极其幼稚的类型推断系统可能会扩展递归，直到内存不足，但不会出现停止问题——如果类型需要与自身的一部分统一，那永远不会发生工作（至少在 Haskell 中，可能有一些语言将其视为等同于newtype上面的显式递归）。

除非您启用，否则 GHC 中的类型检查和类型推断都不是图灵完备的UndecidableInstances，在这种情况下，您可以通过函数依赖项或类型族进行任意计算。

Safe Haskell 并没有真正参与进来。UndecidableInstances很容易生成非常大的推断类型，尽管它是有限的，但会耗尽系统内存，如果内存为我服务，Safe Haskell无论如何都不会限制使用。

于 2012-09-19T14:04:50.607 回答
7

我的书签中有以下精彩邮件：无限类型没有错！即使有无限类型，也没有使类型检查器循环的真正危险。类型系统不是图灵完备的（除非您明确要求它与UndecidableInstances扩展类似）。

于 2012-09-19T13:36:21.663 回答
4

目的（在 Haskell 编译器中）是为了防止代码中的常见错误。可以构建一个类型检查器和推理引擎来支持类型的无限递归。这个问题有一些进一步的信息。

OCaml 使用 实现递归类型-rectypes，所以这绝对是可能的。OCaml 社区将更加精通出现的一些问题（默认情况下该行为是关闭的）。

发生检查识别无限类型扩展。例如，这段代码：

Prelude> let a = [a]
<interactive>:2:10:
    Occurs check: cannot construct the infinite type: t0 = [t0]
    In the expression: a
    In the expression: [a]
    In an equation for `a': a = [a]

如果您尝试手动计算类型，则类型为[ [ [ [ ... ] ] ] ]. 手动编写这样的类型是不可能的，因为它们是无限的。

发生检查发生在类型推断期间，这是与类型检查分开的阶段。必须推断无限类型，因为它们不能手动注释。Haskell-98 类型推断是可判定的，因此不可能欺骗编译器进入循环（当然排除错误，我怀疑这个示例利用了这些错误）。GHC 默认使用 System F 的受限子集，其类型推断也是可判定的。对于某些扩展，例如RankNTypes，GHC 确实允许类型推断无法确定的代码，但随后需要类型注释，因此再次没有类型推断阶段循环的危险。

由于图灵完备的语言是不可判定的，所以默认类型系统不可能是图灵完备的。我不知道 GHC 的类型系统是否在启用某些扩展组合的情况下成为图灵完备的，但某些扩展（例如UndecidableInstances）允许编写会因堆栈溢出而使编译器崩溃的代码。

顺便说一句，禁用发生检查的主要问题是许多常见的编码错误会导致无限的类型错误，因此禁用它通常会导致比它解决的问题更多的问题。如果您确实打算使用无限类型，则 newtype 包装器将允许它，而无需过多的符号。

于 2012-09-19T14:58:36.117 回答