Michi’s blog » read post

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

  • October 15th, 2009

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

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?

  • October 15th, 2009 at 7:24
Michi Said...

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

  • October 15th, 2009 at 7:42
ja Said...

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

  • October 15th, 2009 at 15:45
Craig T. Nelson Said...

ja,

I think I once saw Cale say something like “the integral of the list type is the type of directed cycles” in #haskell.

  • October 15th, 2009 at 17:37
Dan Piponi Said...

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.

  • October 15th, 2009 at 18:26
Michi Said...

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

  • October 15th, 2009 at 19:17
Dan Piponi Said...

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!

  • October 15th, 2009 at 20:06
Max Weber Said...

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…

  • October 15th, 2009 at 23:26
Michi Said...

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.

  • October 16th, 2009 at 2:42
Edward Kmet Said...

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.

  • October 16th, 2009 at 13:23

Want your say?

XHTML: You can use these tags: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>

post navigation
about
Michi is a recent PhD working in homological algebra and applied algebraic topology. This blog is his outlet for texts with some manner of thought put into them. Over at his LiveJournal intimate details and streams of consciousness might be found.
Not all here is mathematics. All here, though, are my personal thoughts and opinions. Please read the about page (linked above) for more details.
This blog uses statcounter.com for logging and traffic analysis. In order to identify return visitors, this site will issue a cookie on viewing the blog.
RSS Travel plans
Recent Comments
Tags
Categories
Blogroll
Family
Mathematician blogs
Archives
the rdc* theme