At Hac Phi a few weekends ago (which, by the way, was awesome), Dan Doel told me about a certain curiosity in type algebra, and we ended up working out a bunch more details together with Gershom Bazerman, Scott Walck, and probably a couple others I’m forgetting. I decided to write up what we discovered. I have no idea what (if any) of this is really novel, but it was new to me at least.

## The Setup

I’ll assume you’re already familiar with the basic ideas of the algebra of types— represents the void type, represents the unit type, sum is tagged union, product is (ordered) pairing, and so on.

Given a type , since product represents pairing, we can write to represent ordered -tuples of values. Well, how about *unordered* -tuples of values? Since there are possible ways to order values, it seems that perhaps we could somehow divide by to "quotient out" by the symmetries we want to disregard: .

If you’ve never seen this sort of thing before it is certainly not at all obvious that this makes any sense! But bear with me for a minute. At the very least, we can say that if this is to make sense we ought to be able to use these sorts of type expressions to calculate the *number of inhabitants* of a finite type. So, let’s try it. For now let’s take = `Bool`

= . I’ll draw the elements of `Bool`

as and .

There are clearly four different ordered pairs of `Bool`

:

is supposed to represent ordered -tuples of , and indeed, . How about unordered pairs? Since we don’t care about the order I’ll just choose to canonically sort all the s to the front, followed by all the s. It’s not hard to see that there are three unordered pairs of `Bool`

:

(To distinguish them from ordered tuples, I’ll draw unordered tuples as above, with the elements slightly separated and a gray circle drawn round them.)

However, when we substitute into , we get not , but . What gives?

## The problem

The problem is that is only correct if all the values in the tuples are *distinct*. Then we overcount each unordered tuple by exactly a factor of —namely, all the many permutations of the tuple, each of which is distinct as an ordered tuple. However, when some of the tuples have repeated elements, there can be fewer than distinct ordered variants of a given unordered tuple. For example, the unordered tuple has only (rather than ) ordered variants, namely

because the two ‘s are identical.

(As a small aside, when working in the theory of *combinatorial species* one is concerned not with actual data structures but with data structure *shapes* full of distinct *labels*—and the fact that the labels are distinct means that is (in some sense) actually the correct way to talk about unordered tuples within the theory of species. More on this in another post, perhaps.)

If is not the correct expression for unordered tuples, what is? In fact, Dan started off this whole thing by telling me the answer to this question—but he didn’t understand *why* it is the answer; we then proceeded to figure it out. For the purposes of pedagogy I’ll reverse the process, working up from first principles to arrive at the answer.

## Counting unordered tuples

The first order of business is to count unordered tuples. Given a set , how many unordered -tuples are there with elements drawn from (where repetition is allowed)? Again, since the order doesn’t matter, we can canonically sort the elements of with all copies of the first element first, then all copies of the second element, and so on. For example, here is an unordered -tuple with elements drawn from , , , :

Now imagine placing "dividers" to indicate the places where changes to , changes to , and so on:

(Note how there are two dividers between the last and the first , indicating that there are no occurrences of .) In fact, given that the elements are canonically sorted, it is unnecessary to specify their actual identities:

So, we can see that unordered -tuples with elements from correspond bijectively to such arrangements of eight dots and three dividers. In general, unordered -tuples are in bijection with arrangements of dots and dividers, and there are as many such arrangements as ways to choose the positions of the dividers from among the total objects, that is,

(As an aside, this is the same as asking for the number of ways to place indistinguishable balls in distinguishable boxes—the balls in box indicate the multiplicity of element in the unordered -tuple. This is #4 in Gian-Carlo Rota’s "twelvefold way", and is discussed on page 15 of Richard Stanley’s *Enumerative Combinatorics*, Volume I. See also this blog post I wrote explaining this and related ideas).

## So what?

And now for a little algebra:

The expression on top of the fraction is known as a *rising factorial* and can be abbreviated . (In general, , so .) In the end, we have discovered that the number of unordered -tuples of is , which looks surprisingly similar to the naïve but incorrect . In fact, the similarity is no coincidence, and there are good reasons for using a notation for rising factorial similar to the notation for normal powers, as we shall soon see.

And indeed, the correct type expression for unordered -tuples of values from is . This means that if we consider the set of ordered -tuples where the first element is drawn from , the second element from plus some extra distinguished element, the third from plus two extra elements, and so on, there will be exactly of them for every unordered -tuple with elements drawn from . (In fact, we would even expect there to be some nice function from these "extended -tuples" to unordered -tuples such that the preimage of every unordered -tuple is a set of size exactly —just because combinatorics usually works out like that. Finding such a correspondence is left as an exercise for the reader.)

## A detour

Before we get back to talking about , a slight detour. Consider the variant type expression , where is a *falling factorial*. What (if anything) does it represent?

Subtraction of types is problematic in general (without resorting to virtual species), but in this case we can interpret as an ordered -tuple with *no duplicate values*. We can choose any element of to go first, then any but the first element to go second, then any but the first two, and so on. This can in fact be made rigorous from the perspective of types, without involving virtual species—see Dan Piponi’s blog post on the subject.

## Infinite sums and discrete calculus

And now for some fun. If we sum over all , it ought to represent the type of unordered tuples with distinct values of any length—that is, the type of sets over .

Can we find a more compact representation for ?

Consider the *forward difference* operator , defined by

This is a discrete analogue of the familiar (continuous) differentiation operator from calculus. (For a good introduction to discrete calculus, see Graham *et al.*‘s *Concrete Mathematics*, one of my favorite math/CS books ever. See also the Wikipedia page on finite differences.) For our purposes we simply note that

(proving this is not hard, and is left as an exercise). This is what justifies the notation for falling factorial: it is in some sense a discrete analogue of exponentiation!

The reason to bring into the picture is that given the above identity for applied to falling factorials, it is not hard to see that is its own finite difference:

Expanding, we get and hence . (Yes, I know, there’s that pesky subtraction of types again; in the time-honored tradition of combinatorics we’ll simply pretend it makes sense and trust there is a way to make it more formal!) Solving this recurrence together with the initial condition yields

which we can interpret as the space of functions from to `Bool`

—that is, the type of sets over , just like it should be! (Note that replacing falling factorial with exponentiation yields something which is its own derivative, with a solution of —which indeed represents the *species* of sets, though it’s harder to see what has to do with anything.)

Enough with the detour. What if we sum over ?

There’s a *backward difference* operator, , with the property that

Hence , *i.e.* , but here I am a bit stuck. Trying to solve this in a similar manner as before yields , which seems bogus. is certainly not a solution, since . I think in this case we are actually not justified in subtracting from both sides, though I’d be hard-pressed to explain exactly why.

Intuitively, ought to represent unordered tuples of of any length—that is, the type of *multisets* over . This is isomorphic to the space of functions , specifying the multiplicity of each element. I claim that is in fact a solution to the above equation—though I don’t really know how to *derive* it (or even what it really means).

The middle step notes that if you take one element away from the natural numbers, you are left with something which is still isomorphic to the natural numbers. I believe the above can all be made perfectly rigorous, but this blog post is already much too long as it is.

I think the problem is that equation for M(T) involving an infinite sum cannot be interpreted as a power series, nor can the result we’re trying to prove – that M(T)=N^T – be interpreted combinatorially. (For S(T) the corresponding equation and results can be).

Lets lean on a simplified analogy: (2+4) / 6 equals 1, which is in some sense a statement purely about integers: the only operations in the statement are + and division, and the division only appears in an instance where you don’t leave the ring of integers. But we want to derive this statement by temporarily leaving the ring of integers: (2+4)/6 = 2/6 + 4/6 = 1. The middle expression steps outside the integers into the rationals. Our demand for justification is satisfied since the steps are legal steps for rational numbers. We turn around at the end and say that we started and ended with integer expressions, so we’ve discovered a true equality about integers too.

With both species and types you can’t make sense of subtraction. If you want to subtract them – not for the backwards difference even, just for the rising factorial – then the only thing to do is to “step outside” and end up in the ring of power series instead. But once there you meet rules you are stuck with, like not being able to take infinite sums without restriction.

Types (unlike both species and power series) somehow don’t have this problem with infinite sums though. Our infinite sum of types is just taking infinite disjoint unions of sets (in my mind at least, I’m hazy on how type expressions are formalized.) So the venn diagram of “stepping outside” types into power series is different, one sort of expressions doesn’t subsume the other! I don’t think I’ve ever noticed that.

I think I can derive the N^T solution, but this is after the fact..so who knows.

M(T) – M(T-1) = M(T)

Add M(T-1) to both sides.

M(T) = M(T) + M(T-1) which we can use as a recursion to build M(T).

M(0) = 1

M(1) = M(1) + 1 ~=~ N = N + 1 (I.e. e in M(1) looks like S (S (S… (S O) )

M(2) = M(2) + M(1) ~=~ (i.e. e in M(2) looks like S2 (S2…(S2 (S (S ..(S O) )

So for any finite type its easy..not sure if this actually lets you define M (n) for non finite types..but the identification of exponent and function makes it least sort of obvious.

Hmm..yeah I think you have to handwave that because even for N the recusion fails to define it usefully. M(N) = M(N) + M(N-1) = M(N) + M(N) is true but not ?constructive?/?constraining? (not sure what the right word here is.

Though maybe some sort of argument by continuity on ordinals or something similar could work?

Pingback: Creating documents with embedded diagrams | blog :: Brent -> [String]

There’s a significant difference between N^T and the sum of rising factorials you give. The sum gives the finite multisets but N^T allows infinite multisets. For example const 1 is an element of N^T but isn’t an element of any of the terms in the sum.

Anyway, it’s cool you’re thinking about these things. I think there’s an enormous area of combinatorial type theory waiting to be explored.

If you haven’t already, check out “umbral calculus”. It’s all about families of polynomials with associated derivative-like operators such as rising factorials with backward differences. Many theorems about ordinary calculus carry over to umbral calculus and I think many of these theorems get type interpretations.

And note also that Conor McBride’s Jokers and Clowns papers is actually about finite differences, though he doesn’t say it.

So suppose you have a bunch of polynomials with associated derivative-like operator. You can also define an associated exponential-like operator from the power-like series and it will also be a fixed point of the derivative-like operator.

For ordinary monomials x^n you get e^x. For falling factorials you get 2^x. For rising factorials you get N^x.

I am enjoying this type of discussion, and would like to contribute some links. Firstly, these two articles touch on much the same stuff

http://blog.sigfpe.com/2007/09/type-of-distinct-pairs.html

http://blog.sigfpe.com/2007/09/tries-and-their-derivatives_08.html

Nice post!

The sum of the first $k + 1$ terms of $M(T)$ is $(T+1)^{\overline{k}/k!$.

Hence $M(T) = (T+1)^{\overline{T}}/T!$.

Proof: Consider adding a “spacer” element to $T$, and then compute the number of unordered $T$-tuples of these $T+1$ elements, that is, $(T+1)^{\overline{T}}/T!$.