The theory of species was originally conceived by Andre Joyal and is used to analyze combinatorial structures in terms of their generating functions. In my talk on Friday I showed how the theory of species can be developed from a functional programming perspective with a view towards using them to analyze datatypes. I am diverging a bit from the classical definitions in defining a generalisation of species which matches with a specialisation of the notion of a container.
A generalized species is given by a family , the idea is that is the set of structures which have positions. E.g. consider the species of leaf-labelled binary trees : is the set of the two binary trees, which have leafs (insert picture here). Given a species we assign a functor by . The definition corresponds to the generating function, but this is a function on the reals not on sets (see my recent posting on sets and numbers). Note that is just where we identify a natural number with the set of numbers smaller than it (usually called Fin in dependently typed programming).
Category question: If species are the objects, what are the morphisms? Let’s define a category . Given species , a morphism is given by a triple [math](f,g,h)[/math]:
Calculating the numbers of positions.
Calculating the new shape.
Assigning source positions to target positions.
I leave it as an exercise to define identity and composition of those morphisms.
The definition of morphisms hopefully becomes clear when we give their interpretation as natural transformations, i.e. to every species morphism we assign a natural transformation :
Operations on species: Given species :
- Coproducts are easy:
- Products are a bit more involved:
- Composition is also interesting:
Given a species we can construct its initial algebra .
to be continued