lists as function monoids

Question

I was shown that lists in programming are an example of a free monoid. I was thinking about their structure and noticed lists can be represented as functions from finite lists, and want to know more about what this implies about lists. Is there a name communicating that free monoids can have an index?

Let $J_n = \{0, ..., n - 1\}$ and let $f : J_n \rightarrow A$ and $g : J_m \rightarrow A$.

Define $\langle f, g\rangle: J_{n+m} \rightarrow A$ by

$$\langle f, g\rangle(x) = \begin{cases} f(x) &\text{if $x < n$ and}\\ g(x - n) &\text{otherwise}. \end{cases} $$ I want to call this the concatenation of $f$ and $g$.

There is a unique function $I : J_0 \rightarrow A$ which satisfies $\langle f, I\rangle = \langle I, f\rangle = f$.

It seems clear to me the above operator is associative, which means these functions form a monoid.

Now, I like this, because it shows that lists having indexes is natural. Is there a name for this property, or these sets? I would like to learn a little bit more about them.

Answer 1

A list, i.e. element of the free monoid, can be thought of as an $n$-tuple for some $n$. You've just noted that $n$-tuples can also be represented as functions from an $n$ element set. This is even suggested by notation: we write the set of $n$-tuples of elements of $A$ as $A^n$ and your representation would be notated as $A^{J_n}$, the set of functions from $J_n$ to $A$.

If you are familiar with Agda or a similar dependently typed language, what you call $J_n$ is usually the type Fin n. The type of tuples indexed by a natural number is usually called Vec. You could then fairly easily write out an explicit isomorphism between Vec n A and Fin n -> A. You can also show that List A is isomorphic to the dependent sum Σ Nat (\n -> Vec n A) and thus also to Σ Nat (\n -> Fin n -> A). These latter two types can be thought of as saying that a list is a pair of a natural number, $n$, and an $n$-tuple in either of the two aforementioned representations. With these explicit isomorphisms you could then define your concatenate function by converting to the "usual" representations of lists, concatenating, and then converting back if you wanted (and similarly for other operations).

Answer 2

Well, as you mention in your introduction, this is an example of a free monoid, namely the free monoid $A^*$ on the alphabet $A$. To see this, you just have to identify a word $f = a_0 a_1 \cdots a_{n-1}$ to the map $f: J_n \to A$ defined by $f(i) = a_i$. If you do this, you will see that the product $\langle u, v\rangle$ is precisely the concatenation $uv$ of $u$ and $v$ (so your intuition is correct). And your function $I$ corresponds to the empty word.