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

[Tobias Nipkow]

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
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev