Why does this Haskell filter terminate?

Question

I don't understand why the following Haskell code terminates under GHCi:

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

I did not expect the call to filter to ever complete, given that its second argument is infinite, and I did not think the comparison could take place until the lhs was completely calculated. What's happening?

Answer 1

The comparison can take place before the LHS is completely calculated. As soon as filter has produced one element, /= is able to conclude that the list can't possibly be equal to [] and immediately return True.

/= on lists is implemented something like this:

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

Since Haskell is lazy, we will only evaluate the arguments as much as is necessary to choose which right hand side we will use. Evaluation of your example goes something like this:

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

As soon as we know that the first argument of /= is (1 : something), it matches the third equation for /= in the code above, so we can return True.

However, if you try thereExists (\x -> False) [1..] it will indeed not terminate, because in that case filter will never make any progress towards producing a constructor we can match against.

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

and so on infinitely.

In conclusion, thereExists on an infinite list can return True in finite time, but never False.