I'm attempting to formalize some thoughts I've had about paths into data structures. For example, a path into a list of T
s 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 T
s 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 T
s—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.