Re: [isabelle] argument order of List.foldr



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.






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.