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?

  • 5
    Can you spell out $\mu$? I think it's not straightforward and not going to work.. – Berci Apr 15 at 0:07
  • 3
    In more detail, concatenation is definitely wrong, since concatenating two copies of the ordered set $\mathbb{N}$ gives an ordered set that is not isomorphic to $\mathbb{N}$. – Hurkyl Apr 15 at 2:18
up vote 5 down vote accepted

$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)

  • For context, the monad you describe is called the Reader (or sometimes Environment) monad in the functional programming community. As your definition alludes to, this works for any $B$ in $A^B$, i.e. that $\mathbf N$ is the natural numbers is not used at all. One comonad on this does rely on $\mathbf N$ being a monoid and is defined as $\epsilon(f)=f(0)$ and $\delta(f)(m,n)=f(m+n)$ where $0$ and $+$ can be any monoid unit and operation. – Derek Elkins Apr 15 at 4:04
  • 'You probably want a comonad' - this was my first instinct when I read the OP's question, since streams are coinductive datatypes. – Clive Newstead Apr 15 at 4:04

Your Answer

 

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.