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

Question

在Andrew Koenig的关于ML类型推理的轶事中,作者使用合并排序的实现作为ML的学习练习,并且很高兴地发现"不正确"的类型推断.

令我惊讶的是,编译器报告了一种类型

'a list -> int list

换句话说,这个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]

如何在达马斯-辛德米尔纳算法推断出这种类型的？

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 ₂.然后它看到第一行:

mergesort [] = []

并且认识到t ₁和t ₂必须是列表类型,比如t ₁ = [t ₃ ]和t ₂ = [t ₄ ].因此mergesort必须是函数[t ₃ ]→[t ₄ ].下一行

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

告诉它:

• xs必须是要分割的输入,即某些a的类型[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 ₄ ].这符合先前已知的类型[t ₃ ]→[t ₄ ] mergesort,因此不再进行推论,并且Hindley-Milner算法的"统一"部分是完整的.mergesort是[t ₃ ]→[t ₄ ]类型,t ₄ in Ord.

这就是你得到的原因:

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

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