Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] argument order of List.foldr


view this post on Zulip 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?

view this post on Zulip 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:

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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 -> '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?


Last updated: Mar 28 2024 at 08:18 UTC