= Solution
Let $P(zss)$ mean `concat (map f zss) = f (concat zss)`. We use <structural induction on lazy lists>, including the <bottom value> and allowing arbitrary, possibly partial, inner <lists>.
For `[]`, the left side is `[]` and the right side is `f [] = []`. For the <bottom value> $\bot$, both `map f` and `concat` are <strict functions> in the outer spine, and the supplied strictness of $f$ makes the right side $f\,\bot=\bot$ too.
For the cons case, assume $P(zss)$ and write the new head as `xs`. The defining equations and the <induction hypothesis> give
$$
\begin{aligned}
\operatorname{concat}(\operatorname{map}f\,(xs:zss))
&=f(xs)\mathbin{++}\operatorname{concat}(\operatorname{map}f\,zss)\\
&=f(xs)\mathbin{++}f(\operatorname{concat}zss)\\
&=f(xs\mathbin{++}\operatorname{concat}zss)\\
&=f(\operatorname{concat}(xs:zss)).
\end{aligned}
$$
The third equality is exactly the supplied <list concatenation> preservation law. No inspection of `xs` was required, so the argument includes partial inner <lists> and undefined elements.
This proves the identity for every finite outer spine ending in either `[]` or $\bot$. In the usual pure <Haskell> semantics, these <functions> are <Scott continuous maps>. An infinite outer <list> is obtained as a limit by <finite approximation of a lazy list>; both composite <functions> preserve that limit. Equality on all its finite approximations therefore gives equality on the infinite outer <list>. Equivalently, $P$ is an <admissible predicate on lazy lists>. Consequently
$$
\boxed{\operatorname{concat}\circ\operatorname{map}f=f\circ\operatorname{concat}.}
$$
The continuity assumption is the usual semantic assumption for definable <functions> here; an extension from finite to infinite inputs cannot be justified by ordinary finite <induction> alone.
Back to article page
