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 positions. E.g. consider the species of leaf-labelled binary trees $\mathrm{BT} : \mathbb{N}\to\mathrm{Set}$ : $BT\,3$ is the set of the two binary trees, which have leafs (insert picture here). Given a species 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]:

$f : \Pi n:\mathbb{N}, A n \to \mathbb{N}$
Calculating the numbers of positions.
$g : \Pi n:\mathbb{N}, a: A n, B\,(f\,n)$
Calculating the new shape.
$h : \Pi n:\mathbb{N}, a: A n, (f n) \to n$
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 $(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}$ :

Coproducts are easy:
$(A + B)\,n = A\,n + B\,n$
Products are a bit more involved:
$(A \times B)\,n = \Sigma i,j:\mathrm{Nat},i+j=n \times A\,i\times B\,j$
Composition is also interesting:
$(A \circ B)\,n = \Sigma m:\mathbb{N},f:m \to \mathbb{N},(\Sigma i:m,f\,i = n),A\,m \times \Pi i:m.B\,(f\,i)$

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

to be continued