haskell - 为什么这个 Haskell 过滤器会终止？

Question

我不明白为什么以下 Haskell 代码在 GHCi 下终止:

let thereExists f lst = (filter (==True) (map f lst)) /= []
thereExists (\x -> True) [1..]

考虑到它的第二个参数是无限的，我没想到对 filter 的调用会完成，而且我认为在完全计算 lhs 之前不会进行比较。发生了什么？

Answer 1

可以在完全计算 LHS 之前进行比较。尽快filter产生了一种元素，/=能够得出该列表不可能等于 [] 的结论并立即返回True .
/=列表上的实现是这样的:

(/=) :: Eq a => [a] -> [a] -> Bool
[] /= []         = False
[] /= (y:ys)     = True
(x:xs) /= []     = True
(x:xs) /= (y:ys) = (x /= y) || (xs /= ys)

由于 Haskell 是惰性的，我们将只评估参数，以选择我们将使用哪个右手边。对您的示例的评估如下所示:

    filter (== True) (map (\x -> True) [1..]) /= []
==> (True : (filter (== True) (map (\x -> True) [2..]))) /= []
==> True

一旦我们知道 /= 的第一个参数是 (1 : something) ，它匹配 /= 的第三个方程在上面的代码中，所以我们可以返回 True .

但是，如果您尝试 thereExists (\x -> False) [1..]它确实不会终止，因为在那种情况下 filter将永远不会在生成我们可以匹配的构造函数方面取得任何进展。

     filter (== True) (map (\x -> False) [1..]) /= []
==>  filter (== True) (map (\x -> False) [2..]) /= []
==>  filter (== True) (map (\x -> False) [3..]) /= []
...

以此类推。

总之，thereExists在无限列表上可以返回 True在有限的时间内，但从不False .