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?

  • $\begingroup$ I believe this would benefit from a bisimulation and a coinduction tag, but these don't exist. $\endgroup$
    – Turion
    Mar 31, 2016 at 9:13
  • $\begingroup$ 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 $\endgroup$ Apr 2, 2016 at 13:42

1 Answer 1


Here's a well written piece explaining what the proper definition of a stream monad should be: Proper Definition of the Stream Monad

The resumption and reactive resumption monads are similar to the stream monad:Resumption Monad Transformers

  • $\begingroup$ 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. $\endgroup$
    – Turion
    Apr 1, 2016 at 8:32
  • $\begingroup$ 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). $\endgroup$
    – Khaos
    Apr 1, 2016 at 20:23
  • $\begingroup$ (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? $\endgroup$
    – Turion
    Apr 1, 2016 at 20:53

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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