Streams supporting fair and unbounded search.
Spivey has a nice and authoratitive paper on this, understanding streams as a breadth-first search. If that description appeals to you, I recommend his paper. Personally, I found it helpful to understand streams a bit differently, as concurrent processes that go off and discover data.
First, we have generations, which are collections of zero or more data. The data in each generation is discovered simultaneously, and therefore, it doesn't make much sense to have any ordering imposed on the generations. In fact, the lack of an ordering is essential for getting the associativity laws of the monad, and is why Spivey's paper works with bags.
Now a stream is just a lazy list of generations. We want to think of the indices into these streams as temporal indices. So the first generation in the lazy list was discovered at time 0. The second was discovered at time 1. The third was discovered at time 2. And so on.
Thinking this way helped me figure out return and join. Here, return x gives you the process which immediately discovers x and then terminates.
With join xss, we should interpret the xss as a process which discovers other processes. When we join them, we ask the outer process to fork each inner process as soon as it is discovered, and then merge in all the values found by the forked processes. For instance, if xs discovers a process p at time 5, and in turn, p discovers the string "hello world!" at time 13, then join xs discovers "hello world!" at time 5 + 13 = 18.
Now we can understand bind, realising that it is just the result of doing a map and then a join. The expression bind xs f forks processes f which depend on a discovered value x, and then merges back all their values.
Technically, all our streams should be infinite, and the processes should run forever, but this gave me sad performance in my theorem proving code. So for efficiency, our streams can be truncated, which represents a process that terminates.
Note that it is impossible to define a general BaseLazyPlus.null predicate for streams, because we would have to be able to decide whether an infinite stream of values consists entirely of the empty generation. Turing says that's impossible, and I believe him. As a crude approximation, then, we have it that
BaseLazyPlus.null returns true just for the special case that its input is an empty lazy list.
include LazyPlus with type 'a m = 'a t Stdlib.Lazy.tinclude BaseLazyPlus with type 'a m = 'a t Stdlib.Lazy.tinclude BatInterfaces.Monad with type 'a m = 'a t Stdlib.Lazy.ttype 'a m = 'a t Stdlib.Lazy.tThe type of a monad producing values of type 'a.
include MonadPlus with type 'a m := 'a minclude BasePlus with type 'a m := 'a minclude BatInterfaces.Monad with type 'a m := 'a mval zero : unit -> 'a mval null : 'a m -> boolnull x implies that x is zero. If you do not want to or cannot answer whether a given x is zero, then null x should be false. I have provided this so that streams can be implemented more efficiently.
val of_list : 'a list -> 'a mGeneralises matrix transposition. This will loop infinitely if BasePlus.null cannot answer true for zeroes.
val of_llist : 'a LazyList.t -> 'a mval lsum : 'a LazyList.t m -> 'a mval lmsum : 'a m LazyList.t -> 'a mval ltranspose : 'a LazyList.t m -> 'a m LazyList.tGeneralises matrix transposition. You don't necessarily have to worry about correctly implementing BaseLazyPlus.null for this function, since the return value can happily be infinite.
Delay a stream by one time step. This is needed when you write recursive streams and you have to avoid deadlock. The nice thing about Ocaml here is that it will generally detect deadlock for you, announcing to you that you're writing viciously circular lists!