Re: [isabelle] argument order of List.foldr



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





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