Finite comprehension of an infinite list

I typed the following into ghci, thinking that one of two things would happen: 1) The interpreter would hang, searching every member of an infinite list for matches to a predicate; or 2) through behind-the-curtains Haskell jujitsu, the interpreter would somehow figure out that the sequence terminates at 4 and stop there.

[x | x <- [1..],5>x]

Outcome 1 was what happened. Now, outcome 2 was a lot to ask for. But since a human can prove that the sequence terminates at 4, might there be a way to get the interpreter to do it? Could this be rewritten in such a way that it does terminate? In fact, is there ever a predicate which makes a finite comprehension out of an infinite list?

Solution 1:

But since a human can prove that the sequence terminates at 4, might there be a way to get the interpreter to do it?

In this simple case, yes. But there cannot exist a general algorithm to determine if an expression is true or false for all natural numbers >n for some n, because Haskell is Turing-complete, so it's impossible to prove that an expression even represents a terminating program for all natural numbers.

Even if your expression were limited to basic integer arithmetic, its truth would still be undecidable in the general case.

Could this be rewritten in such a way that it does terminate?

As Mog wrote in the comment, it's takeWhile (< 5) [1..].

Solution 2:

takewhile is the correct solution for your specific problem, as mentioned above.

However, this is only because in your case, all acceptable arguments come before all unacceptable arguments, and the general list comprehension doesn't obey that constraint. It would certainly possible to add symbolic reasoning to the interpreter so that it could prove that no further elements will be acceptable and then terminate. (In fact, the sophisticated type system in Haskell would be quite useful in implementing such reasoning.) But it would not make sense to add this to the standard [|] operator, since the detector would have to run on all list comprehensions that are evaluated, and would very often fail to contribute anything except much more computing expense.

Solution 3:

"But since a human can prove that the sequence terminates at 4, might there be a way to get the interpreter to do it?"

Good question. The difficult thing is not the proof that it terminates at 4, but the idea that it could possibly terminate at 4, followed by the insight that this is indeed so.