**neelk**and William Lovas about the tantalizingly cute paper at the bottom of Conor McBride's publication list. It talks about "taking the derivative" of type operators or something. I haven't actually read the paper, (though I should soon) but I've absorbed a bit of its contents through folklore over the last few years.

I was thinking about what is going on when you take the derivative of the type operator underneath the μ in a recursive type, and why you need to slap the

`list`type operator onto the end when you're done. On the bus to D's I think I figured out why.

So if I start with a type T defined in terms of a type operator F as μα.F(α), then let us say that TH(X) = μβ.X + F(β). This type operator TH once applied to X gives us a type that looks much like T, except that there is, at every level of the recursion, the possibility of wedging in a piece of data of type X, instead of providing something of type T, as we would normally. So now we have a variable to "differentiate" with respect to. I have intentionally positioned this variable in every place that a "hole" might go when one invokes the slogan that the "derivative" of a regular type of things is the "type of one-holed things" of that (recursive) regular type. Except

*actually*you need to plug the original type back into the argument of the derivative, and plug that whole mess into the type operator

`list`. Which is exactly the thing I'm trying to explain away.

So what I claim is that what TH(X) is, is an explanation of what "hole" means (or rather, what it

*might*be said to mean - I think one might alternatively think, for example, of TH(X) = μβ.X * F(β) for a different notion of hole) for recursive types. If you now differentiate with respect to X, you indeed get a type which is just like TH(X), except whose inhabitants have exactly one placeholder for one of the Xs. Just watch:

TH'(X) = (μβ.X + F(β))'

= (X + F(μβ.X + F(β)))'

= X' + (F(μβ.X + F(β)))'

= 1 + (F(TH(X))' (by X' = 1, and by definition of TH)

= 1 + F'(TH(X)) * TH'(X) (by

*[muffled laughter]*the chain rule)

But actually we don't want to admit this extra X-junk into our types. If we set X = 0, i.e., the void type, then TH(0) in fact is isomorphic to T. Thus

TH'(0) = 1 + F'(TH(X)) * TH'(0) = 1 + F'(T) * TH'(0)

and this means the type we're seeking, really, is the solution of a type fixpoint, and can be written as

μα 1 + F'(T) * α

which is immediately familiar as F'(T)

`list`, identical with the original method, qed.

Speaking of which, I should read some of McBride's other stuff. His writing style is hilarious.