Conor McBride has a beautiful functional pearl, “Clowns to the Left of me, Jokers to the Right”, in which he discusses the idea of suspending the computation of a catamorphism. I just wanted to point out the relation of his work to the -derivative. Since Star Trek’s character Q is a trickster god like Loki, Anansi, or Coyote, -derivatives also fit nicely with McBride’s theme.
The usual definition of the derivative is
Instead of translating by an infinitesimal amount , we can scale by an infinitesimal amount ; these two definitions coincide in the limit:
However, when people talk about the -derivative, they usually mean the operator we get when we don’t take the limit and . It should probably be called the “-difference”, but we’ll see that the form of the difference is so special that it deserves the exceptional name.
The -derivative, as one would hope, behaves linearly:
Even better, the -derivative of a power of is separable into a coefficient that depends only on and a single smaller power of :
Clearly, as , . Whereas counts the number of ways to insert a point into an ordered list of items, counts the number of ways to insert a linearly independent ray passing through the origin into an -dimensional vector space over a field with elements with a given ordered basis.
The -derivative even works when is an operator rather than a number. Polynomials work in any rig, so if is, say, a function instead of a number, could be the Fourier transform.
Let’s lift this to types. The derivative of a datatype is the type of its one-holed contexts, so we expect the -derivative to have a similar interpretation. When we take and to be types, the -derivative of a tuple is
Each option factors into two parts: the ‘clowns’ are a power of to the left of the hole, followed by the ‘jokers’, a power of after the hole. This type is the one we expect for the intermediate state when mapping a function over the tuple; any function can be lifted to such a function .
Similarly, the -derivative of the list datatype is ; that is, the ‘clowns’ form the list of the outputs of type for the elements that have already been processed and the ‘jokers’ form the list of the elements yet to process.
When we abstract from thinking of as a number to thinking of it as an operator on ring elements, the corresponding action on types is to think of as a functor. In this case, is not a pair type, but rather a parametric type . One might, for example, consider mapping the function over a list of real numbers. The resulting outputs will be real except when the input is zero, so we’ll want to adjoin an undefined value. Taking , the -derivative of is , consisting of the list of values that have already been processed, followed by the list of values yet to process.