Generalizing fold such that it becomes expressive enough to define any finite recursion?

Question

So, there is something known as a "universal property of fold", stating exactly following:

g [] = i; g (x:xs) = f x (g xs) <=> g = fold f i

However, as you probably now, there are rare cases like dropWhile, which can not be redefined as fold f i unless you generalize it.

The simplest yet obvious way to generalize is to redefine universal property:

g' y [] = j y; g' y (x:xs) = h y x xs (g' y xs) <=> g' y = fold (?) l

---

At this point I can make my assumption: I assume existence of somewhat function p :: a -> b -> b, which would satisfy the equation g' y = fold p l. Let's try to solve given equation with help of universal property, mention at the very beginning:

• g' y [] = j y = fold p l [] = l => j y = l
• g' y (x:xs) = h y x xs (g' y xs) = fold p l (x:xs) = p x (fold p l xs) = p x (g' y xs) => letting rs = (g' y xs), h y x xs rs = p x rs, which is wrong: xs occurs freely from the left and thus equality can't hold.

---

Now let me try to interpret result I've came up with and ask question. I see that the problem is xs emerging as unbound variable; it's true for various situations, including above mentioned dropWhile. Does it mean that the only way that equation can be solved is by "extending" rs to a pair of (rs, xs)? In other words, fold accumulates into tuple rather than a single type (ignoring the fact that tuple itself is a single type)? Is there any other way to generalize bypassing pairing?

Answer 1

It is as you say. The universal property says that g [] = i; g (x:xs) = f x (g xs) iff g = fold f i. This can't apply for a straightforward definition of dropWhile, as the would-be f :: a -> [a] -> [a] depends not just on the element and accumulated value at the current fold step, but also on the whole list suffix left to process (in your words, "xs emerg[es] as an unbound variable"). What can be done is twisting dropWhileso that this dependency on the list suffix becomes manifest in the accumulated value, be it through a tuple -- cf. dropWhilePair from this question, with f :: a -> ([a], [a]) -> ([a], [a]) -- or a function -- as in chi's implementation...

dropWhileFun = foldr (\x k -> \p -> if p x then k p else x : k (const False)) (const [])

... with f :: a -> ((a -> Bool) -> [a]) -> ((a -> Bool) -> [a]).

At the end of the day, the universal property is what it is -- a fundamental fact about foldr. It is no accident that not all recursive functions are immediately expressible through foldr. In fact, the tupling workaround your question brings to the table directly reflects the notion of paramorphism (for an explanation of them, see What are paramorphisms? and its exquisite answer by Conor McBride). At face value, paramorphisms are generalisations of catamorphisms (i.e. a straightforward fold); however, it only takes a slight contortion to implement paramorphisms in terms of catamorphisms. (Additional technical commentary on that might be found, for instance, in Chapter 3 of Categorical Programming With Inductive and Coinductive Types, Varmo Vene's PhD thesis.)