[isabelle] argument order of List.foldr



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





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