haskell - Haskell 如何对无限递归值进行类型检查？

Question

定义此数据类型:

data NaturalNumber = Zero | S NaturalNumber
    deriving (Show)

在 Haskell(使用 GHC 编译)中，此代码将在没有警告或错误的情况下运行:

infinity = S infinity
inf1 = S inf2
inf2 = S inf1

因此，递归和相互递归的无限深值都通过了类型检查。

但是，下面的代码给出了错误:

j = S 'h'

错误状态无法将预期类型“NaturalNumber”与实际类型“Char”匹配。即使我设置了(相同的)错误仍然存​​在

j = S (S (S (S ... (S 'h')...)))

有大约一百个嵌套的 S。

Haskell 如何判断 infinity 是 NaturalNumber 的有效成员而 j 不是？

有趣的是，它还允许:

bottom = bottom
k = S bottom

Haskell 是否只是试图证明程序的不正确性，如果它没有这样做，那么就允许它？还是 Haskell 的类型系统不是图灵完备的，所以如果它允许程序，那么程序可证明(在类型级别)是正确的？

(如果类型系统(在 Haskell 的形式语义中，而不仅仅是类型检查器)是图灵完备的，那么它要么无法意识到一些正确类型的程序是正确的，要么是一些错误类型的程序是不正确的，由于停止问题的不可判定性。)

Answer 1

嗯

S :: NaturalNumber -> NaturalNumber

在

infinity = S infinity

我们首先不做任何假设:我们分配 infinity一些 Unresolved 类型_a并试图弄清楚它是什么。我们知道我们已经申请了S至infinity , 所以 _a必须是构造函数类型中箭头左侧的任何内容，即 NaturalNumber .我们知道 infinity是 S 应用程序的结果, 所以 infinity :: NaturalNumber , 再一次(如果这个定义有两个冲突的类型，我们就必须发出一个类型错误)。

类似的推理适用于相互递归的定义。 inf1必须是 NaturalNumber因为它作为 S 的参数出现在 inf2 ; inf2必须是 NaturalNumber因为它是 S 的结果;等等

一般算法是为定义分配未知类型(值得注意的异常(exception)是文字和构造函数)，然后通过查看每个定义的使用方式来为这些类型创建约束。例如。这必须是某种形式的列表，因为它是 reverse d，这必须是 Int因为它被用来从 IntMap 中查找值等。

如果是

oops = S 'a'

'a' :: Char因为它是一个字面量，但是，我们必须有 'a' :: NaturalNumber因为它被用作 S 的参数.我们得到一个明显虚假的约束，即文字的类型必须都是 Char和 NaturalNumber ，这会导致类型错误。

在

bottom = bottom

我们从 bottom :: _a 开始.唯一的约束是 _a ~ _a , 因为 _a 类型的值( bottom ) 用于 _a 类型的值预期(在 bottom 的定义的 RHS 上)。由于没有进一步限制类型， Unresolved 类型变量是泛化的:它被一个通用量词绑定(bind)以产生 bottom :: forall a. a .

注意 bottom 的两种用法以上具有相同的类型( _a )同时推断 bottom 的类型.这打破了多态递归:在其定义中每次出现的值都被认为与定义本身具有相同的类型。例如

-- perfectly balanced binary trees
data Binary a = Leaf a | Branch (Binary (a, a))
-- headB :: _a -> _r
headB (Leaf x) = x -- _a ~ Binary _r; headB :: Binary _r -> _r
headB (Branch bin) = fst (headB bin)
-- recursive call has type headB :: Binary _r -> _r
-- but bin :: Binary (_r, _r); mismatch

所以你需要一个类型签名:

headB :: {-forall a.-} Binary a -> a
headB (Leaf x) = x
headB (Branch bin) = fst (headB {-@(a, a)-} bin)
-- knowing exactly what headB's signature is allows for polymorphic recursion

所以:当某些东西没有类型签名时，类型检查器会尝试为它分配一个类型，如果它在途中遇到虚假约束，它会拒绝该程序。当某事物具有类型签名时，类型检查器会深入其中以确保它是正确的(尝试证明它是错误的，如果您更愿意这样想的话)。

Haskell 的类型系统不是图灵完备的，因为有严格的句法限制来防止例如输入 lambdas(没有语言扩展)，但不足以确保所有程序运行完成而没有错误，因为它仍然允许底部(更不用说所有不安全的函数)。它提供了较弱的保证，即如果程序在不使用不安全函数的情况下运行完成，它将保持类型正确。在 GHC 下，有了足够的语言扩展，类型系统确实变得图灵完备。我认为它不允许输入错误的程序通过；我认为你能做的最多就是让编译器陷入无限循环。