patternModerate
Is there a non-trivial type which is equal to its own derivative?
Viewed 0 times
derivativenonequaltypetrivialitsownwhichthere
Problem
An article called The Derivative of a Regular Type is its Type of One-Hole Contexts shows that the "zipper" of a type—its one hole contexts—follow the differentiation rules in type algebra.
We have:
\begin{align}
\partial_x x &\mapsto 1 \\
\partial_x 0 &\mapsto 0 \\
\partial_x 1 &\mapsto 0 \\
\partial_x (S + T) &\mapsto \partial_x S + \partial_x T \\
\partial_x (S\times T) &\mapsto \partial_xS \times T + S \times \partial_x T
\end{align}
We can use this model to derive that the derivative of unit is void, that the derivative of list is a product of two lists (prefix times suffix), and so on.
A natural question to ask is, "what type is its own derivative?" Of course we already have $\partial_x 0 \mapsto 0$, which tells us that void (the uninhabited type) is its own derivative, but that is not very interesting. It is the analog of the fact that the derivative of zero is zero in the ordinary infinitesimal calculus.
Are there other solutions to the equation $\partial_x T \mapsto T$? In particular, is there an analog of $\partial_x e^x = e^x$ in type algebra? Why or why not?
We have:
\begin{align}
\partial_x x &\mapsto 1 \\
\partial_x 0 &\mapsto 0 \\
\partial_x 1 &\mapsto 0 \\
\partial_x (S + T) &\mapsto \partial_x S + \partial_x T \\
\partial_x (S\times T) &\mapsto \partial_xS \times T + S \times \partial_x T
\end{align}
We can use this model to derive that the derivative of unit is void, that the derivative of list is a product of two lists (prefix times suffix), and so on.
A natural question to ask is, "what type is its own derivative?" Of course we already have $\partial_x 0 \mapsto 0$, which tells us that void (the uninhabited type) is its own derivative, but that is not very interesting. It is the analog of the fact that the derivative of zero is zero in the ordinary infinitesimal calculus.
Are there other solutions to the equation $\partial_x T \mapsto T$? In particular, is there an analog of $\partial_x e^x = e^x$ in type algebra? Why or why not?
Solution
Consider the finite multisets $\mathbf{Bag}\:X$. Its elements are given by $\{x_1,\ldots,x_n\}$ quotiented by permutations, so that $\{x_1,\ldots,x_n\}=\{x_{\pi 1},\ldots,x_{\pi n}\}$ for any $\pi\in\mathbf{S}_n$. What is a one-hole context for an element in such a thing? Well, we must have had $n>0$ to select a position for the hole, so we are left with the remaining $n-1$ elements, but we are none the wiser about which is where. (That's unlike lists, where choosing a position for the hole cuts one list into two sections, and the second derivative cuts selects one of those sections and cuts it further, like "point" and "mark" in an editor, but I digress.) A one-hole context in a $\mathbf{Bag}\:X$ is thus a $\mathbf{Bag}\:X$, and every $\mathbf{Bag}\:X$ can arise as such. Thinking spatially, the derivative of $\mathbf{Bag}\:X$ ought to be itself.
Now,
$$\mathbf{Bag}\:X = \sum\limits_{n\in\mathbb{N}}X^n/\mathbf{S}_n$$
a choice of tuple size $n$, with a tuple of $n$ elements up to a permutation group of order $n!$, giving us exactly the power series expansion of $e^x$.
Naively, we can characterize container types by a set of shapes $S$ and a shape-dependent family of positions $P$:
$$\sum\limits_{s:S}X^{(P\,s)}$$
so that a container is given by a choice of shape and a map from positions to elements. With bags and the like, there's an extra twist.
The "shape" of a bag is some $n\in\mathbb{N}$; the "positions" are $\{1,\ldots,n\}$, the finite set of size $n$, but the map from positions to elements must be invariant under permutations from $\mathbf{S}_n$. There should be no way to access a bag that "detects" the arrangement of its elements.
The East Midlands Container Consortium wrote about such structures in Constructing Polymorphic Programs with Quotient Types, for Mathematics of Program Construction 2004. Quotient containers extend our usual analysis of structures by "shapes" and "positions" by allowing an automorphism group to act on the positions, allowing us to consider structures such as unordered pairs $X^2/2$, with derivative $X$. An unordered $n$-tuple is given by $X^n/n!$, and its derivative (when $n>0$ is an unordered $n-1$ tuple). Bags take the sum of these. We can play similar games with cyclic $n$-tuples, $X^n/n$, where choosing a position for the hole nails the rotation to one spot, leaving $X^{n-1}$, a tuple one smaller with no permutation.
"Type division" is hard to make sense of in general, but quotienting by permutation groups (as in combinatorial species) does make sense, and is fun to play with. (Exercise: formulate a structural induction principle for unordered pairs of numbers, $\mathbb{N}^2/2$, and use it to implement addition and multiplication so that they're commutative by construction.)
The "shapes-and-positions" characterization of containers imposes finiteness on neither. Combinatorial species tend to organised by size, rather than shape, which amounts to collecting terms in and computing the coefficient for each exponent. Quotient-containers-with-finite-position-sets and combinatorial species are basically different spins on the same substance.
Now,
$$\mathbf{Bag}\:X = \sum\limits_{n\in\mathbb{N}}X^n/\mathbf{S}_n$$
a choice of tuple size $n$, with a tuple of $n$ elements up to a permutation group of order $n!$, giving us exactly the power series expansion of $e^x$.
Naively, we can characterize container types by a set of shapes $S$ and a shape-dependent family of positions $P$:
$$\sum\limits_{s:S}X^{(P\,s)}$$
so that a container is given by a choice of shape and a map from positions to elements. With bags and the like, there's an extra twist.
The "shape" of a bag is some $n\in\mathbb{N}$; the "positions" are $\{1,\ldots,n\}$, the finite set of size $n$, but the map from positions to elements must be invariant under permutations from $\mathbf{S}_n$. There should be no way to access a bag that "detects" the arrangement of its elements.
The East Midlands Container Consortium wrote about such structures in Constructing Polymorphic Programs with Quotient Types, for Mathematics of Program Construction 2004. Quotient containers extend our usual analysis of structures by "shapes" and "positions" by allowing an automorphism group to act on the positions, allowing us to consider structures such as unordered pairs $X^2/2$, with derivative $X$. An unordered $n$-tuple is given by $X^n/n!$, and its derivative (when $n>0$ is an unordered $n-1$ tuple). Bags take the sum of these. We can play similar games with cyclic $n$-tuples, $X^n/n$, where choosing a position for the hole nails the rotation to one spot, leaving $X^{n-1}$, a tuple one smaller with no permutation.
"Type division" is hard to make sense of in general, but quotienting by permutation groups (as in combinatorial species) does make sense, and is fun to play with. (Exercise: formulate a structural induction principle for unordered pairs of numbers, $\mathbb{N}^2/2$, and use it to implement addition and multiplication so that they're commutative by construction.)
The "shapes-and-positions" characterization of containers imposes finiteness on neither. Combinatorial species tend to organised by size, rather than shape, which amounts to collecting terms in and computing the coefficient for each exponent. Quotient-containers-with-finite-position-sets and combinatorial species are basically different spins on the same substance.
Context
StackExchange Computer Science Q#75896, answer score: 18
Revisions (0)
No revisions yet.