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 '16 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$ – Chad Brewbaker Apr 2 '16 at 13:42

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

| cite | improve this answer | |
  • $\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 '16 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 '16 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 '16 at 20:53

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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