Lambda the Ultimate

Last Friday I gave a talk about differentiating data structures at local student scientific group seminar; but I only read the original Conor McBride paper, I haven't known about this one.

I must admit that I didn't understand fully his approach. What bothers me that I cannot tell if it works also for mutually recursive types, such as

type B = leaf | node(B,C)
and C = leaf | node(C,B,C)

It appears that the one-hole context of such type is not of a form (a' list), but rather a mixed-step-type mutual lists:

B' = nil | (B',C) | (C',B)
C' = nil | (C', (B,C)|(C,B) ) | (B',(C,C))

However, when we convert the type definition to polynomial equation system (converting leaf to x)

B(x) = x + B(x)C(x)
C(x) = x + C(x)B(x)C(x)

and differntiate it, we get

B'(x) = 1 + B'(x)C(x) + C'(x)B(x)
C'(x) = 1 + 2C'(x)B(x)C(x) + B'(x)C(x)^2

which is pretty similar to the type of one-hole context.

To sum up - I wonder if the differentiaion of mutually recursive types is also covered. Perhaps it is, but lacks a good example to explain?

Suppose F[X] is the type of containers of objects of type X. Then consider F[X+E]. This is the type of containers of objects that are either X or E. Suppose we can rewrite F[X+E]=F0[X]+E.F1[X]+E^2.F2[X]+... where the Fi[X] are independent of E. Then the first term in the series should be containers with no E's in them (so we expect F0[X]=F[X]) and the second term corresponds to containers where there is precisely one E instead of an X somewhere in the structure. Remove that E to get the one hole context and we get F1[X]. Elementary calculus shows F1[X]=F'[X].

was differentiating datatypes in 1980. Read
Andre Joyal, Une theorie combinatoire des series formelles, Adv. Math. 42 (1981), 1-82. for the beginnings of this theory, which continue in Andre Joyal, Foncteurs analytiques et especes de structures, in Combinatoire Enumerative, Springer Lecture Notes in Mathematics 1234, Springer, Berlin (1986), 126-159.

But they are not all that easy to read. Instead, I recommend the excellent book
F. Bergeron, G. Labelle, and P. Leroux, Combinatorial species and tree-like structures, Cambridge, Cambridge U. Press, 1998

This has already drawn the attention of many others, John Baez in particular.