*To*: Brian Huffman <brianh at cs.pdx.edu>*Subject*: Re: [isabelle] argument order of List.foldr*From*: Lucas Dixon <ldixon at inf.ed.ac.uk>*Date*: Sat, 06 Mar 2010 18:36:25 +0000*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <cc2478ab1003061009r64142752u7d2d64a7d128953c@mail.gmail.com>*References*: <cc2478ab1003061009r64142752u7d2d64a7d128953c@mail.gmail.com>*User-agent*: Thunderbird 2.0.0.22 (X11/20090625)

I really like Isabelle's argument-order for fold; in particular I frequently fold over list in order to update some value: a |> fold f l |> fold f2 l2 This is intuitively updating the value of "a" and using each value of "l" and "l2". This argument order is also nice for combine folds... fold o fold : ('a -> 'b -> 'b) -> 'a list list -> 'b -> 'b In my applications, I've rarely had has use for other argument orderings. But perhaps we should have a fold' it haskel style? (incidentally, looking at my version of Isabelle from Feb 23, [changeset 35329:cac5a37fb638], I have: List.foldr : ('a * 'b -> 'b) -> 'b -> 'a list -> 'b fold : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b) best, lucas 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 > > -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.

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

- Previous by Date: [isabelle] argument order of List.foldr
- Next by Date: Re: [isabelle] argument order of List.foldr
- Previous by Thread: [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