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) ysThe 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 have appeared, the nested list filters need skip only a finite input prefix: an infinite collection of distinct values cannot all belong to the 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.List concatenation exhausts one inner list before reaching the next. For example, with rows
[0,2..] and [1], concat outputs the infinite even row and never reaches 1. First-occurrence duplicate removal cannot recover a value that its input stream never supplies. HenceThe obstruction is separate from the undefined final tail in part (c): here a required distinct value is never emitted at all. A fair enumeration must give every row and every element within it a finite opportunity to contribute.For two proper lazy lists,
twiddle alternates heads, swapping which list is served after each output. Thus both input positions have finite waiting time. A tempting extension is remalldups . foldr twiddle [], but arbitrary empty rows make that insufficient: for [ [1,2] ] ++ repeat [], it emits 1 and then demands the combination of infinitely many empty rows before it can return to 2.Use diagonal merging of lazy lists to avoid that obstruction. Maintain a finite active collection, add at most one new row per round, and take one head from every nonempty active row. The supplied
twiddle combines those singleton contributions into a finite batch:union' = remalldups . rounds []
rounds [] [] = []
rounds active [] = emit active []
rounds active (row:rows) = emit (active ++ [row]) rows
emit active rows = batch ++ rounds tails rows
where (batch, tails) = sweep active
sweep [] = ([], [])
sweep ([]:rows) = sweep rows
sweep ((x:xs):rows) = (twiddle [x] heads, xs:tails)
where (heads, tails) = sweep rowsHere
rounds takes the finite active collection first and the not-yet-introduced outer list second. Because heads is a finite list, twiddle [x] heads emits x followed by those heads; the finite batch is then completely consumed before the next round. Empty exhausted rows are removed by sweep. No step tries to combine infinitely many not-yet-introduced rows.Index rows and positions from zero. Row is introduced in round and contributes its element in round , if that element exists. Every earlier round inspects only finitely many rows. Therefore every occurrence has a finite emission time, proving fair enumeration. Applying first-occurrence duplicate removal givesAll outer and inner spines must be proper lazy lists and equality tests must terminate. Infinitely many empty rows after the final contribution still prevent certifying a terminating empty tail, just as part (c) predicts. Undefined input spines have the separate partial-list interleaving obstruction; the construction makes no promise to bypass them.
On two finite total lists, the equations agree. If either list is empty they return the other; if both have heads, expanding
twiddle twice gives x : y : twiddle xs ys, exactly the third equation for twiddle'. The same finite-prefix reasoning proves agreement on infinite inputs with defined spines.They differ on partial lists. Take the first argument
[1] and the second argument . The original definition can emit its first head immediately:After recognizing the nonempty first argument, twiddle' must inspect the second argument to distinguish its second and third equations. That inspection diverges, soFor example, demanding only the head distinguishes them: the original returns 1, while the primed version diverges. Equality of functions under lazy evaluation requires agreement on these partial inputs too. Articles by others on the same topic
There are currently no matching articles.