A Taylor Series for Types
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!
posted by sigfpe at Friday, June 16, 2006
3 Comments:
This is certainly something I've been kicking around for a few years, but it requires a little caution. As with Taylor series in analysis, you've got to worry about the remainder. The series summation translates to typespeak as ‘for some finite number of elements’, which means you don't get a Taylor series for Stream. If you require that each possible shape of F has finitely many positions, then you do get a Taylor series, or perhaps we should say a Taylor species.
It's also quite weird trying to figure out how to work with these jumbled up data structures. There are lots of things which intuitively should make sense, eg these bags X^n/n!, or circles X^n/n (the derivative of an (n+1)-circles is an n-tuple). Finding a notation which seduces you into writing truths is harder. Eg, X^2 is not isomorphic to 2*X^2/2. If I only give you an unordered pair and a bit, you can't recover my original ordered pair. Unless, somehow, you know that was the very bit which was used to record the order when the pair was scrambled.
So although it's a very attractive idea, it's been quite tricky getting the tools together to make it precise in the context of mucking about more generally with quotients. (By the way, Epigram 2 will support quotients: we're planning to hack up all of this stuff.)
However, the same sort of story showed up when I was trying to characterise tail-recursive iteration over trees. There, the thing that pops out is a sort of ‘Remainder Theorem’ for types, giving rise to a power series construction by repeated division. It turns out that division means (wlog) ‘finding the context of the leftmost hole’. You would expect that finding all n holes left to right, then choosing a permutation is the same as finding n holes in any order, and so it is. The beginnings of an article about this misadventure may be found here.
But yeah, this stuff is a barrel of laughs. With a hole in it.
It seems to me that X^2 is isomorphic to 2*X^2/2. The former is an ordered pair, and the latter is (depending upon which way you want to look at it) an unordered pair X^2/2 (i.e. also a bag) with a bit which then defines it to be an ordered pair.
Oh wait.
Now that I write that paragraph I see what you mean! :p Is it that you also need to know the encoding scheme used for the positioning of the two elements of the pair? ... how the bit actually tells you which way around they go?
It seems to me that if taken at "type level" then X^2 is still 'essentially' isomorphic to 2*X^2/2... if you have an unordered pair and a bit you have the information to construct an ordered pair. Granted you might not be able to recreate a particular pair, and hence my qualifier about "at type level" :)
This is probably nitpicking, but:
>> If I only give you an unordered pair and a bit, you can't recover my original ordered pair. Unless, somehow, you know that was the very bit which was used to record the order when the pair was scrambled.
I think this argument is not right (although the conclusion is still correct). Forget about unordered pairs for the moment and consider 2*2 and 2+2. If I give you Left True, you can't recover the original pair, unless you know that Left was used to encode that the left bit was true and the value true was used to encode the right bit being true. Nevertheless, these types are isomorphic, and it's easy to show an isomorphism.
Although a positive answer to the question "If I give you an element of Y, can you recover the element of X I used to make it?" is sufficient to show that there is an isomorphism, a negative answer just shows that there's no _unique_ isomorphism. If you have a total order on X, you can try making an isomorphism using the bit to record the order. However, it can't be done because 2*X^2/2 has more elements than X^2. This is because (x,x) has only one representation in X^2, but two in 2*X^2/2 (specifically (false, {x,x}) and (true, {x,x})). So it's the presence of the diagonal, not the lack of knowledge about what the bit does that prevents the isomorphism.
Post a Comment
<< Home