To focus the search input from anywhere on the page, press the 'S' key.

in-package search v0.1.0

Library

Module

Module type

Parameter

Class

Class type

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 Lazy.t`

`include MonadPlus with type 'a m := 'a m`

`include BasePlus with type 'a m := 'a m`

`include BatInterfaces.Monad with type 'a m := 'a m`

`val zero : unit -> 'a m`

`val null : 'a m -> bool`

null 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 m`

Generalises matrix transposition. This will loop infinitely if `BasePlus.null`

cannot answer `true`

for `zero`

es.

`val of_llist : 'a LazyList.t -> 'a m`

`val lsum : 'a LazyList.t m -> 'a m`

`val lmsum : 'a m LazyList.t -> 'a m`

`val ltranspose : 'a LazyList.t m -> 'a m LazyList.t`

Generalises 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!