Please explain in the simplest, most jargon-free English possible, the "universal property of fold"?

Question

I am working through "Real World Haskell", which led to to a free PDF called "A tutorial on the universality and expressiveness of fold". It makes the point that a "fold" is "universal". I am wrestling with his definition of "universal", and would like to hear the from those who have already invested time digesting it: Please explain in the simplest, most jargon-free English possible, the "universal property of fold"? What is this "universal property", and why is it important?

Thanks.

Answer 1

(Jargon mode off :-)

The universal property is just a way of proving that two expressions are equal. (That's what is meant by the jargon "proof principle".) The universal property says that if you are able to prove these two equations

g []     = v
g (x:xs) = f x (g xs)

then you may conclude the additional equation

g = fold f v

The converse is also true, but that's trivial to show just by expanding the definition of fold. The universal property is a much deeper property (which is a jargony way of saying it's less obvious why it is true.)

The reason it's interesting to do this at all is that it lets you avoid proof by induction, which is almost always worth avoiding.

Answer 2

the paper defines two properties:

g   []     = v
g (x : xs) = f x (g xs)

and then states that fold is not only a function that satisfies those properties, but is the only function that satisfies those properties. that it is unique in that regard is what makes it 'universal' in the sense the paper is using.