I agree very strongly. I am not tied to any particular argument order, but there should only be 2, not 3 folds. And there should be no claims of canonicity. If anything, the canonical fold operator (with some sensible argument order) is foldr f c which replaces :: by f and [] by c. And to avoid further canonicity arguments, the two names should be foldl and foldr (The nice article by Graham Hutton calls foldr fold and only mentions foldl in a subsection.)
Tobias Am 13/01/2012 08:33, schrieb 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 > _______________________________________________ > isabelle-dev mailing list > [email protected] > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
