Nottingham FP Lab Blog

The origin of species

by Thorsten on November 19, 2008.
Tagged as: Lunches.

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 A : \mathbb{N} \to \mathrm{Set}, the idea is that A\,n is the set of structures which have n positions. E.g. consider the species of leaf-labelled binary trees \mathrm{BT} : \mathbb{N}\to\mathrm{Set}: BT\,3is the set of the two binary trees, which have 3 leafs (insert picture here). Given a species A we assign a functor [\![A]\!] : \mathrm{Set} \to \mathrm{Set} by [\![A]\!]\,X = \Sigma n:\mathbb{N}.A n \times X^n. 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 X^n is just n \to X 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 \mathbb{S}. Given species A,B:\mathbb{N}\to\mathrm{Set}, a morphism is given by a triple [math](f,g,h)[/math]:

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 (f,g,h) : \mathbb{S}\,A \,B we assign a natural transformation  [\![f,g,h]\!] : \Pi X:\mathrm{Set},[\![A]\!]\,X \to [\![B]\!]\,X:
 [\![f,g,h]\!]\,X\,(n,a,\mathbf{x}) = (f\,n\,a,g\,n\,a,\mathbf{x}\circ (h\,n\,a)).

Operations on species: Given species A, B : \mathbb{N}\to\mathrm{Set}:

Given a species A : \mathbb{N} \to \mathrm{Set} we can construct its initial algebra \mu A : \mathrm{Set}.

to be continued

comments powered by Disqus