Email Gateway (Aug 18 2022 at 14:51): Email Gateway (Aug 18 2022 at 14:51):From: Brian Huffman <brianh@cs.pdx.edu>
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?
Email Gateway (Aug 18 2022 at 14:51):From: Lucas Dixon <ldixon@inf.ed.ac.uk>
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:
Email Gateway (Aug 18 2022 at 14:51):From: Alexander Krauss <krauss@in.tum.de>
Hi Brian,
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 "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:
Email Gateway (Aug 18 2022 at 14:51):From: Brian Huffman <brianh@cs.pdx.edu>
On Sat, Mar 6, 2010 at 10:36 AM, Lucas Dixon <ldixon@inf.ed.ac.uk> wrote:
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 argument order is also nice for combine folds...fold o fold : ('a -> 'b -> 'b) -> 'a list list -> 'b -> 'b
On Sat, Mar 6, 2010 at 12:28 PM, Alexander Krauss <krauss@in.tum.de> wrote:
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).
These are good points. I guess both argument orders have their uses,
in different situations. I suppose I was thinking with a Haskell bias,
since partially-applied foldr is used a lot in Haskell. Also, the
"fold o fold" situation never seems to come up in Haskell either,
since for state transformers people generally use mapM with a state
monad rather than a fold.
Email Gateway (Aug 18 2022 at 14:51):From: Lawrence Paulson <lp15@cam.ac.uk>
This one is used in my ML book. It (and the corresponding foldl) work for lists of lists nested to any depth. E.g.
fun sum_of_sums xss = foldl (foldl op+) (0, xss);
Larry
Email Gateway (Aug 18 2022 at 14:51):From: Tobias Nipkow <nipkow@in.tum.de>
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 -> 'band the type of foldr from Haskell's List library:
foldr :: (a -> b -> b) -> b -> [a] -> bBut 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 -> 'bSince 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
Last updated: Nov 21 2024 at 12:39 UTC