Differentiating Data Structures

This paper was mentioned here before, but not on the home page.

It deserves to get more attention, since it is quite cool.

Warning: This one isn't for the faint of heart, and uses scary terms like polynomial functors, initial algebras and terminal coalgebras, constructive set theory and more...

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Mutually recursive types

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?

mutually recursive datatypes

.. are a special instance of nested types. e.g. your type
can be written as
B(x) = mu Y.X+mu C.X+CxBxC
and similar for C(x). However, it may be worthwhile to spell out the rules for mutual types directly. Have a go!

An informal explanation...

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].

Andre Joyal...

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.

I'm glad to hear this is a go

I'm glad to hear this is a good book -- I've been thinking about reading it, and this is probably going to push me over the edge.