Ada*_*ark 6 haskell typechecking ghc
GHC发生检查阻止您构建无限类型.它的目的是防止代码中的常见错误或防止类型检查程序无限循环,或两者兼而有之？
它识别的是什么情况,恶意用户是否有可能欺骗它(如在安全Haskell上下文中)进入循环？如果类型系统是图灵完成的(是吗？)我不明白GHC如何保证计算停止.
Mik*_*kov 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]
因此,我们得到一个等式a = [a],从中我们可以得出结论,这个方程组没有解,因此代码没有很好的类型.如果我们不拒绝公式a = [a],我们的确会去一个无限循环增加的方程a = [a],a = [[a]],a = [[[a]]],等我们的系统(或者,如丹尼尔在他的回答指出,我们可以让我们的类型系统的无限远类型,但是这将使错误的程序,如f x = x : xtypecheck).
你也可以在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的类型系统不是Turing-complete而且typechecker保证停止 - 除非你启用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
安全Haskell不会保护您免受这种情况的影响 - 如果您希望允许潜在恶意用户在您的系统上编译Haskell程序,请查看mueval.
GHC发生检查阻止您构建无限类型.
这只是在字面意义上预防句法上无限的类型.这里真正发生的只是一种递归类型,统一算法在某种意义上需要内联递归.
通过使递归显式化,始终可以定义完全相同的类型.这通常可以使用以下类型级别的版本来完成fix:
newtype Fix f = Fix (f (Fix f))
作为一个例子,该类型Fix ((->) a)是相当于统一b用(a -> b).
然而,在实践中,"无限类型"错误几乎总是表示代码中的错误(因此如果它被破坏,你可能不应该Fix这样).通常的情况是混合参数顺序或在不使用显式类型签名的代码中将表达式放在错误的位置.
以正确的方式非常幼稚的类型推理系统可能会扩展递归直到内存耗尽,但停止问题不会进入它 - 如果一个类型需要与其自身的一部分统一,那就永远不会工作(至少在Haskell中,可能有一些语言将其视为等同于newtype上面的显式递归).
GHC中的类型检查和类型推断都不是Turing-complete,除非你启用UndecidableInstances,在这种情况下你可以通过功能依赖或类型族进行任意计算.
安全Haskell根本没有真正进入画面.很容易生成非常大的推断类型,尽管有限,但会耗尽系统内存,如果内存为我服务,那么Safe Haskell并不会限制使用UndecidableInstances.