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