foldl and foldr

foldl.com and foldr.com are two fun websites that may just help you wrap your head around left and right folds. They are the product of Oliver Steele, designer of (Open)Laszlo.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Put a smile on my

Put a smile on my face...

Thanks!

Backwards?

Cute, but these seem a bit backwards to me. Every time I click I see the expression expand in the window. It feels more like an unfold. I would have thought that it should work more like

(1+(1+(1+(1+(1+(1)))))))
... click ...
(1+(1+(1+(1+(2)))))
... click ...
(1+(1+(1+(3))))

am I missing something insightful?

It kind of makes sense...

Define

fold f g 0 = g
fold f g (1+n) = f (fold f g n)

(This is a specialisation of a natural generalisation of the usual foldr.)

The third argument to fold is of type ∞ where 1+∞ is isomorphic to ∞ (here '+' means disjoint union and '1' is the type with one instance called '0'). In fact, consider how the function above is evaluated. At each stage in the recursion you have an element of ∞. This is isomorphic to 1+∞. So you either have the base element of the type, 0, or you have an element of ∞ again and you need to recurse further. So clicking on the link precisely models the execution of fold.

At least that's my guess...

fold


Define

fold f g 0 = g
fold f g (1+n) = f (fold f g n)

(This is a specialisation of a natural generalisation of the usual foldr.)

The third argument to fold is of type ∞ where 1+∞ is isomorphic to ∞ (here '+' means disjoint union and '1' is the type with one instance called '0').

The third argument is of type N (where N is a set of natural numbers). There is no need to talk about ∞ at all since ∞ is *not* a natural number unless by ∞ you mean N which it would be non-standard notation.

it would be non-standard notation.

Yes, that's my claim. That foldr.com (1) makes perfect sense and (2) actually has something to do with 'fold' but (3) is using non-standard notation (but not wildly non-standard notation).

Perfect sense

So given:

1+(1+(1+(1+(1+(1+(…))))))=∞

Assuming the standard definition of summation, the expression is aleph_0 (or omega), the cardinality of the natural numbers.

1. How do *you* interpret

1+(1+(1+(1+(1+(1+(…)))))) ?

2.

...∞ is the initial algebra itself

If '...∞ is the initial algebra itself', then

1+(1+(1+(1+(1+(1+(…))))))=∞

is nonsensical. How can a sum of natural numbers be equal to an algebraic structure ?

3. On the other hand, you say that


At each stage in the recursion you have an element of ∞.

which sort of implies that ∞ is a synonym for N (the set of natural numbers). You have to make your mind and decide what ∞ really is because it's unclear what you are talking about.

∞ is a synonym for N

Yes, exactly that. Didn't I make this clear by stating that '1' is the type with 1 element called '0', '+' is disjoint union and '=' is isomorphism? Apologies for any confusion caused if I didn't say those things.

Tne "natural" numbers in

Tne "natural" numbers in Haskell are actually the co-natural numbers. In Haskell, datatypes are greatest fixpoints, so 1 + 1 + 1 ... iterated infinitely is actually a perfectly good term of type Nat. So instead of thinking of Nat as the initial algebra of the functor F(X) = 1 + X, think of it as the final coalegbra. Then you can define ∞ as 1 + 1 + 1 + ..., and you can use coinduction to show that the other terms which ought to be infinite are all equal to this term.

(All this is modulo some domain theoretic considerations I am firmly ignoring.)

Haskel N


Tne "natural" numbers in Haskell are actually the co-natural numbers.

Actually, you can define them both ways:

Inductively:

data Nat = Zero | Succ Nat

or corecursively:

naturals = add 0
add n = n : add (n+1)


So instead of thinking of Nat as the initial algebra of the functor F(X) = 1 + X, think of it as the final coalegbra.

Right, in this case Nat would be {∞} union N, however, the website in question uses foldr which presupposes the inductive definition in which case Nat = N, i.e. Nat does not contain ∞.

= ∞

being a bit pedantic probably but my education as a math teacher is to blame for that.
you can not say =∞ that is just nonsens.

What is the problem with = ∞ ?

Sure, you need to define ∞, but there's a perfectly good definition in this case. In particular, we're probably looking at the F-algebra called N in the wikipedia page here and '=' means isomorphism.

the problem is

Your probably a real mathematician knowing a F algebra called N a high-school teacher here in the Netherlands is not always Drs. . All abstract algebra i ever learned was Groups and body's and a bit of galoise theory and linear algebra so i am probably wrong that is what I get posting here. But i learned there was a problem with just summing to infinity by this example. the row of numbers

1,-1/2,1/2,-1/3,1/3,-1/4,...

you can argue that for every positive term there is a negative term.
so (1-1/2)+(1/2-1/3)+...=1

and because for example 1/8-1/9 = (9-8)/8*9 =1/8*9
so
1/1*2+1/2*3+1/3*4+... = 1

but it is easy to see that 1/2*3 = -1/2+2/3 , 1/3*4 = -2/3+ 3/4 ,...

so 1/1*2+1/2*3+1/3*4+... =0 and that is a problem.
that is why i learned to think of convergence (do i say that right in english) when thinking of summing rows.

Greetings Remco

when being really pedantic

You also must define ∞ . and + and even ... and the number system we are talking about when we start doing algebra maybe it is a kind of finit group + with 0, 1,... and ∞ ?

eureka now i understand

I am a bit slow this time of day i worked all day and doing math is realy some time ago. You mean he is defining somthing like the natural numbers like Peano (was it Peano?). and ∞ means natural numbers or something

Algebra


Sure, you need to define ∞, but there's a perfectly good definition in this case.

Natural numbers can be seen as an initial algebrs of the F(X) = 1 + X functor allright, but how does that define ∞ ?

I'm suggesting that...

...∞ is the initial algebra itself - assuming '1', +' and '=' are what I suggest they mean above. They all seem like reasonable interpretations of the symbols '∞', '1', +' and '=' to me.

Of course we're just trying to divine someone's intentions here...

∞ algebra


...∞ is the initial algebra itself - assuming '1', +' and '=' are what I suggest they mean above. They all seem like reasonable interpretations of the symbols '∞', '1', +' and '=' to me.

If ∞ means the [zero, successor, N] triple/algebra, then 1+2+3+...=∞, does not make sense. Let's agree that 1+2+3+...=∞ is nonsensical ;)

Are we talking at cross purposes

Here is the content of the web site foldr.com after a few clicks: 1+(1+(1+(1+(1+(1+(…))))))=∞

There's no 1+2+3+...=∞ there.

but there is ;)

1+(1+(1+1))+....=
1+1+1+1+....=1+(1+1)+(1+1+1)+... ahhh help all those 1s
or i can say something like for some n element of N there excists 1+1+1 (n times) = equal to 1+2 .... (help this is difficult in ascii) the first sum is the same as the second.

I mean of course the converge to the same thing

I mean of course the converge to the same thing

What's the difference


Here is the content of the web site foldr.com after a few clicks: 1+(1+(1+(1+(1+(1+(…))))))=∞

There's no 1+2+3+...=∞ there

What's the difference ?


being a bit pedantic probably but my education as a math teacher is to blame for that.
you can not say =∞ that is just nonsens.

The expression 1+2+3... = ∞ is clearly nonsensical if ∞ is understood as a natural number. On the other hand, if you define ∞ as a cardinality of some set corresponding to the 1+2+3+..., then such cardinality does exist and is equal omega, the natural numbers cardinality.

cantor

That makes me think of Cantor you say it is infinit and countable.Hey I am starting to remember all that stuf and having fun. But if + is closed than you have a litle problem don't you than ∞ have to be a natural number.

canto


But if + is closed than you have a litle problem don't you than ∞ have to be a natural number.

Right, ∞ is not a natural number unless by ∞ we mean, say, 42 ;)

Yes 42 is definitely the answer

that was a funny book.

Or...

...-1/12.

foldl f = foldr g, solve for g

There's a fun little puzzle for all you aficionados of 'fold': a foldl can be written as a foldr. The reverse is not true -- explain why. Read Erik Meijer's PhD thesis or Google "Graham Hutton" if you experience pain for more than one day.

These things were disucssed

These things were disucssed here quite a few times in the past, so you can just google the archives if you want...

Why don't these work?

I'm not sure whether you're saying that foldr can't be defined in terms of foldr, or the reverse, so here are my attempts at both:

foldl' f b0 as = foldr (\a k b -> k (f b a)) id as b0
foldr' f b0 as = foldl (\k a b -> k (f a b)) id as b0

Lazy

As I understand it, there are problems with your foldr' if as is an infinite list

Cheating

Hmm, I checked my copy of the bananas paper, and indeed, Erik Meijer defines his algebraic data types using lazy products. Didn't notice that on the first read(s)... Isn't it abusing the terminology?
Wasn't the difference between algebraic and coalgebraic exactly that one is defined by (means of) construction, and the other by (means of) destruction? Or am I completely off-track?

That depends in which

That depends in which category your are. In CPO, the category in which Haskell lives, initial algebras and final co-algebras coincide.

If you want to learn more start with this, and then get a copy of Peter J. Freyd's "Recursive Types Reduced to Inductive Types" or do some Googling to track references.

BTW One of our interview questions is to write foldr in terms of foldl and vice versa :-)