haskell - Finite comprehension of an infinite list

Question

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?

Answer 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..].