<p>Here's a well written piece explaining what the proper definition of a stream monad should be: <a href="http://patternsinfp.wordpress.com/2010/12/31/stream-monad/" rel="nofollow">Proper Definition of the Stream Monad</a></p>

<p>The resumption and reactive resumption monads are similar to the stream monad:<a href="https://www.google.com/url?sa=t&amp;rct=j&amp;q=&amp;esrc=s&amp;source=web&amp;cd=1&amp;cad=rja&amp;uact=8&amp;ved=0ahUKEwjqzejI-ezLAhXBJR4KHV-oDCcQFggcMAA&amp;url=http%3A%2F%2Fwww.softlab.ntua.gr%2Fresearch%2Ftechrep%2FCSD-SW-TR-2-01.pdf&amp;usg=AFQjCNE5GXnUYg8tYNRNsz4-hRGL6FXmbg&amp;sig2=HpsCmHLRfebxEk06BqysNg&amp;bvm=bv.118443451,d.dmo" rel="nofollow" title="Resumption Monad Transformers">Resumption Monad Transformers</a> </p>

CC BY-SA 3.0
2016-04-01T08:32:33.080Z
I know that `S` in my example is a monad. But that's not the question. I'm asking about monadic streams, which are a generalisation of streams.
Turion
CC BY-SA 3.0
2016-04-01T20:23:43.313Z
As it stands, absent any verification that S is in fact a monad (given the information you provided). Head and tail aren't sufficient (by themselves) for defining a stream monad. Perhaps, we're just talking past one another. At any rate, to point you in the right direction, you'll want to convince yourself that unit and join for a *stream monad*  aren't defined simply in terms of head and tail operations. For example, unit = repeat and join = unfold fork(head.head,tail . map tail).
Khaos
CC BY-SA 3.0
2016-04-01T20:53:17.560Z
(Friendlier version of my original comment.) Thanks, I agree that we're talking past one another. For the purposes of the question, it's irrelevant whether `S` is a monad or not. Do resumption monad transformers give you any tools for proving equality of two monadic streams?
Turion
CC BY-SA 3.0
2016-04-01T07:51:26.140Z
2016-04-01T07:51:26.140Z
Khaos
<p>For ordinary streams $S_A := \nu X. A \times X$, there is a bisimulation lemma. It says that two streams are equal if there exists a bisimulation between them. A bisimulation is a relation $\sim$ on streams defined like this:
$s_1 \sim s_2 \iff \operatorname{head} s_1 = \operatorname{head} s_2 \wedge \operatorname{tail} s_1 \sim \operatorname{tail} s_2$.</p>

<p>Now, let $M$ be a monad. We'll define the type of <strong>"monadic streams"</strong> $S^M_A := \nu X. M (A \times X)$. Intuitively, if $M$ corresponds to a side effect, every time I retrieve the head from the stream I have to perform the side effect. I can define $\operatorname{head}^M: S^M_A \to M A$ and $\operatorname{tail}^M: S^M_A \to M S^M_A$ (using functoriality of $M$).</p>

<p>My question is now: Is there anything similar to bisimulation for monadic streams? Can I prove equality of monadic streams in the same way, using $\operatorname{head}^M$ and $\operatorname{tail}^M$? If not, what are proof methods that work on this coinductive type? Maybe the approximation lemma?</p>

<p>Edit: Maybe there has to be a restriction on the monad, like being completely positive?</p>

CC BY-SA 3.0
2016-03-31T09:13:39.497Z
I believe this would benefit from a `bisimulation` and a `coinduction` tag, but these don't exist.
Turion
CC BY-SA 3.0
2016-04-02T13:42:35.403Z
I think Monads in general are Trees not just Lists. Could you modify Reed's recursion for tree canonization?  Read, Ronald C. (1972), "The coding of various kinds of unlabeled trees", Graph Theory and Computing, Academic Press, New York, pp. 153–182
Chad Brewbaker
<data-streams><monad><streaming>
Does bisimulation or the approximation lemma work for monadic streams?
Turion
# Does bisimulation or the approximation lemma work for monadic streams?

(Asked by: username_0 on 2016-03-31)

For ordinary streams $S\_A := \nu X. A \times X$, there is a bisimulation lemma. It says that two streams are equal if there exists a bisimulation between them. A bisimulation is a relation $\sim$ on streams defined like this:
$s\_1 \sim s\_2 \iff \operatorname{head} s\_1 = \operatorname{head} s\_2 \wedge \operatorname{tail} s\_1 \sim \operatorname{tail} s\_2$.

Now, let $M$ be a monad. We'll define the type of **"monadic streams"** $S^M\_A := \nu X. M (A \times X)$. Intuitively, if $M$ corresponds to a side effect, every time I retrieve the head from the stream I have to perform the side effect. I can define $\operatorname{head}^M: S^M\_A \to M A$ and $\operatorname{tail}^M: S^M\_A \to M S^M\_A$ (using functoriality of $M$).

My question is now: Is there anything similar to bisimulation for monadic streams? Can I prove equality of monadic streams in the same way, using $\operatorname{head}^M$ and $\operatorname{tail}^M$? If not, what are proof methods that work on this coinductive type? Maybe the approximation lemma?

Edit: Maybe there has to be a restriction on the monad, like being completely positive?

**Tags:** data-streams, monad, streaming

> **Comments:**
> **username_0**: I believe this would benefit from a `bisimulation` and a `coinduction` tag, but these don't exist.  
> **username_1**: I think Monads in general are Trees not just Lists. Could you modify Reed's recursion for tree canonization?  Read, Ronald C. (1972), "The coding of various kinds of unlabeled trees", Graph Theory and Computing, Academic Press, New York, pp. 153–182  

---

## 1 answers

### Answer by username_2 on 2016-04-01. Score: -1

Here's a well written piece explaining what the proper definition of a stream monad should be: [Proper Definition of the Stream Monad](http://patternsinfp.wordpress.com/2010/12/31/stream-monad/)

The resumption and reactive resumption monads are similar to the stream monad:[Resumption Monad Transformers](https://www.google.com/url?sa=t&rct=j&q=&esrc=s&source=web&cd=1&cad=rja&uact=8&ved=0ahUKEwjqzejI-ezLAhXBJR4KHV-oDCcQFggcMAA&url=http%3A%2F%2Fwww.softlab.ntua.gr%2Fresearch%2Ftechrep%2FCSD-SW-TR-2-01.pdf&usg=AFQjCNE5GXnUYg8tYNRNsz4-hRGL6FXmbg&sig2=HpsCmHLRfebxEk06BqysNg&bvm=bv.118443451,d.dmo "Resumption Monad Transformers")

> **Comments:**
> **username_0**: I know that `S` in my example is a monad. But that's not the question. I'm asking about monadic streams, which are a generalisation of streams.  
> **username_2**: As it stands, absent any verification that S is in fact a monad (given the information you provided). Head and tail aren't sufficient (by themselves) for defining a stream monad. Perhaps, we're just talking past one another. At any rate, to point you in the right direction, you'll want to convince yourself that unit and join for a *stream monad*  aren't defined simply in terms of head and tail operations. For example, unit = repeat and join = unfold fork(head.head,tail . map tail).  
> **username_0**: (Friendlier version of my original comment.) Thanks, I agree that we're talking past one another. For the purposes of the question, it's irrelevant whether `S` is a monad or not. Do resumption monad transformers give you any tools for proving equality of two monadic streams?  

---

