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的类型系统（在其正式语义中而不仅仅是类型检查器中）是图灵完备的，则由于停机问题的不可判定性，它将无法意识到某些正确类型化的程序是正确的或某些错误类型化的程序是不正确的。）

- H. User

---

你可能会对阅读 Hindley-Milner 类型推断感兴趣。 GHC 有一种双向类型检查形式。当看到 infinity 时，Haskell 将尝试合成 infinity :: NaturalNumber（因为它是使用 S :: NaturalNumber -> NaturalNumber 构造的），然后检查 infinity :: NaturalNumber（因为 infinity 是给定给 S 的参数）。 - Alec

好的 - 所以基本上它会以某种智能的方式猜测类型，然后尝试看看这些类型是否匹配？那么在正确的结果下，有没有终止（类型检查器）的任何保证呢？ - H. User

Answer 1

很好。

S :: NaturalNumber -> NaturalNumber

In

infinity = S infinity

我们从零开始：我们将无穷大赋予一些未解决的类型“_a”，并尝试找出它是什么。我们知道我们已经将“S”应用于“infinity”，所以“_a”必须是构造函数类型中箭头左侧的任何内容，即“NaturalNumber”。我们知道“infinity”是“S”的应用结果，因此“infinity :: NaturalNumber”，同样地（如果我们为此定义得到两个冲突的类型，则必须发出类型错误）。

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

一般算法是将定义的未知类型分配给它们（特别说明的例外是字面量和构造函数），然后通过查看如何使用每个定义来创建对这些类型的约束条件。例如，这必须是某种列表，因为它正在被“reverse”，这必须是一个“Int”，因为它正在被用来从“IntMap”中查找值，等等。

在这种情况下，

oops = S 'a'

'a' :: Char 是一个字面量，但是我们还需要 'a' :: NaturalNumber 因为它作为 S 的参数。这导致了一个明显的错误约束：字面量的类型既必须是 Char 又必须是 NaturalNumber，从而导致类型错误。

在...

bottom = bottom

我们从 bottom :: _a 开始。唯一的限制是 _a ~ _a，因为在定义 bottom 的 RHS 上期望一个类型为 _a 的值（bottom）被使用。由于没有进一步约束类型，未解决的类型变量被 泛化：它通过普遍量化被绑定，生成 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的类型系统不是图灵完备的，因为有严格的语法限制以防止例如类型lambda（没有语言扩展），但这并不足以确保所有程序都能无误地完成运行，因为它仍然允许底部（更不用说所有不安全的函数了）。它提供了一个较弱的保证，即如果一个程序在不使用不安全函数的情况下运行完成，它将保持类型正确。在GHC下，通过足够的语言扩展，类型系统确实变得图灵完备。我认为它不允许出现类型不正确的程序；最多只能使编译器陷入无限循环。

- HTNW

---

谢谢。这解释得很清楚，尤其是最后一段。 - H. User

我认为更准确的说法是类型检查器试图证明程序是良好类型化的。发现明显的错误是无法对程序进行类型化的特殊情况。 - dfeuer