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

Question

在安德鲁·科尼格的关于ML类型推断的轶事中，作者使用归并排序的实现作为ML的学习练习，并且发现了一个“不正确”的类型推断，这让他非常高兴。

Much to my surprise, the compiler reported a type of

'a list -> int list

In other words, this sort function accepts a list of any type at all and returns a list of integers.

That is impossible. The output must be a permutation of the input; how can it possibly have a different type? The reader will surely find my first impulse familiar: I wondered if I had uncovered a bug in the compiler!

After thinking about it some more, I realized that there was another way in which the function could ignore its argument: perhaps it sometimes didn't return at all. Indeed, when I tried it, that is exactly what happened: sort(nil) did return nil, but sorting any non-empty list would go into an infinite recursion loop.

当翻译成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算法如何推断这种类型？

- Greg Bacon

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₄]。因此，mergesort必须是一个函数[t₃]→[t₄]。下一行

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

告诉它：

• xs 必须是 split 的输入，即某种类型 [a] 的输入（对于 a=t₃，它已经满足了这一点）。
• 因此，p 和 q 也都是类型为 [t₃] 的数组，因为 split 是一个函数 [a]→([a],[a])。
• 因此，mergesort p(记住 mergesort 的类型是 [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₄]。这符合先前已知的 mergesort 的类型 [t₃]→[t₄]，因此不需要进行更多的推断，Hindley-Milner 算法的“统一”部分已经完成。 Mergesort 的类型是 [t₃]→[t₄]，其中 t₄ 属于 Ord。

这就是为什么会得到：

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

（上述逻辑推理的描述等价于算法所做的事情，但算法遵循的具体步骤仅仅是维基百科页面上给出的步骤。）

- ShreevatsaR

---

我认为说类型推断“检测到”无限循环有些牵强。相反，类型系统推断出一个（完全有效的）类型，与程序员的预期不同，这导致他重新审视代码并自己检测到了无限循环。但这仍然非常有趣！ - Geoff

@Geoff：同意。 （我试图用“本质上”来修饰它:p）然而，令人惊奇的是，类型检查使程序员能够在编译时找到无限循环错误。 Mark Jason Dominus在他的类型讲座中也讨论了这个例子，链接在这里：http://perl.plover.com/classes/OOPSLA/samples/slide061.html - ShreevatsaR

我几年前从Dominus的演讲中了解到这个例子。一开始我有他笔记的指针，但是因为额外的引用看起来有点啰嗦，所以我把它拿掉了：http://perl.plover.com/yak/typing/notes.html - Greg Bacon

Answer 2

这种类型可以被推断出来，因为它看到您将mergesort的结果传递给merge，后者使用<与列表的头进行比较，这是Ord类型类的一部分。因此，类型推断可以推断它必须返回一个Ord实例的列表。当然，由于它实际上会无限递归，我们不能推断出关于它没有实际返回的类型的其他信息。

- Chuck