推断类型似乎检测到无限循环，但到底发生了什么？

Question

在 Andrew Koenig 的 An anecdote about ML type inference 中，作者使用 merge sort 的实现作为 ML 的学习练习，很高兴发现“不正确”的类型推断。

令我惊讶的是，编译器报告了一种

'a list -> int list

换句话说，这个排序函数接受任何类型的列表并返回一个整数列表。

那是不可能的。输出必须是输入的排列；它怎么可能有不同的类型？读者肯定会发现我的第一个冲动很熟悉：我想知道我是否在编译器中发现了一个错误！

再想一想之后，我意识到还有另一种方法可以让函数忽略它的参数：也许它有时根本不返回。事实上，当我尝试它时，确实发生了这样的事情：sort(nil) 确实返回了nil，但是对任何非空列表进行排序都会进入无限递归循环。

翻译成 Haskell 时

split [] = ([], [])
split [x] = ([x], [])
split (x:y:xs) = (x:s1, y:s2)
  where (s1,s2) = split xs

merge xs [] = xs
merge [] ys = ys
merge xx@(x:xs) yy@(y:ys)
  | x < y     = x : merge xs yy
  | otherwise = y : merge xx ys

mergesort [] = []
mergesort xs = merge (mergesort p) (mergesort q)
  where (p,q) = split xs

GHC 推断出类似的类型：

*Main> :t mergesort
mergesort :: (Ord a) => [t] -> [a]

Damas–Hindley–Milner algorithm 是如何推断这种类型的？

Answer 1

可以推断出该类型，因为它看到您将mergesort 的结果传递给merge，后者又将列表的头部与< 进行比较，< 是 Ord 类型类的一部分。所以类型推断可以推断它必须返回一个 Ord 实例的列表。当然，由于它实际上是无限递归的，所以我们无法推断出它实际上没有返回的类型。

Answer 2

这确实是一个了不起的例子；本质上，在编译时检测到一个无限循环！这个例子中的 Hindley-Milner 推理没有什么特别之处。一切照常进行。

请注意，ghc 正确获取了split 和merge 的类型：

*Main> :t split
split :: [a] -> ([a], [a])
*Main> :t merge
merge :: (Ord t) => [t] -> [t] -> [t]

现在谈到mergesort，一般来说，对于某些类型t₁，它是一个函数t₁→t₂ > 和 t₂。然后它看到第一行：

mergesort [] = []

并意识到 t₁ 和 t₂ 必须是列表类型，例如 t₁=[t₃] 和 t₂=[t₄]。所以归并排序一定是一个函数[t₃]→[t₄]。下一行

mergesort xs = merge (mergesort p) (mergesort q) 
  where (p,q) = split xs

告诉它：

• xs 必须是要拆分的输入，即，对于某些 a（对于 a=t₃，它已经是 [a] 类型）。
• 所以p 和q 也是[t₃] 类型，因为split 是[a]→([a],[a])
• 因此，mergesort p（回想一下，mergesort 被认为是 [t₃]→[t₄] 类型）是 [t_4]。
• mergesort q 属于 [t₄] 类型，原因完全相同。
• 由于merge 的类型为(Ord t) => [t] -> [t] -> [t]，并且表达式merge (mergesort p) (mergesort q) 中的输入都是[t₄] 类型，因此类型t₄ 必须加入Ord。
• 最后，merge (mergesort p) (mergesort q) 的类型与其两个输入相同，即 [t₄]。这与 mergesort 的先前已知类型 [t₃]→[t₄] 相吻合，因此无需再进行推论和“统一”部分Hindley-Milner 算法完成。 mergesort 的类型为 [t₃]→[t₄]，t₄ 在 Ord 中。

这就是你得到的原因：

*Main> :t mergesort 
mergesort :: (Ord a) => [t] -> [a]

（上面关于逻辑推理的描述等同于算法所做的，但是算法遵循的具体步骤顺序只是在维基百科页面上给出的，例如。）