= Solution
The most informative <occurrence-position representation of a sequence> of natural numbers is
``
naturals :: Seq Integer
naturals v
| v < 0 = []
| otherwise = [v]
``
Each nonnegative integer occurs once at its own index, and negative integers never occur.
\b[This is not equal to `rep [0..]` under <lazy evaluation>.] For a nonnegative query `v`, `rep` eventually emits `v`, but then searches forever for another occurrence: its result has the shape `v : undefined`, rather than the terminating singleton `[v]`. For a negative query, even the outer constructor is never produced, whereas `naturals` immediately returns `[]`.
No general, correct `rep :: Eq a => [a] -> Seq a` can always certify those absences from an arbitrary infinite input. A terminating certification has inspected only finitely many elements, and the same prefix could be followed by the supposedly absent value, or by a further occurrence of it. Extra knowledge changes the problem: for a promised strictly increasing integer input, a search can stop with `[]` when it first exceeds the query and return `[i]` immediately upon equality. That specialised representation can produce `naturals`; a generic search cannot. This is the <absence-detection obstruction for infinite lists>.
Back to article page
