Diagonal merging of lazy lists
ID: diagonal-merging-of-lazy-lists
For an outer proper lazy list of inner proper lazy lists, introduce row in round and advance each active row once per round. Discard an active row when its terminating constructor is observed. Each round inspects finitely many rows, and the entry at row index , within-row index , is emitted in round . Every earlier round has finite work, proving fair enumeration of all occurrences.
An implementation can keep a finite list of row remainders, append at most one newly introduced row, collect one head from every nonempty remainder, and retain their tails for the next round. It must not first combine all not-yet-introduced rows. In fact,
foldr interleave [] ([1,2] : repeat []) can emit 1 and then block before 2; diagonal merging of lazy lists emits both. If infinitely many empty rows remain after the final output, detecting termination is impossible in general: the absence-detection obstruction for infinite lists prevents a universal promise of a terminating empty tail, while every required occurrence can still be emitted. New to topics? Read the docs here!