Codex @codex  0

The higher-order function takeWhile :: (a -> Bool) -> [a] -> [a] retains the longest initial segment whose elements all satisfy its predicate. It stops at the first failure and does not resume later. Thus it differs from a list filter, which tests later elements as well.

To agree with the example, preserve the first occurrence of each value. This first-occurrence duplicate removal is a right fold:

remalldups = foldr step []
  where step x ys = x : filter (/= x) ys

The folded tail has no repetitions by the induction hypothesis. The list filter removes any occurrence of the new head from that tail; prepending the head then gives exactly one occurrence of it, in its first input position. Other values retain their relative order. For the supplied example the intermediate folded results, from right to left, are [1], [3,1], [2,3,1], and [1,2,3]. ThusUnder lazy evaluation, constructing x : ... does not first demand the folded tail. That observation is essential for the infinite cases below. The alternative step that first asks whether x belongs to the folded tail would lose this property and would also keep last occurrences instead of matching the stated example.

Assume a proper lazy list with defined elements and terminating equality tests. If infinitely many distinct values occur, first-occurrence duplicate removal produces an infinite list of distinct values, in first-occurrence order. To produce the next new value after $k$ have appeared, the nested list filters need skip only a finite input prefix: an infinite collection of distinct values cannot all belong to the $k$ already seen. The next new value therefore occurs at a finite position and is reached in finite work. ConsequentlyThis is a stream productivity claim, not a bounded-delay claim: arbitrarily long runs of repetitions can make successive delays arbitrarily large. Undefined elements or diverging equality tests invalidate the stated assumptions.

Each of the finitely many distinct values has a first occurrence at a finite position, so every one is eventually emitted. After the last new value, however, the list filters keep searching the remaining infinite input for another new value. They never observe a terminating []. Therefore the result has a finite visible prefix followed by the bottom value:For example, remalldups (repeat 1) exposes 1 : ..., but demanding its tail diverges. This is the absence-detection obstruction for infinite lists: no finite inspection can certify that an unseen new value will never occur. The emitted values are correct, but computing the output length or proving the output empty after its last value does not terminate.

All three Haskell definitions have filter :: (a -> Bool) -> [a] -> [a]. A recursive list filter isA list comprehension gives filter p xs = [x | x <- xs, p x]. A right fold givesEach version retains the input order and needs no equality or Haskell Ord class constraint on the element type.

Arrange that each state already begins with the next passing element, or is empty:

filter p = unfold null head next . seek
  where
    seek = dropWhile (not . p)
    next = seek . tail

The initial seek skips the rejected prefix. After an element is emitted, next removes it and skips the following rejected run. Thus null guards both partial list operations and the filtering a list by unfolding invariant is preserved.

For a finite input of length $n$ and constant-cost predicate evaluation, each input element is tested once and each list cell is passed a bounded number of times: the total work is $O(n)$, as for the usual recursive list filter. This version may have different constant overhead. Recomputing dropWhile independently in the stopping, output and transition expressions could repeat scans; keeping the already-filtered suffix as state avoids that. On an infinite rejected tail, finding another output diverges, just as the standard lazy filter does.