Why does this Haskell filter terminate?

ghc, ghci, haskell, lazy-evaluation

Solution

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`.

Problem

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?

Original source