Michi’s blog » [MATH 198] Lecture 4 and a question for the community

## [MATH 198] Lecture 4 and a question for the community

• October 15th, 2009
• 6:56 am

Lecture 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?

### 10 People had this to say...

• blaaargh
• October 15th, 2009
• 7:24

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?

• Michi
• October 15th, 2009
• 7:42

@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?

• ja
• October 15th, 2009
• 15:45

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).

• Craig T. Nelson
• October 15th, 2009
• 17:37

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.

• Michi
• October 15th, 2009
• 19:17

@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…

• Michi
• October 16th, 2009
• 2:42

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.