Michi’s blog » [MATH 198] Lecture 4 and a question for the community
[MATH 198] Lecture 4 and a question for the communityLecture 4 was held, and the notes are up on the wiki: Lecture 4 notes
During class, and in unrelated conversations afterwards, though, the question emerged:
If Formally differentiating datatypes gives us zippers? What happens if we formally integrate datatypes?
@blaaargh
Well, I guess, part of the question is verifying that integrating over an actual zipper gives me back whatever I started with.
The other part is – what happens if we integrate a non-zipper?
If you integrate the list type, you get a non-empty cyclic list. I can’t remember where I read that, but if you do the math, it’s not to hard to see. Using the series representation, integrating t^n gives (t^(n+1))/(n+1).
ja,
I think I once saw Cale say something like “the integral of the list type is the type of directed cycles” in #haskell.
A regular type is one that can be formed from polynomial functors and fixed points. Sadly there is no guarantee that a regular type has an integral that’s a regular type. Even a simple container type like the identity, which you could write as the functor F(X)=X, would have an integral like X^2/2, and division makes no sense here.
Nonetheless, some integrals and some differential equations do make sense and you’re just solving to find which types have holes given by some other type.
BTW If you look at differential equations in types, like F’(X) = G(F(X)) for some functor G, you’re led towards Hopf Algebras of trees. Don’t know if that’s significant.
@Dan
But is it really completely hopeless to interpret divisions? It seems that what Ed Kmett does in his Generatingfunctorology entry, and what the directed cycles comment above does, is to view divisions by integers, at least, as a sort of symmetrization operation – which would tie in with the decategorification ideas: the number of multisets on k elements will correspond to the number of lists on those k elements, divided by some constant for the symmetrization of the order of the elements.
Hence, X^2/2 could, potentially, be interpreted as being, really, (sort X^2); since two cases of these will get us the unsorted list: namely the cases (sort X^2) and (reverse . sort X^2)…
One of Conor McBride’s papers considers types with symmetries acting on them. If you do that then you can consider exp(X), say, to be the multiset (ie. lists without order) type. In order to do that we need to have a way to compute equality of elements (and order them if we want something implementable efficiently).
My antidiagonal types could be viewed as ways to evaluate X(X-1)(X-2)…(X-n+1)/n!
4th lecture notes are better than 3rd one , much more detailed, it will be be good if you use some videos or flash for the notes.
Good work…
Using flash or video brings in the question of PRODUCING the video or flash. Which, given that even TeXed diagrams is a bit of a bother doing well here, is a whole new game that I’m reluctant to go into.
You might want to look at the Joyal’s Theory of Combinatorial Species, or Brent Yorgey’s species library to get a feel for general species rather than polynomial functors that formalizes the notion of division I used in my generatingfunctorology post. Note that I only divided the nth coefficient by up to n! so everything remained an exponential generating function, but if you allow virtual species you can derive proper division and subtraction on data structures.
As Dan pointed out your integrals may go places that can’t be expressed with polynomial functors. That said, I’m not sure they will remain closed under combinatorial species off the top of my head either.
You could formally integrate the power series, but alas two species that have the same power series are not necessarily isomorphic, although two isomorphic species will have the same power series.
http://en.wikipedia.org/wiki/Combinatorial_species#Calculus_of_species
In general obtaining the power series doesn’t necessarily give you a nice recurrence that generates that power series.
RSS feeds available for 
Velcro(tm)?
Just guessing, but since “integrating” a zipper gives back the original datatype, the question should be what type the datatype in question is a zipper for?