为什么Haskell过滤器会终止？

我不明白，为什么下面的Haskell代码GHCI下终止：为什么Haskell过滤器会终止？

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

没想到调用过滤永远完整的，因为它的第二个参数是无穷的，我没想到的比较可能会发生，直到lhs被完全计算。发生了什么？

来源

2012-10-29 Ellen Spertus

顺便说一下，'thereExists'在标准库中，除了它被称为'any'。 – hammar

我让学生将自己的版本作为测试问题写入thereExists。我告诉一个学生他的版本（上面）没有终止，他告诉我它做到了。他是对的，我现在明白为什么。 –

还要注意[1 ..]是*不*必须是无限的。默认类型是[Integer]，但它也可以是[Int]，它通常具有2^31-1或2^63-1元素。 – Tener

比较被完全计算出的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。

来源

2012-10-29 22:13:29 hammar

谢谢。你能告诉我关于这个魔法是如何实现的吗？是/ =内置到Haskell中，还是可以用Haskell编写？ –

@espertus它可以用Haskell编写 - 它是。它定义为'xs/= ys = not（xs == ys）'，'（==）'由'[== ==] [] = True给出; （x：xs）==（y：ys）= x == y && xs == ys; _ == _ = False'。 –

@espertus这只是非严格的评估。这种情况没有什么特别的特别之处。这就是Haskell的工作原理。 – Ben

为什么Haskell过滤器会终止？

回答

相关问题