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

### 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.)

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:

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.

...-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 :-)