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

Question

在安德鲁·柯尼格的书中 关于 ML 类型推断的轶事, ，作者使用的实现 归并排序 作为 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 算法 推断出这种类型？

Answer 1

这确实是一个了不起的例子；本质上，检测到无限循环 编译时间！在这个例子中，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 必须是 split 的输入，即对于某个 a 来说，其类型为 [a]（对于 a=t 来说，它已经是这样了）₃).
• 所以 p 和 q 也是类型 [t₃]， 自从 split 是 [a]→([a],[a])
• mergesort p, ，因此，（回想一下，归并排序被认为是 [t₃]→[t₄]) 的类型为 [t₄].
• mergesort q 类型为 [t₄] 出于完全相同的原因。
• 作为 merge 有类型 (Ord t) => [t] -> [t] -> [t], ，以及表达式中的输入 merge (mergesort p) (mergesort q) 都是 [t 类型₄]，类型 t₄ 必须在 Ord.
• 最后，类型 merge (mergesort p) (mergesort q) 与其两个输入相同，即 [t₄]。这符合先前已知的类型 [t₃]→[t₄] 为了 mergesort, ，因此无需进行更多推论，Hindley-Milner 算法的“统一”部分已完成。 mergesort 类型为 [t₃]→[t₄] 与 t₄ 在 Ord.

这就是为什么你会得到：

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

（上面的逻辑推理描述与算法的作用相同，但算法遵循的具体步骤顺序只是维基百科页面上给出的，例如。）

Answer 2

这类型可以推断，因为它看到传递mergesort的结果来merge，这反过来又清单的头与<，这是奥德类型类的部分进行比较。所以类型推断可能原因，它必须返回奥德的实例的列表。当然，因为它实际上无限递归，也不能推断任何关于它实际上并不返回类型。