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

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.

Answer 2

(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 3

The property that fold has is that it is a list-recursing function, which is equivalent to all other list-recursing functions, provided you give it the right parameters.

It has this property, because it accepts as a parameter, the functions which will be applied to the items in the list.

For example, if we wrote a simple sum function:

sum []          = 0
sum (head:tail) = head + (sum tail)

then we could actually write it as a fold function instead, by passing in the (+) operator which we want to use to combine the items:

sum list = foldl (+) 0 list

So any function which acts simply and recursively over a list can be rewritten as a fold function. That equivalence is the property it holds. I believe he calls the property universal, because it works over all these linear-list-recursive algorithms, without exception.

And as he explains, the reason this property is so useful, is that because we can show all these other algorithms are actually equivalent to fold, by proving something about fold, we also prove it for all those other algorithms.

I personally found the fold function hard to understand, so sometimes I used my own which looks like this:

-- forall - A kind of for next loop
-- list is list of things to loop through
-- f is function to perform on each thing
-- c is the function which combines the results of f
-- e is the thing to combine to when the end of the list is reached
forall :: [a] -> (a->b) -> (b->b->b) -> b -> b
forall [] f c e = e
forall (x:xs) f c e = c (f x) (forall xs f c e)

(This is actually slightly more powerful than foldl because it has the extra feature of applying the function f to each item in the list.)

Well nobody proved anything about my function. But that doesn't matter, because I can show that my function is in fact a fold function:

forall l f c e = foldl c e (map fn l)

And hence all the things that have been proved about fold, are also proven true for my forall function, and all its uses throughout my program. (Note we need not even consider what kind of function c is supplied in each of the different calls to forall and foldl, it doesn't matter!)

Answer 4

I just found a new (to me) entry in Wikipedia, "Universal Property". It sheds a TON of light on this question. Here's the link: From it, I (tenatively) conclude the following:

1. Though you may think of 100 different ways to walk through a list, computing along the way, and producing one final value from the list, all 100 of those ways are isomorphic (meaning that ultimately, they're the same). There really is only one way to reduce a list to one value, and that is FOLD.
2. Fold is also the "most efficient solution" to how to reduce a list to a single value. Or you might say, the most "factored" or most "simplified" solution.

Together, it seems, those 2 points capture the meaning of the term "universal property".