Are “logarithm types” a thing?

Question

I'm attempting to formalize some thoughts I've had about paths into data structures. For example, a path into a list of Ts might be a pair of an index with a path into a T; a path into a pair (A, B) would be the tagged union of a path into A or a path into B. Think of a path as a way to specify some small (atomic?) piece of a larger data structure—not unlike a lens, but here I'm emphasizing the structural decomposition of a data type as opposed to an arbitrary computation that satisfies the lens laws (maybe every path is usable as a lens, but not every lens corresponds to a path).

Strictly speaking, my first example about lists of Ts is a little sloppy, since a path into such a list l should have its index bounded by the length of l. The pair (Nat, path T) is more properly a path into an infinite list of Ts—or, equivalently, a path into a function Nat -> T.

So my first interesting observation is that I have an operator that turns exponentials into products and products into sums in a way that's awfully reminiscent of logarithms:

path (T^Nat) = Nat * (path T)
path (A * B) = path A + path B

That got me thinking about whether there's an exp T type as well. Leaving aside all restraint and sense of rigor, the terms of the usual series expansion for $e^x$ offer a hint:

$$e^x = \sum_{n\ge0} \frac {x^n} {n!}$$

A type-theory interpretation of $\frac {x^n} {n!}$ might be a bag (as in multiset) of $x$s of size $n$ (it's an $n$-tuple $x^n$ but we don't care about the $n!$ ways the tuple can be ordered), so then a value of type $e^x$ would be a bag of $x$s of any size.

So if bag and path might be inverses, then that's saying something like, the type of all bags of paths into a type T, if it exists, is isomorphic to T. For example, there's an obvious isomorphism between (bag A) * (bag B) and bag (A + B) (an isomorphism that doesn't work if you replace bag with list or set or some other collection type, which reinforces my intuition that bag is the correct interpretation of $e^x$).

Of course, this is all appealing-sounding nonsense. I haven't even formally defined what a path is, never mind all the abuses involved in pretending the series expansion of $e^x$ is an algebraic data type. path may also be an idea of limited use, since it's not at all clear to me what to think about something like path (A + B) or path Bool. But has anyone made a more careful study of these ideas? Searching for "type theory" or "algebraic data types" along with "logarithms", "paths", "bags", "multisets", etc. hasn't yielded anything like what I'm attempting to describe here.

Answer 1

Logarithm types are definitely a thing and have been noticed before by a number of people. In functional programming, a Type -> Type functor has a logarithm if it's representable, and then the logarithm is the representing object. See also this, this, and this. You are correct about the exponential functor being the bag functor, see e.g. this, where it's described as the fixed point of the derivative operation on endofunctors.

Answer 2

In addition to András' answer, there's one thing you might want to be aware of with all this. I think it's not well known, because although I noticed it many years ago, I haven't really talked about it with many people.

Basically, if you think about some finite arithmetic behind the arithmetic of types, and compare it to some of the power series formula type stuff, what you get won't actually make sense. For instance, you'll probably come across the booleans written as $\mathbf 2$, because it has two values. Now, if you write down the formula for unordered pairs, you'll say: $$\frac{2^2}{2!} = 2$$ and expect the unordered pairs of booleans to be isomorphic to the booleans. But this is actually wrong; there are three unordered pairs: $$\{0,0\}, \{0,1\}, \{1,1\}$$

The reason for this is that when we deal with actual types, we are either over-counting the relevant permutations, or under-counting some of the values relative to their representation in terms of combinatorial species. In terms of the permutations, there is a permutation between $(0,1)$ and $(1,0)$, but $(0,0)$ and $(1,1)$ cannot be permuted into distinct ordered pairs. In terms of values, there are actually two ways we could imagine representing $(0,0)$ in terms of distinct labellings:

$$((x, y), \{x → 0, y → 0\}) \\ ((y, x), \{x → 0, y → 0\})$$

And same for $(1,1)$. This comes from the study of species, where instead of constructions directly on types, one thinks primarily about combining different shapes of labelled trees, and then mapping the labels to the values that should occur at the labelled position. The discrepancy comes because with species, we usually consider structures where each position is distinctly labelled, like $(0,1)$, whereas with types you can have degenerate labellings that don't require a permutation to eliminate redundancies.

It is still true that in e.g. Conor McBride's answer linked in András' answer, the type of unordered pairs is something like $2^2/S_2$ as some sort of type theoretic quotient by permutations. Just, some of the quotienting will be redundant, so you cannot do straight integer arithmetic to count the number of resulting values. Another example of this would be getting the answer: $$ℕ = e$$ by plugging in $\mathbf 1$ for $x$ in the power series. However, all the permutations are redundant in that case. (There is a different notion where this does work, though, here.)

It is possible to work out a formula that works for counting the values of unordered pairs of finite types. I think the easiest way to do it is to think in terms of total orders of the finite types, and ordered tuples that must also have ordered components. So $(0,0), (0,1), (1,1)$. You can represent $n$-tuples of finite types with size $k$ by having $n$ dots with $k-1$ marks interspersed, where the marks indicate when you should move to successive values. So the above pairs are: $$\cdot\cdot|\\ \cdot|\cdot\\ |\cdot\cdot$$ I forget the formula for this, but it's something like $n+k-1 \choose n$ or similar.