首页 文章

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

提问于
浏览 次
25

在Andrew Koenig的An anecdote about ML type inference中，作者使用merge sort的实现作为ML的学习练习，很高兴找到“不正确”的类型推断 .

令我惊讶的是，编译器报告了一种'list - > int列表
换句话说，这个sort函数接受任何类型的列表并返回一个整数列表 . 那是不可能的 . 输出必须是输入的排列;它怎么可能有不同的类型？读者肯定会发现我的第一个冲动：我想知道我是否在编译器中发现了一个错误！在考虑了一些之后，我意识到还有另一种方法可以忽略它的论点：也许它根本没有返回 . 确实，当我尝试它时，这正是发生的事情：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 algorithm如何推断这种类型？

haskell type-inference type-systems ml hindley-milner

2 回答

  • 30

    这确实是一个了不起的例子;基本上，在编译时检测到一个无限循环！在这个例子中，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] . 因此mergesort必须是函数[t3]→[t4] . 下一行

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

    告诉它：

    • xs必须是分割的输入，即某些a的类型[a]（对于a = t3，它已经是） .

    • 所以 p 和 q 也是[t3]类型，因为 split 是[a]→（[a]，[a]）
      因此，（回想一下，mergesort被认为类型为[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算法的"unification"部分已完成 . mergesort 的类型为[t3]→[t4]，其中t4为 Ord .

    这就是你得到的原因：

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

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

    回复于
  • 2

    可以推断出该类型，因为它看到您将 mergesort 的结果传递给 merge ，后者又将列表的头部与 < 进行比较，后者是Ord类型类的一部分 . 因此类型推断可以推断它必须返回Ord实例的列表 . 当然，因为它实际上无限地递归，我们实际上可以返回 .

    回复于

相关问题