Jacques: Created page with "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 M..."

2018-05-15T17:13:09Z

Created page with "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 M..."

New page

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.

WG211/M18Carette - Revision history

Jacques: Created page with "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 M..."