WG211/M18Carette

It is well-known that Monoids and Lists are related: Lists are the Free Monoid on a type. One can formalize this completely: there is an adjunction between the theory of Monoids (and Monoid homomorphisms) and the theory of a single type, with the forgetful functor in one direction and the Free functor in the other.

But is this an isolated incident? Are there other data-structures, familiar from functional programming, which arise in this way? And are there simple mathematical theories that give rise to interesting data-structures? The answer to the latter two question is a resounding Yes.

Unwinding the category theory that formalizes these relations comes with an additional benefit: the usual 'kit' that comes with some natural data-structures actually falls out of the proof requirements showing that we have an actual adjunction. Furthermore, the tale has interesting twists and turns, which gives some interesting insights as to why some theoretically very natural data-structures are not pervasive in functional languages.