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

Question

在 Andrew Koenig 的 An anecdote about ML type inference ，作者使用 merge sort 的实现作为 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 algorithm 如何推断这种类型？

Answer 1

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

注意 ghc 获取 split 的类型和 merge正确:

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

现在谈到 mergesort ，一般来说，对于某些类型 t1 和 t2，它是一个函数 t1→t2。然后它看到第一行:

mergesort [] = []

并意识到 t1 和 t2 必须是列表类型，例如 t1=[t3] 和 t2=[t4]。所以归并排序一定是一个函数[t3]→[t4]。下一行

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

告诉它:

xs 必须是 split 的输入，即某些 a 的类型为 [a](对于 a=t3，它已经是)。

所以p和 q也是 [t3] 类型，因为 split是[a]→([a],[a])

mergesort p ，因此(回想一下，归并排序被认为是 [t3]→[t4] 类型)是 [t4] 类型。

mergesort q出于完全相同的原因，属于 [t4] 类型。

如merge有类型 (Ord t) => [t] -> [t] -> [t] ，以及表达式 merge (mergesort p) (mergesort q) 中的输入都是 [t4] 类型，类型 t4 必须在 Ord .

最后是merge (mergesort p) (mergesort q)的类型与它的两个输入相同，即[t4]。这适合 mergesort 的先前已知类型 [t3]→[t4] , 所以不需要再做推论，Hindley-Milner 算法的“统一”部分就完成了。 mergesort是 [t3]→[t4] 类型，其中 t4 在 Ord .

这就是为什么你得到:

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

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