- 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?
- 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.
- Recent Comments
- Tags
- Categories
-
- 10th grade topology
- 9th grade topology
- A-infinity
- Administrative
- Algebra
- Algebraic geometry
- Blogs
- Calligraphy
- Carnival of Mathematics
- Category theory
- Combinatorics
- Communicating science
- Computer
- Conferencing
- Cookies
- Cooking
- Differential geometry
- English
- Geometry
- Haskell
- Homology and Homotopy
- Improbable research
- Intellectual property
- J
- Jahr der Mathematik
- JMM2008
- Knot theory
- LaTeX
- Liveblogging
- Mathematics
- Meme
- Metablogging
- Modular Representation Theory
- Operads and PROPs
- Parallel
- PhD
- Politics
- Postdoc Carnival
- Privacy
- Programming
- Python
- R
- Recipe
- Religion
- Research
- Ruby
- Ruby on Rails
- Security
- Sillyness
- Svenska
- Teaching
- Topology
- Travel
- Travelogue
- Web 2.0 for Mathematics
- Weekly report
- Blogroll
- Family
- Mathematician blogs
- Archives
-
- February 2010
- December 2009
- November 2009
- October 2009
- September 2009
- August 2009
- July 2009
- June 2009
- May 2009
- March 2009
- February 2009
- January 2009
- December 2008
- November 2008
- October 2008
- September 2008
- August 2008
- July 2008
- June 2008
- May 2008
- March 2008
- February 2008
- January 2008
- December 2007
- November 2007
- October 2007
- September 2007
- August 2007
- July 2007
- June 2007
- May 2007
- April 2007
- March 2007
- February 2007
- January 2007
- December 2006
- November 2006
- October 2006
- September 2006
- July 2006
- June 2006
- May 2006
- April 2006
- March 2006
- February 2006
- January 2006
- December 2005
- May 2005
10 People had this to say...
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?
@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.
Want your say?