在 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 returnnil
, 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 如何推断这种类型?
最佳答案
这确实是一个了不起的例子;本质上,在编译时检测到无限循环!这个例子中的 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
告诉它:
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]
(上面关于逻辑推理的描述等同于算法所做的,但是算法遵循的具体步骤顺序只是在维基百科页面上给出的,例如。)
关于haskell - 推断类型似乎检测到无限循环,但到底发生了什么?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/1830005/