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

Question

定义此数据类型：

data NaturalNumber = Zero | S NaturalNumber
    deriving (Show)

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

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

所以递归和相互递归的无限深值都通过了类型检查。

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

j = S 'h'

错误状态为Couldn't match expected type ‘NaturalNumber’ with actual type 'Char'。即使我设置了（相同的）错误仍然存​​在

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

有一百个左右嵌套的S's。

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

有趣的是，它还允许：

bottom = bottom
k = S bottom

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

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

Answer 1

嗯

S :: NaturalNumber -> NaturalNumber

在

infinity = S infinity

我们首先什么都不做假设：我们分配 infinity 一些未解决的类型 _a 并尝试找出它是什么。我们知道我们已经将S 应用于infinity，所以_a 必须是构造函数类型中箭头左侧的任何内容，即NaturalNumber。我们知道infinity 是S 的应用程序的结果，所以infinity :: NaturalNumber 再次出现（如果这个定义有两个冲突的类型，我们将不得不发出一个类型错误）。

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

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

如果是

oops = S 'a'

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

在

bottom = bottom

我们从bottom :: _a 开始。唯一的约束是_a ~ _a，因为在需要_a 类型的值的地方使用_a (bottom) 类型的值（在bottom 的定义的RHS 上）。由于没有进一步限制类型，未解决的类型变量是泛化的：它被一个通用量词绑定以产生bottom :: forall a. a。

请注意，在推断bottom 的类型时，上述bottom 的两种用法如何具有相同的类型（_a）。这打破了多态递归：在其定义中每次出现的值都被认为与定义本身具有相同的类型。例如

-- 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 下，有了足够的语言扩展，类型系统确实变得图灵完备。我认为它不允许输入错误的程序通过；我认为你能做的最多就是让编译器陷入无限循环。