A new species

I spent some time last night looking more closely at Carette and Uszkey's new paper on species, as mentioned recently on Lambda the Ultimate. I mostly concentrated on the first few sections and the Haskell bit at the end. They say many tantalizing things, and I had kind of hoped the punchline would be something like "here is how you can write code in a beautifully functional style over graphs and cyclic structures" (assuming I understood the potential of species correctly).  Perhaps in a follow up paper.

I also found it interesting that their dot product operator sounds more like the traditional Cartesian product type (one of each type), and their Cartesian product type sounds much more like an intersection type (the value is a structure having both types). Perhaps it is a notational holdover from previous work on species. It also seem to make for some nice concrete examples of the "locative" aspects of Girard's Ludics.

Now back to reviewing journal and ICFP papers...

2 Comments »

  1. Jacques Carette said,

    May 2, 2008 @ 5:16 pm

    We wanted to get to that punchline, but couldn’t quite yet. We know that the underlying tools are there in the semantics (folds, etc). But an actual implementation is altogether different.

    In Haskell, there is foldl, foldl1, foldr and foldr1, right? There are “only” 4 because there is an obvious interpretation of regular functors as L-species that give you 2 canonical choices of ordering (but 2 more choices from laziness). The problem with other structures is that you don’t have such canonical choices, so you get a whole tree of potential folds. Of course if what you are using in your fold is a commutative-associative binary function, then the whole tree collapses as all choices are isomorphic [but not identical]. There just was not time for us to explain this properly in this paper.

    Another obvious route to take is to look at build-fold fusion rules. If we stay ‘categorical’, then the fold is ok (as just a map from one F-algebra to another). But we have yet to get a good picture of the underlying ‘build’ for species. And we are pretty sure that some of neatest computations will come from just that. Well, that and from fusing away Virtual Species, although that’s another thread altogether.

    You are quite right that our notation for products comes from previous work on species, and that work itself is greatly influenced by analysis. In other words, the notation for the species operations is a lift of the notation for the corresponding operation on generating functions!

    As to the link with Ludics, I don’t know. I have tried to read Girard’s Ludics paper, but gave up. I will file that idea away for further study though.

  2. washburn said,

    May 13, 2008 @ 12:22 pm

    @Jacques: Thanks for the additional details, I look forward to seeing what you come up with in your future research. If nothing, else I really like the idea of having differentiation or pointing available as first class type operators.

    Girard’s writing on Ludics are indeed quite impenetrable. I’ve managed to understand some of the pieces. Part of Ludics is based upon the ideas surrounding focusing, that the folks at CMU are now explaining in a much more approachable fashion. Another part seems to be based upon location, which is why fairly early on in Locus Solum he starts describing derivations entirely in terms of indices. Somewhere along the lines he starts defining “locative” variants of the usual logical operators, and there is some comments about how locative and delocalized products related to standard Cartesian products and intersection types, but it is all very difficult to follow. I guess what is particularly interesting is there also seems to be a “delocation” connective/modality to convert from intermediate between the locative to delocalized forms.

RSS feed for comments on this post · TrackBack URI

Leave a Comment