A Taylor Series for Types (original) (raw)

There's a result that I'm surprised isn't mentioned in Derivatives of Containers. It's pretty obvious considering what's in that paper but it's still interesting to mention, so maybe it's well known and too obvious for anyone else to state explicitly. Basically this

F[X+Y]=F[X]+Y F'[X]+Y²/2! F''[X]+Y³/3! F'''[X]+...

is true when interpreted as a statement about types.

But first I have to say what I mean by dividing a type by n!. That's explained at the end of the above paper, but first some notation: Let n be the set {0,...,n-1}. Then use the suggestive notation X! to mean the group of permutations of X. Clearly #(n!)=n!, where the on the right hand side I'm using ! to mean factorial. We now allow groups to act on containers by permuting the elements within them. For example a triple of X's is written X³. This datatype has a notion of an ordering of the elements ie. (1,2,3) is not the same as (3,2,1). The group 3! acts in a natural way on triples by permuting the three elements. If we take the quotient by this group then we get the 3-element bag where order doesn't matter. So Xn/n! is the n-element bag. (As pointed out in the paper, we can't define sets in this way because sets require a notion of equality.)

The paper also shows that F'[X] is the type of F-containers with one of the X's punched out to leave a hole. So F(n)[X] is an F-container with n holes punched out. But note that it still retains information about the order in which the holes were punched out. For example, consider pairs with F[X]=X². F''[X]=2. This corresponds to the fact that there are two orders in which you can punch out the two elements of a pair.

Now consider a Yn/n! F(n)[X]. This is an F-container of X's where n of the X's have been punched out, combined with n Y's. We can insert the n Y's into the holes in the order specified by the F(n)[X]. So Yn/n! F(n)[X] is an F-container of X's with n of the X's replaced by Y's.

Now look at the right hand side of the Taylor series. This is basically an F-container of X's where some (or zero) of the X's have been replaced by Y's.

And finally note what the left hand side is: it's an F-container of X+Y's. Ie. each object in the F-container is either an X or a Y. And it's pretty obvious that's the same thing as a container of X's where some of the X's are replaced by Y's.

I like to write it as F[X+Y]=exp(Y d/dX)F[X].

Hey! I just discovered there's a Container Type blog!