The most informative occurrence-position representation of a sequence of natural numbers isEach nonnegative integer occurs once at its own index, and negative integers never occur.
naturals :: Seq Integer
naturals v
| v < 0 = []
| otherwise = [v]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. Articles by others on the same topic
There are currently no matching articles.