Out of his monadic series i always liked best the part where Philip Wadler in his ‘How to declare …’ (p. 14-) demonstrates how to erase causality from streams (of cons… famous Irishman to chime in here) and recover it by means of convergence, but showing how to have this orthogonality and glue right from the start when you keep your inner and outer worlds monadwise connected.

Since the underlying functor of the IO Monad is a stream, can’t we then have η defined by fold[(l|r)] to gain a more typeful insight?

The mixed co/data representation of your Stream (that not is of alternating least/greatest fixpoint) to me foregrounds the Altenkirch/Hutton question of when a function is a fold or an unfold.