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

[Tobias Nipkow]

Am 13/01/2012 21:13, schrieb Florian Haftmann:
> Hi all,
> 
>> 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 short: I have no objections to get rid of foldl.
> 
> There were indeed some considerations before introducing List.fold into
> Main HOL (being present in HOL-Library since around early summer 2010).
>  At some time I will set out them on the mailing list.
> 
> The only remark on the discussion about »canonicity« I want to add is
> that the use of the word »canonical« is quite canonical in our
> community, no matter how canonical Ubuntu is.

As Makarius already pointed out: you are conflating two communities
here. What is defined as canonical on the Isabelle/ML level is
definitely un-canonical on the logical level: logically, the fold
operator is a recursion pattern, just like list_rec and list_case, which
have the logically canonical type of recursion operators. Hence a
library for logical developments should give the fold operator its
logical type. By convention, the function comes first and the constant
comes next (list_rec and list_case swap these). This is the type of
foldl. When I introduced foldr a long time ago I made the mistake of
giving foldr a logically un-canonical type and have no objection if that
is corrected.

Just to summarize:

- There should only be 2 fold functions and their types should be as
discussed above. (If you would like a third one for code generation
purposes, it should be clearly marked as such and be less prominent.)
- If one of them is singled out as "fold", then it should be foldr, not
foldl: "fold" should be the one that leads to simpler proofs, which is
foldr (Brian mentioned this already), not the one that is more efficient
- we are on the logical, not the implementation level.

Thanks
Tobias

> 	Florian
> 
> 
> 
> 
> This body part will be downloaded on demand.