25

在 Andrew Koenig 的关于 ML 类型推断的轶事中，作者使用归并排序的实现作为 ML 的学习练习，并且很高兴发现“不正确”的类型推断。

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

'a list -> int list

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

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

再想一想，我意识到还有另一种方法可以让函数忽略它的参数：也许它有时根本不返回。事实上，当我尝试它时，这正是发生的事情：sort(nil)确实 return 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 算法如何推断这种类型？

4

2 回答 2

30

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

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

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

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

mergesort [] = []

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

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

告诉它：

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

这就是为什么你得到：

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

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

于 2009-12-02T02:13:28.690 回答
2

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

于 2009-12-02T01:40:26.363 回答