container-algebra

container-algebra

Yesterday I was reading some fascinating posts on sigfpe's blog A Neighborhood of Infinity. In particular, Fun With Derivatives Of Containers

Fascinating stuff. The rest of this post is going to assume that you have read it, so check out the link.

One part got me blogging: He says "Pity we can't write X.F'[X]-F[X] to mean just the address, but '-' makes no sense in this context". In another place (somewhere) he (or someone) says that neither subtraction nor division

I got to thinking, that's not entirely true. Consider the case of a list from which we intend to pop an element. The input an be any list except the empty list. Following his notation, the type of a list of X's is:

1 + X + X^2 + etc

where '+' is understood as a discriminated union. Or equivalently,

sum(N,0,oo,X^N)

The type of the empty list is '1'. That's actually not specific; 1 is the type of which there can be only one instance. Similarly, a boolean flag is of type 2, an enumerated type of N elements is of time N.

So the possible inputs, list other than empty list, could be written:

sum(N,0,oo,X^N) - 1

And the type of `pop' as

sum(N,0,oo,X^N) - 1 -> sum(N,0,oo,X^N)

It's a little disconcerting that `pop' looks like "+1". When we look at it closer, we see that's not really the case. In type theory, objects don't have identity beyond that of their type signature, so we can't see that all of the objects have moved one place closer to the list head. We can, however, let the upper limit not be infinity but merely approach infinity. Letting M be that limit, we see that `pop's type signature is actually:

sum(N,0,M,X^N) - 1 -> sum(N,0,M-1,X^N)

which we can stretch to write as:

1/X

So we can have some semblance of division!

What's "e"?

Reading thru his other posts on the topic (highly recommended), I find that amazingly, the Taylor series for exponentiation is applicable to container types, ie

exp(X) = 1 + X/1! + X^2/2! + X^3/3! + etc

where a container of the form

X^N/N!

is interpreted as a bag of N elements of type X. The "N!" comes from the fact that they are insensitive to permutations, ie, there are N! ways to compose a list of N elements of type X from those.

So I asked myself, what's the equivalent of "e" in this system? And the answer seems to be,

exp(1) = 1 + 1/1! + 1^2/2! + 1^3/3! + etc

A bag of any number of elements, each of which is void. Amazing.