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

Question

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

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

我没想到过滤器的调用永远不会完成,因为它的第二个参数是无限的,我不认为比较可能发生在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.