? ?
Notes from a Medium-Sized Island [entries|archive|friends|userinfo]

[ website | My Website ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

[Feb. 17th, 2005|11:04 pm]
[Tags|, ]

Was talking to 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.

[User Picture]From: roseandsigil
2005-02-18 04:38 am (UTC)
Yeah, William mentioned that in the ConCert meeting today. It looks really cool. I should try to understand it better ;-).
(Reply) (Thread)