It is not hard to state, prove and use laws for well-known operations such as addition, multiplication and - at the function level - composition. It is, however, quite hard to state, prove and use laws for arbitrarily recursively defined functions, mainly because it is difficult to refer to the recursion scheme in isolation. The algorithmic structure is obscured by using unstructured recursive definitions. We crack this problem by treating various recursion schemes as separate higher order functions, giving each a notation of its own independent of the ingredients with which it constitutes a recursively defined function.
This philosophy is similar in spirit to the 'structured programming' methodology for imperative programming. The use of arbitrary goto's is abandoned in favour of structured control flow primitives such as conditionals and while-loops that replace fixed patterns of goto's, so that reasoning about programs becomes feasible and sometimes even elegant. For functional programs the question is which recursion schemes are to be chosen as a basis for a calculus of programs. We shall consider several recursion operators that are naturally associated with algebraic type definitions. A number of general theorems are proven about these operators and subsequently used to transform programs and prove their correctness.
By Erik Meijer, Maarten Fokkinga, and Ross Patterson https://maartenfokkinga.github.io/utwente/mmf91m.pdf