A set with elements of type $a$ typically is represented in type theory by $Set \ a: a \to bool$ or, as an algebraic expression $Set \ a: 2^a$.
The idea is that, for each element of the type $a$, you ask whether it is a member of your set. $2^a$ counts how many distinct subsets there are. For instance, if our set is $\{1,2,3\}$, we get, as possibilities, the empty set $\{\}$, each individual element $\{1\}, \{2\}, \{3\}$, any two elements $\{2, 3\}, \{1, 3\}, \{1, 2\}$, or the full set $\{1, 2, 3\}$. A total of $2^3=8$ subsets.
Now, due to Conor McBride we know that you can get the one-hole context of any type simply by treating it as an algebraic expression and taking its derivative with respect to its type variables. The resulting data structure is called a zipper. In our case:
$$\frac{d}{da} 2^a = 2^a log(2)$$
or expressed as a type:
$$\partial_a \ a \to 2 = \left(a \to 2, log(2)\right)$$
which basically tells us (or at least me) nothing: The logarithm is completely opaque to interpretation.
So this is my question. How to interpret that expression?
I made some progress on my own though, using the following expression:
$$b^a = \sum_{n=0}^{\infty}{\binom{a}{n}(b-1)^n}$$
where $\binom{a}{n} = \frac{a!}{n!(a-n)!}$ is the usual binomial coefficient.
In particular, if $b=2$, we get:
$$2^a = \sum_{n=0}^{\infty}{\binom{a}{n}}$$
which simply counts the subsets of size n and then sums them up to find all subsets of arbitrary size. For $n>a$ the expression conveniently vanishes.
Here are the first few terms expressed as polynomials:
$$\begin{array}{l|l|l} n & \binom{a}{n} & \text{expanded} \\ \hline 0 & \frac{1}{0!} & 1 \\ 1 & \frac{1}{1!}a & a \\ 2 & \frac{1}{2!}a(a-1) & \frac{1}{2}\left(-a + a^2\right) \\ 3 & \frac{1}{3!}a(a-1)(a-2) & \frac{1}{6}\left(2a - 3a^2 + a^3\right) \\ 4 & \frac{11}{4!}a(a-1)(a-2)(a-3) & \frac{1}{24}\left(-6a+11a^2-6a^3+a^4\right) \end{array}$$
While the expanded form is kind of opaque with weird fractions and negative signs, for the column $\binom{a}{n}$ the interpretation is pretty clear:
- There is only one way to take no elements from $a$ to generate a set. You'll get the empty set.
- There is one way for each $x : a$ to generate a set. You'll get the set $\left\{x\right\}$ for what ever choice $x$ you make.
- There are $a \left(a-1 \right)$ ways to generate a set of two elements $\left\{x, y\right\}$ from $a$: You pick your first element, and then, because sets have no duplicates, you pick your second element from a type $a-1$ which no longer includes your first pick. However, because in sets order doesn't matter, there are always $2!=2$ choices that lead to the same outcome. - You can pick $x$ first and $y$ second, or $y$ first and $x$ second. So then, that choice is ignored by dividing by $2!$.
- etc.
As expected, this also works for when your source type $a$ is smaller than your target set. For instance, attempting to take two elements from the unit type $1$ results in $\frac{1}{2!}1(1-1) = 0$ - there are $0$ ways to do that.
Ok, so with all that out of the way, lets differentiate term-wise by $a$:
$$\frac{d}{da}\binom{a}{n} = \binom{a}{n} \left(H(a) - H(a-n)\right)$$
where $H(j)$ is the $j^\text{th}$ Harmonic number.
Or, simply by applying the product rule to the above table:
$$\begin{array}{l|l|l} n & \frac{d}{da}\binom{a}{n} & \text{expanded} \\ \hline 0 & \frac{0}{0!} & 0 \\ 1 & \frac{1}{1!} & 1 \\ 2 & \frac{1}{2!} \left((a-1) + a \right) & \frac{1}{2}\left(-1 + 2a\right) \\ 3 & \frac{1}{3!}\left((a-1)(a-2) + a(a-2) +a(a-1) \right) & \frac{1}{6}\left(2 - 6a + 3a^2\right) \\ 4 & \frac{11}{4!}(a-1)(a-2)(a-3) + a(a-2)(a-3) + a(a-1)(a-3) + a(a-1)(a-2) & \frac{1}{24}\left(-6+22a-18a^2+4a^3\right) \end{array}$$
That looks fine and dandy, right? Well, there is a problem now. I'm pretty sure these polynomials never ever become integer-valued for any integer. Nor do their summed-up forms. And they even give multiple ways to pick an empty set with no hole.
For instance, take $n=2$ elements from a type $a \cong 3$, leaving one of them a hole:
$$\frac{1}{2!}\left((3-1) + 3 \right) = \frac{5}{2}$$
In principle I read this as: You can either take the hole first and then any of the three values, or you can first take one of the three values, and then a hole with the two possible remaining values, and the order doesn't matter, so divide by 2.
But I think there should still be an integer number of ways to do this, right? Is there any way to make sense of that fraction? Or did I do something wrong here?
If I'm not mistaken, given my type used at the beginning $a = \{1, 2, 3\}$, a 2-element subset with one hole would look something like this:
$$\left\{\_, 1\right\} | \left\{\_, 2\right\} | \left\{\_, 3\right\} | \\ \left\{1, \_ \right\} | \left\{2, \_ \right\} | \left\{3, \_\right\}$$
where the first three expressions have holes of type $a \cong 3$, the last three of type $a-1 \cong 2$ (after removing the appropriate element), but they are also paired up, each of the top line with the one below it.
The closest to interpreting $\frac{5}{2}$ I got is that, ignoring the no order constraint, we're dealing with something of type $3 + 2$ - that is $3 \ or\ 2$ - for the hole and, perhaps, the constraint can only be fulfilled once the hole is filled back in? But that doesn't yet resolve how there apparently can be several ways - even "negative" ways - to get a hole from an empty set or similar such problems.