*To*: Alexander Krauss <krauss at in.tum.de>*Subject*: Re: [isabelle] argument order of List.foldr*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Sun, 07 Mar 2010 09:33:46 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, Brian Huffman <brianh at cs.pdx.edu>*In-reply-to*: <4B92BAD6.3040509@in.tum.de>*References*: <cc2478ab1003061009r64142752u7d2d64a7d128953c@mail.gmail.com> <4B92BAD6.3040509@in.tum.de>*User-agent*: Thunderbird 2.0.0.23 (Macintosh/20090812)

> as far as I know, the folds in the List theory, as well as > Library.foldl/foldr in ML are memories from a distant past... they are > just what they happen to be, but there is no "why". The "why" is Larry's book. I took it from there. Tobias > The "one and only true fold" is the "fold" of ML, with variant fold_rev. > But it is not so much folding a binary operation like "+" but more an > iteration of a transformation of a state. But it is the only version > that composes (fold o fold). > > Alex > > > Brian Huffman wrote: >> Here is the type of List.foldr from the Standard ML basis library: >> val foldr : ('a * 'b -> 'b) -> 'b -> 'a list -> 'b >> >> and the type of foldr from Haskell's List library: >> foldr :: (a -> b -> b) -> b -> [a] -> b >> >> But List.foldr in Isabelle has this type: >> foldr :: "('a => 'b => 'b) => 'a list => 'b => 'b" >> >> Why are the arguments in that order? >> >> The standard argument order would be much more useful for partial >> application. >> >> Maybe it is based on Isabelle's Library.foldr, which has this type: >> Library.foldr : ('a * 'b -> 'b) -> 'a list * 'b -> 'b >> >> Since it has an uncurried type, the argument order doesn't make any >> difference here as far as partial application is concerned, and I >> recognize that there is a mnemonic benefit to this argument order: >> Library.foldr (op +) ([1,2,3], 4) = 1 + (2 + (3 + 4)) >> >> But I think that being amenable to partial application is more important. >> >> Does anyone else have an opinion on this? >> >> - Brian >

**References**:**[isabelle] argument order of List.foldr***From:*Brian Huffman

**Re: [isabelle] argument order of List.foldr***From:*Alexander Krauss

- Previous by Date: [isabelle] Question about classes
- Next by Date: Re: [isabelle] Question about classes
- Previous by Thread: Re: [isabelle] argument order of List.foldr
- Next by Thread: Re: [isabelle] argument order of List.foldr
- Cl-isabelle-users March 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list