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

[Florian Haftmann]

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

a) History: The fold in HOL-Library has been introduced by me at some
stage to accomplish various definitions and lemmas relating lists and
sets.  Using foldl just exposed to many pain.

The movement of the code setup for sets into the HOL-Main corpus also
brought this fold into List.thy.

In the light that the corresponding code equations prefer foldr anyway
for the sake of tail recursion,  it could have been conceivably more
appropriate to use foldr right from the beginning.

b) Purpose: The main idea was to use the relation between
Finite_Set.fold and fold to lift various operations on sets to lists.
So, fold is indeed used as a recursion combinator, and experience
suggests that is hardly any other use (cf. the inherent problems with
function specification with a fold combinator at their right hand side).
Giving a definition like
  "sort_key f xs = foldr (insort_key f) xs []"
it is best to provde simp rules for sort_key afterwards immediately, to
obtain usable automation-
Here again foldr is the preferred combinator again.

c) Pervasiveness: Beside the list fold, there are also folds on dlists
and rbts (maybe more) which have to be considered.

d) Relation of fold and foldr:
  "foldr f xs = fold f (rev xs)"
This is a straightforward correspondence, which can't be expressed that
neatly for fold combinators which different argument order.

So what to do?  In the light of d), I would even suggest to provide only
*one* fold combinator as constant, and the other one as abbreviation
(and also code abbreviation).  a) and b) would suggest that the proper
constant would be foldr rather than fold.  Then the set of lemmas needed
would reduce drastically.

I still argue that the argument order of fold is more appropriate than
that of foldl for many standard applications,
Nominal/Examples/Standardization.thy being an example to the notable
exception of abstract term structures).

Anyway, personally I have no strong opinion about this, so anybody who
wants to get hands on should feel invited to do so.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20120212/9a7ddb64/attachment.asc>