= 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.
Back to article page