Past exam of the year 1 of the computer science course of the University of Oxford / 2019 / Functional programming, design and analysis of algorithms / 4 / b / Solution

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 $j$-th input occurrences appear after at most $2j+2$ 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.