"Any function on finite lists that is defined by pairing the desired result with the argument list can always be redefined in terms of fold"

Question

I was reading through the paper A tutorial on the universality and expressiveness of fold, and am stuck on the section about generating tuples. After showing of how the normal definition of dropWhile cannot be defined in terms of fold, an example defining dropWhile using tuples was proved:

dropWhile :: (a -> Bool) -> [a] -> [a]
dropWhile p = fst . (dropWhilePair p)

dropWhilePair :: (a -> Bool) -> [a] -> ([a], [a])
dropWhilePair p = foldr f v
  where
    f x (ys,xs) = (if p x then ys else x : xs, x : xs)
    v           = ([], [])

The paper states:

In fact, this result is an instance of a general theorem (Meertens, 1992) that states that any function on finite lists that is defined by pairing the desired result with the argument list can always be redefined in terms of fold, although not always in a way that does not make use of the original (possibly recursive) definition for the function.

I looked at Meerten's Paper but do not have the background (category theory? type theory?) and did not quite find how this was proved.

Is there a relatively simple "proof" why this is the case? Or just a simple explanation as to why we can redefine all functions on finite lists in terms of fold if we pair the results with the original list.

Answer 1

Given the remark that you can / may need to use the original function inside, the claim as stated in your question seems trivial to me:

rewriteAsFold :: ([a] -> (b, [a])) -> [a] -> (b, [a])
rewriteAsFold g = foldr f v where
    f x ~(ys,xs) = (fst (g (x:xs)), x:xs)
    v            = (fst (g []), [])

EDIT: Added the ~, after which it seems to work for infinite lists as well.