For proper lazy lists, the generic condition is a finite first list, or an empty second list. A finite first list reaches its terminating constructor, after which list concatenation exposes the second one. An infinite first list never yields control to the second; it therefore cannot deliver occurrences originating there unless there are none. This concerns input occurrences, rather than an accidental overlap of the two inputs' value sets.
A first spine ending in the bottom value also prevents access to the second list. Such inputs require the partial-input qualification in part c; a visible prefix is different from a terminating finite list.
Swap roles after emitting one element:
interleave :: [a] -> [a] -> [a]
interleave []     ys = ys
interleave (x:xs) ys = x : interleave ys xs
While both lists are nonempty, the function alternates between them. Their -th input occurrences appear after at most output steps, counting positions from zero; once either list ends, the other is returned directly. Every output constructor comes from one input constructor, and every input occurrence is eventually selected. This proves fair enumeration and productivity on the two proper lazy lists, including two infinite ones.
No universally correct sequential Haskell implementation has that guarantee for partial lists. Compare undefined paired with [v], and [v] paired with undefined, where the element type is arbitrary. A generic program cannot fabricate v; it must eventually inspect an input spine to obtain it. Whichever input it first demands can be chosen to be the undefined one, blocking access to the available element in the other input.
In particular, the implementation in part b can emit a defined prefix and then block when alternation reaches an undefined tail. Lazy evaluation postpones demands; it cannot recognize that a demanded computation will never finish. The result is the partial-list interleaving obstruction, not an objection to fairness under the proper-input hypothesis. Additional concurrent primitives would change the computational model.[ref]
Use diagonal merging of lazy lists: introduce one new row each round, and advance every active row once. Each round contains finitely many active rows, even when the outer list is infinite.
fairConcat :: [[a]] -> [a]
fairConcat = concat . levels []
  where
    levels [] [] = []
    levels active pending =
      let (new,rest) = case pending of
            []     -> ([],[])
            r:rs   -> ([r],rs)
          live = [r | r@(_:_) <- active ++ new]
      in map head live : levels (map tail live) rest
Number rows and positions within each row from zero. An occurrence at is emitted in round : its row enters in round and advances once per subsequent round. All earlier rounds and each round's output are finite, so every required occurrence appears after finite work. live discards only empty rows, and head emits only existing entries; no new value is invented.
Figure 1.
Diagonal merging of lazy lists visits every finite row-position pair after finitely many rounds
. Details.
Simply nesting interleave is unsafe here: foldr interleave [] ([1,2] : repeat []) emits 1 and then demands an undefined merge of the infinitely many empty rows before it can emit 2. The finite-round construction avoids that starvation. There is still an unavoidable termination qualification: after the last actual output, infinitely many empty pending rows cannot be certified empty in finite work. The result can then have an undefined tail instead of a terminating []. Every required occurrence has nevertheless appeared; no generic algorithm can promise a proper completed output in that exceptional situation, by the absence-detection obstruction for infinite lists.
The ordinary list comprehension exhausts the inner list before advancing the outer one. Therefore it enumerates every argument pair when ys is finite, or when xs has at most one element. If ys is infinite and xs has two or more elements, it stays with the first outer element forever and misses every pair with a later outer occurrence. Applying a constant f might hide missing pairs as duplicate values; it does not make the enumeration fair.
An empty-result caveat remains when ys = [] and xs is infinite: the literal comprehension traverses infinitely many empty rows and does not return a terminating empty list. Its occurrence requirement is vacuous, but its productivity as an empty-result computation fails. An explicit empty-input test avoids that particular failure.
Merge the rows with fairConcat, retaining explicit empty-input cases:
fairPair :: (a -> b -> c) -> [a] -> [b] -> [c]
fairPair _ [] _  = []
fairPair _ _  [] = []
fairPair f xs ys = fairConcat [[f x y | y <- ys] | x <- xs]
For nonempty proper lazy lists, the occurrence f (xs!!i) (ys!!j) belongs to row , position , so the proof in part d puts it in round . This supplies every pair after finite work, even when both input lists are infinite. The guards also return [] for either empty factor without traversing infinitely many empty rows.
For a finite outer list of proper lazy lists, use the fair binary product from part f:
cp :: [[a]] -> [[a]]
cp []       = [[]]
cp (xs:xss) = fairPair (:) xs (cp xss)
The empty family has one selection, the empty selection. For a nonempty finite family, each selection consists uniquely of one first-factor occurrence followed by a selection from the remaining factors. Induction on the number of factors, together with the fairness of fairPair, proves that every such selection is produced and no invalid selection is introduced. Infinite factors are allowed: in particular, the three-factor example is enumerated fairly. If any factor is empty, the finite-family computation returns the empty product.
The printed hypothesis also permits an infinite outer proper lazy list. No function can satisfy the full enumeration requirement for all such inputs. Take repeat [0,1]. Its mathematical Cartesian product contains every infinite binary sequence and is uncountable. If a result list enumerated these sequences as , the binary sequence with would differ from the -th listed sequence at position , contradicting completeness. This is an uncountability obstruction to enumerating infinite Cartesian products. The finite-outer qualification is a necessary repair to the specification, not a restriction imposed for convenience by the code.

Ancestors (10)

  1. Functional programming, design and analysis of algorithms
  2. 2019
  3. Past exam of the year 1 of the computer science course of the University of Oxford
  4. Year 1 of the computer science course of the University of Oxford
  5. Computer science course of the University of Oxford
  6. Undergraduate course of the University of Oxford
  7. Course of the University of Oxford
  8. University of Oxford
  9. List of universities
  10. Home

View article source

Discussion (0)

New discussion

There are no discussions about this article yet.

Articles by others on the same topic (0)

There are currently no matching articles.
See all articles in the same topic Create my own version