How can we define the stream monad and what is it's category of algebras?

Question

Streams are infinite lists. Lists can be modeled as monads. So can Streams. Here is a definition of the Stream monad:

$F(A) = A^{\mathbb{N}}$

All functions for $\mathbb{N}$ to A.

$\mathbb{N}$ represents the position in the list. A function from $\mathbb{N}$ to $A$ says the following:

• at the $0$th position, find $a_0$
• at the $1$st position, find $a_1$
• $\ldots$

Since $\mathbb{N}$ is infinite, we have infinite lists. The functor that defines the monad for streams is then: $$F : A \rightarrow A^N$$ $F$ works on morphisms by replacing the set elements in the list according to the function $f$, the same as the List monad. Next we need to define the natural transformations for the Stream Monad. $$\mu : F \cdot F \rightarrow F$$ This works just like the List monad, via concatenation. $$\eta : I_{Set} \rightarrow F$$ This works by injecting the set of element into the set of infinite lists such that $a$ goes into the list of $a$ repeated, so $[a,a,a, \ldots]$.

Is this correct?

Finally, what is the category of algebras for the Stream Monad? Specifically, I mean by this, given the Stream Monad $\mathcal{M}$, there are adjunctions and categories $U, C$ such that the adjunctions $U$ from $C$ to $Set$ generate monad $\mathcal{M}$. There is a category of such categories. What is this category?

Answer 1

$F$ probably doesn't model your situation

Based on what I think your target application is, this functor is unlikely to be related. For any monad $F$, the set $F(1)$ can be identified with the set of natural unary operations you can perform on $F$-algebras.

However, $F(1) = 1^\mathbf{N} \cong 1$, so there is only one natural unary operation you can perform on a stream.

What I imagine to be the target application, however, has a lot more operations that can be defined, such as "remove the first element and shift everything over one place" or "extract the 17-th element and then create the stream that repeats that element indefinitely". So $F$ is an unsuitable way to model the target application.

Your definition doesn't give a monad

I will consider the question

In what ways can the functor $F(A) = A^{\mathbf{N}}$ be made into a monad?

A key ingredient we will need is the following consequence of the Yoneda lemma

Lemma: Let $X,Y$ be sets. Every transformation $A^X \to A^Y$ natural in $A$ is of the form $A^f$ for some $f : Y \to X$.

Proof: Identifying $A^X$ with $\hom(X, A)$, the contravariant Yoneda embedding is a natural isomorphism $$ \mathrm{Nat}(\hom(X, -), \hom(Y, -)) \cong \hom(Y, X)$$ $\square$

I will now prove

Theorem: If $\eta : \mathrm{id}_{\mathrm{Set}} \to F$ and $\mu : F F \to F$ satisfy the monad identities, then

• $\eta_A : A \to A^\mathbf{N} : a \mapsto [a, a, a, \ldots] $
• $\mu_A : (A^{\mathbf{N}})^{\mathbf{N}} \to A^\mathbf{N} : s \mapsto[s_{0,0}, s_{1,1}, s_{2,2}, \ldots] $

Proof: Since there are natural isomorphisms $(A^\mathbf{N})^\mathbf{N} \cong A^{\mathbf{N} \times \mathbf{N}}$ and $A \cong A^1$, $\mu$ and $\eta$ are determined by functions $u : \mathbf{N} \to \mathbf{N} \times \mathbf{N}$ and $n : \mathbf{N} \to 1$.

Since there is a unique choice for $n$, $\eta$ is the natural transformation given above.

The identities $\mu \cdot (F \eta) = \mu \cdot (\eta F) = \mathrm{id}_F$ unfold to equations $u_0(n) = n$ and $u_1(n) = n$, and thus the only possibility for $u$ is the diagonal map $u(n) = (n,n)$. $\square$

You probably want a comonad

I've browsed the internet a bit on similar topics, and I have the impression what you really want here is a comonad, not a monad. But I've never worked it through. (and I'm not sure what underlying functor you want)