23
$\begingroup$

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?

Improve this question
$\endgroup$
5
  • 5
    $\begingroup$ There is in the theory of combinatorial species, and there it corresponds to the species of (finite) sets, but that doesn't correspond to an algebraic data type. $\endgroup$ – Derek Elkins left SE May 26 '17 at 1:41
  • 1
    $\begingroup$ What do you mean by "equal"? In your world, are $(S + T) \to U$ and $(S \to U) \times (T \to U)$ equal? How about $\mathbb{N}$ and $\mathsf{List}(\mathbb{N})$? $\endgroup$ – Andrej Bauer May 26 '17 at 14:30
  • 1
    $\begingroup$ @AndrejBauer The former yes, the latter no. $\mathsf{List}(\mathbb{N})$ is equal to the iterated product $1 + \mathbb{N} + \mathbb{N} \times \mathbb{N} + \mathbb{N} \times \mathbb{N} \times \mathbb{N} + \ldots = \sum_{n=0}^{\infty} \mathbb{N}^{n}$ in my mind. That said, I do not have a rigorous model of type equality in my mind, and if you have a model you can point me at I'd be happy to read it. $\endgroup$ – Matthew Piziak May 26 '17 at 14:59
  • 3
    $\begingroup$ @DerekElkins as it happens, another article by McBride, called Clowns to the Left of me, Jokers to the Right points out that, "For finite structures, [the iteration of an operator on zippers] gives rise to a power series formulation of datatypes directly, finding all the elements left-to-right....There is thus a significant connection with the notion of combinatorial species". So I would not be surprised if combinatorial species has some interesting role to play in the context of this question as well. $\endgroup$ – Matthew Piziak May 26 '17 at 20:31
  • $\begingroup$ @MatthewPiziak They definitely do. Brent Yorgey has talked about this quite a bit. See also his thesis. $\endgroup$ – Derek Elkins left SE May 26 '17 at 20:56
18
$\begingroup$

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.

Improve this answer
$\endgroup$
2
  • $\begingroup$ The original author appears! Thank you for stopping in to show us this beautiful result. $\endgroup$ – Matthew Piziak May 28 '17 at 22:27
  • $\begingroup$ The intuition of bags being exponentials is very nice. Especially since a bag can be represented as the function space $X\rightarrow\mathbb{N}$ (every element has a count), giving $\mathbb{N}^X$. Though I'm not sure how the base plays a role! Hesitant to say that $\mathbb{N}$ is the "natural" base of exponential types... $\endgroup$ – bitconfused May 30 '20 at 17:50
3
$\begingroup$

How about the infinite sum $$\sum_{i, j \in \mathbb{N}} X^i ?$$ The derivative is $$\sum_{i, j \in \mathbb{N}} \underbrace{X^i + \cdots + X^i}_{i+1}$$ which is equal to the original by associativity and commutativity of sums.

Also, the infinite sum is equal to $\sum_{j \in \mathbb{N}} \mathsf{List}(X)$), so we could try to calculate the derivative using lists.

Improve this answer
$\endgroup$
3
  • $\begingroup$ The derivative of a list is a pair of lists (prefix times suffix). By the sum rule, the derivative of a list of lists is a list of list pairs. Is a list of list pairs isomorphic to a list of lists? $\endgroup$ – Matthew Piziak May 26 '17 at 20:10
  • $\begingroup$ @MatthewPiziak Perhaps it's easier to think of the first formulation as $\sum_{i\in \mathbb{N}} \mathbb{N}\times X^i$. Taking the derivative, we get $\sum_{i\in \mathbb{N}} i\times \mathbb{N}\times X^i$ (with the obvious meaning for $i$). Now, we only need $\mathbb{N}\simeq i\times \mathbb{N}$. To me, this looks a bit similar to (very informally) $e^x = \sum_i x^i/n!$, except the coefficients of the power series are chosen to be $+\infty$ (i.e., $\mathbb{N}$), so that they can satisfy $a_{n} = (n+1) \cdot a_{n+1}$ in a world without division. $\endgroup$ – chi May 26 '17 at 20:17
  • $\begingroup$ @MatthewPiziak Oops, I wrote $n$ instead of $i$, but I think it's clear what I meant. $\endgroup$ – chi May 26 '17 at 20:23

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.