= Solution
\b[Yes, under the finite total assumption in part (d).] The pair result retains enough information to reconstruct the tail; the `~` pattern keeps its two components lazy:
``
spanFold :: (a -> Bool) -> [a] -> ([a], [a])
spanFold p = foldr step ([], [])
where
step x ~(ys,zs)
| p x = (x:ys,zs)
| otherwise = ([],x:(ys ++ zs))
``
Take $f=\operatorname{spanP}\ p$, $g=(:)$ and $a=[]$. The base image is $([],[])$. If $p(x)$ is true, the recursive equation gives the first branch. If it is false, part (d), applied to the tail, gives $ys\mathbin{++}zs=xs$, so the second branch becomes $([],x:xs)$. These are precisely the fusion compatibility equations. Finite <structural induction> establishes the desired equality; it does not require extending the restricted-domain hypothesis to undefined <predicate> applications.
The qualification matters. If $p(v)$ is false but $p(u)$ is undefined, ordinary `spanP p [v,u]` can return the untouched <list suffix> immediately, whereas the reconstruction through `spanFold p [u]` cannot recover that <list suffix>. The weaker condition needed only for the single reconstruction identity in (d) is therefore insufficient for this particular <list fold> on all <list suffixes>. The stronger totality condition stated there supplies exactly the missing premise.
Back to article page
