Lambda the Ultimate

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

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.

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

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.

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

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

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.

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

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

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

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

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

...∞ 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 ;)

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.

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

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.

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.

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

that was a funny book.

...-1/12.

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

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

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

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