Are "logarithm types" a thing?

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 i

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.

StackExchange Computer Science Q#117856, answer score: 7