haskell - GHC发生检查识别哪些情况？

Question

GHC 发生检查可防止您构造无限类型。它的目的是防止代码中的常见错误还是防止类型检查器无限循环，或两者兼而有之？
它识别了哪些情况，恶意用户是否有可能欺骗它(如在 Safe Haskell 上下文中)进入循环？如果类型系统是图灵完备的(是吗？)我不明白 GHC 如何保证计算会停止。

Answer 1

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

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]

所以我们得到一个方程a = [a] ，从中我们可以得出结论，该方程组没有解，因此代码类型不正确。如果我们没有拒绝方程 a = [a] ，我们确实会进入一个无限循环添加方程a = [a] , a = [[a]] , a = [[[a]]]等到我们的系统(或者，正如丹尼尔在他的回答中指出的那样，我们可以在我们的类型系统中允许无限类型，但这会使错误的程序(例如 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 通过具有固定深度的递归堆栈来确保终止，因此不可能构建一个永远不会停止的程序(根据 C.A.McCann 的评论， 编辑:，毕竟这是可能的 - 有类型级别的尾递归的类似物，允许在不增加堆栈深度的情况下循环)。

然而，有可能使编译花费任意长的时间，因为 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

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