什么情况下会发生GHC检查识别？

Question

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

它识别了什么情况，恶意用户有可能欺骗它(就像在安全的Haskell上下文中一样)进入循环吗？如果类型系统是Turing-complete (是吗？)我不明白GHC怎么能保证计算会停止。

Answer 1

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

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

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

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

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

然而，在实践中，"infinite type“错误几乎总是指示代码中的错误(因此，如果代码损坏，您可能不应该对其执行Fix操作)。通常的情况是混淆参数顺序，或者在不使用显式类型签名的代码中将表达式放在错误的位置。

一个以正确方式极其幼稚的类型推断系统可能会扩展递归，直到它耗尽内存，但是停止问题并没有进入其中--如果一个类型需要与其自身的一部分相统一，那么这永远不会起作用(至少在Haskell中，可能有一些语言将其视为与上面的显式递归newtype等价)。

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

Safe Haskell并没有真正进入这幅图景。很容易生成非常大的推断类型，即使是有限的，也会耗尽系统内存，而且如果内存足够安全，Haskell无论如何都不会限制UndecidableInstances的使用。

Answer 2

我的书签里有下面这封很棒的邮件：There's nothing wrong with infinite types!即使有无限类型，也不会有造成类型检查器循环的真正危险。类型系统不是图灵完整的(除非您显式地要求它使用像UndecidableInstances扩展这样的东西)。

Answer 3

目的(在Haskell编译器中)是为了防止代码中的常见错误。可以构造一个类型检查器和推理引擎，它将支持类型的无限递归。在this question上有更多的信息。

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类型推断是decidable的，所以不可能欺骗编译器进入循环(当然，排除bug，我怀疑this example利用了bug)。默认情况下，GHC使用系统F的受限子集，对于该子集，类型推断也是可确定的。对于某些扩展，例如RankNTypes，GHC确实允许类型推断不可确定的代码，但随后需要类型注释，因此类型推断阶段循环的危险也不存在。

由于图灵完全语言是不可确定的，因此默认类型系统不能是图灵完整。我不知道GHC的类型系统是否在启用了某种扩展组合的情况下变得图灵完整，但是某些扩展(例如UndecidableInstances)允许编写会导致编译器崩溃的堆栈溢出代码。

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