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
