[isabelle-dev] "canonical" left-fold combinator for lists

[Brian Huffman]

Hello all,

I am writing about the following recent changeset, which adds another
left-fold operator to HOL/List.thy.

author	haftmann
	Fri Jan 06 10:19:49 2012 +0100 (6 days ago)
changeset 46133	d9fe85d3d2cd
parent 46132 	5a29dbf4c155
child 46134 	4b9d4659228a
incorporated canonical fold combinator on lists into body of List
   theory; refactored passages on List.fold(l/r)

http://isabelle.in.tum.de/repos/isabelle/rev/d9fe85d3d2cd

I would like to take issue with a couple of things here. First, I
don't understand why it should be called "canonical". What mainstream
programming language has a left-fold operation with this particular
type signature? The only place I have ever seen this variety of fold
is in src/Pure/General/basics.ML in the Isabelle distribution.

Second, why is the right-fold now defined in terms of a left-fold? I
think it is generally recognized that inductive proofs about
right-folds are easier than proofs about left-folds. If the goal of
defining folds in terms of each other is to simplify proofs, then I'm
sure that it would work better to define everything in terms of foldr.

Finally, do we really need *two* left-fold combinators in our standard
list library? To maintain a complete set of rewrite rules for the list
library, we need approximately one lemma for every combination of two
library functions - i.e., the number of required theorems is
approximately quadratic in the number of constants. Adding a new fold
constant means we must either add a large number of new theorems about
it, or else we must deal with having some missing theorems. Neither of
these choices sounds good to me.

Here is what I suggest: If there is a concensus that the argument
order of List.fold is more useful than the existing foldl, then we
should simply *replace* foldl with the new fold. Otherwise we should
get rid of the new List.fold.

For users who want to use programming idioms that require different
argument orders, I suggest providing a "flip" function (perhaps in
Fun.thy) as Haskell does:

definition flip :: "('a => 'b => 'c) => 'b => 'a => 'c"
  where "flip f x y = f y x"

- Brian