= Solution
\b[In general, no direct <list fold> with result type `[a]` can implement `dropWhile p`.] Choose total values $u,v$ for which $p(u)=\mathrm{True}$ and $p(v)=\mathrm{False}$. The results on `[]` and `[u]` are both `[]`. A hypothetical implementation `foldr h z` would therefore receive identical folded-tail values when extending either input by the same head $v$. Yet the required outputs are `[v]` and `[v,u]`, respectively. This contradicts the <fold factorisation criterion>: the combining <function> cannot distinguish information already discarded by its tail summary.
The claim concerns a direct same-result-type <list fold>. A <list fold> returning extra information, followed by a projection, is possible: a pair can retain both the original tail and the dropped <list suffix>. Also, special <predicates> can have direct <list folds>: a constantly false <predicate> gives the identity; a constantly true <predicate> can use `foldr (\_ r -> r) []`, which correctly diverges when it must traverse an infinite spine. Those special cases do not supply an implementation for an arbitrary <predicate>.
Back to article page
