= Solution
For finite <lists>, prove the <right-fold fusion law> by <structural induction>. The empty case uses the base-image premise:
``
f (foldr g a []) = f a = b = foldr h b []
``
For the cons case, use the compatibility premise, then the <induction hypothesis>:
``
f (foldr g a (x:xs))
= f (g x (foldr g a xs))
= h x (f (foldr g a xs))
= h x (foldr h b xs)
= foldr h b (x:xs)
``
The assumption that `f` is a <strict function> addresses partial spines. Write $\bot$ for the <bottom value>. A <right fold> must inspect the outer <list> constructor, so
$$
f(\operatorname{foldr}\ g\ a\ \bot)=f(\bot)=\bot=\operatorname{foldr}\ h\ b\ \bot.
$$
The same cons calculation therefore establishes equality for finite partial spines ending in $\bot$, including partial heads, because compatibility was assumed for all arguments.
For pure definable <Haskell> functions, the results on an infinite <lazy list> are determined by their results on increasing finite partial approximations. Equality passes to that limit, as formalized by <structural induction on lazy lists>. Thus
$$
\boxed{f\circ\operatorname{foldr}(g,a)=\operatorname{foldr}(h,b).}
$$
For finite total inputs alone, the empty and cons cases suffice. Strictness is needed to extend the claim to undefined spines; the finite-total proof by itself does not justify the infinite-input claim.
Back to article page
