我不明白为什么以下 Haskell 代码在 GHCi 下终止:
let thereExists f lst = (filter (==True) (map f lst)) /= []
thereExists (\x -> True) [1..]
考虑到它的第二个参数是无限的,我没想到对 filter 的调用会完成,而且我认为在完全计算 lhs 之前不会进行比较。发生了什么?
我不明白为什么以下 Haskell 代码在 GHCi 下终止:
let thereExists f lst = (filter (==True) (map f lst)) /= []
thereExists (\x -> True) [1..]
考虑到它的第二个参数是无限的,我没想到对 filter 的调用会完成,而且我认为在完全计算 lhs 之前不会进行比较。发生了什么?
可以在完全计算 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
一旦我们知道/=
is的第一个参数(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
。