Can any recursive definition be rewritten using foldr?

Question

Say I have a general recursive definition in haskell like this:

foo a0 a1 ... = base_case
foo b0 b1 ...          
    | cond1 = recursive_case_1
    | cond2 = recursive_case_2
    ...

Can it always rewritten using foldr? Can it be proved?

Answer 1

If we interpret your question literally, we can write const value foldr to achieve any value, as @DanielWagner pointed out in a comment.

A more interesting question is whether we can instead forbid general recursion from Haskell, and "recurse" only through the eliminators/catamorphisms associated to each user-defined data type, which are the natural generalization of foldr to inductively defined data types. This is, essentially, (higher-order) primitive recursion.

When this restriction is performed, we can only compose terminating functions (the eliminators) together. This means that we can no longer define non terminating functions.

As a first example, we lose the trivial recursion

f x = f x
-- or even
a = a

since, as said, the language becomes total.

More interestingly, the general fixed point operator is lost.

fix :: (a -> a) -> a
fix f = f (fix f)

A more intriguing question is: what about the total functions we can express in Haskell? We do lose all the non-total functions, but do we lose any of the total ones?

Computability theory states that, since the language becomes total (no more non termination), we lose expressiveness even on the total fragment.

The proof is a standard diagonalization argument. Fix any enumeration of programs in the total fragment so that we can speak of "the i-th program". Then, let eval i x be the result of running the i-th program on the natural x as input (for simplicity, assume this is well typed, and that the result is a natural). Note that, since the language is total, then a result must exist. Moreover, eval can be implemented in the unrestricted Haskell language, since we can write an interpreter of Haskell in Haskell (left as an exercise :-P), and that would work as fine for the fragment. Then, we simply take

f n = succ $ eval n n

The above is a total function (a composition of total functions) which can be expressed in Haskell, but not in the fragment. Indeed, otherwise there would be a program to compute it, say the i-th program. In such case we would have

eval i x = f x

for all x. But then,

eval i i = f i = succ $ eval i i

which is impossible -- contradiction. QED.

Answer 2

In type theory, it is indeed the case that you can elaborate all definitions by dependent pattern-matching into ones only using eliminators (a more strongly-typed version of folds, the generalisation of lists' foldr).

See e.g. Eliminating Dependent Pattern Matching (pdf)