Weak sequences.

While the seq structure allows for lists which may not be finite, a weak sequence also allows the computation of each element to involve an indeterminate amount of computation, including possibly an infinite loop. This is represented as a regular seq interspersed with none elements to indicate that computation is ongoing.

This model is appropriate for Haskell style lazy lists, and is closed under most interesting computation patterns on infinite lists, but conversely it is difficult to extract elements from it.

Turn a sequence into a weak sequence

Turn a list into a weak sequence

Turn a stream into a weak sequence

The empty weak sequence

Prepend an element to a weak sequence

Compute for one tick, without producing any elements

Destruct a weak sequence, to (eventually possibly) produce either none for nil or some (a, s) if an element is produced.

Get the head of a weak sequence. This involves a possibly infinite computation.

Encode a computation yielding a weak sequence into additional think constructors in a weak sequence

Get the tail of a weak sequence. This doesn't need a computation wrapper, unlike head, because flatten allows us to hide this in the construction of the weak sequence itself.

drop the first n elements from s.

Get the nth element of s.

Convert s to a list (if it is finite and completes in finite time).

Get the length of s (if it is finite and completes in finite time).

A weak sequence is finite if to_list s terminates. Equivalently, it is a finite number of think and cons applied to nil.

Get the list corresponding to a finite weak sequence.

A weak sequence is productive if it never stalls forever - there are always a finite number of thinks between cons constructors. The sequence itself is allowed to be infinite though.

Replace the nth element of s with a.

Remove the nth element of s.

Map the elements of s over f, removing any values that yield none.

Select the elements of s that satisfy p.

Get the first element of s satisfying p.

Zip a function over two weak sequences

Zip two weak sequences into a single sequence of pairs

Get the list of indexes of elements of s satisfying p

Get the index of the first element of s satisfying p

Get the index of the first occurrence of a in s

Get the indexes of occurrences of a in s

union s1 s2 is a weak sequence which interleaves s1 and s2 in some order (nondeterministically).

Returns tt if s is nil and ff if s has an element

Calculate one step of computation

Get the first n elements of a weak sequence

Split the sequence at position n into a finite initial segment and the weak sequence tail

Returns tt if any element of s satisfies p

Returns tt if every element of s satisfies p

Apply a function to the elements of the sequence to produce a sequence of partial results. (There is no scanr because this would require working from the end of the sequence, which may not exist.)

Get the weak sequence of initial segments of the input sequence

Like take, but does not wait for a result. Calculates n steps of computation and returns the sequence computed so far

Append two weak sequences. As with seq.append, this may not use the second sequence if the first one takes forever to compute

Map a function over a weak sequence

Flatten a sequence of weak sequences. (Note that this allows empty sequences, unlike seq.join.)

Monadic bind operator for weak sequences

Two weak sequences are lift_rel R related if they are either both empty, or they are both nonempty and the heads are R related and the tails are lift_rel R related. (This is a coinductive definition.)

If two sequences are equivalent, then they have the same values and the same computational behavior (i.e. if one loops forever then so does the other), although they may differ in the number of thinks needed to arrive at the answer.

Given a productive weak sequence, we can collapse all the thinks to produce a sequence.

The monadic return a is a singleton list containing a.