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

[Makarius]

On Fri, 13 Jan 2012, Brian Huffman wrote:

> 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.

"Canonical" is a technical term from the Isabelle/ML culture.  The idea 
behind it is already firmly established for many years, the name is there 
for quite a few years as well.  The Isabelle/Isar Implementation Manual 
privides some text on this in section 0.3.  (Does anybody have a PDF to 
Stone-Tablet-Printer?)

I've never claimed myself that the HOL library or any other language out 
there is or has to be canonical in that sense, although it would do them 
good.


 	Makarius