2
$\begingroup$

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?

$\endgroup$
2
  • 5
    $\begingroup$ Can you spell out $\mu$? I think it's not straightforward and not going to work.. $\endgroup$
    – Berci
    Commented Apr 15, 2018 at 0:07
  • 3
    $\begingroup$ 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}$. $\endgroup$
    – user14972
    Commented Apr 15, 2018 at 2:18

1 Answer 1

5
$\begingroup$

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

$\endgroup$
2
  • $\begingroup$ 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. $\endgroup$ Commented Apr 15, 2018 at 4:04
  • $\begingroup$ 'You probably want a comonad' - this was my first instinct when I read the OP's question, since streams are coinductive datatypes. $\endgroup$ Commented Apr 15, 2018 at 4:04

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .