Partially defined possibly infinite lists #
This file provides a WSeq α
type representing partially defined possibly infinite lists
(referred here as weak sequences).
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.
Equations
- Stream'.WSeq α = Stream'.Seq (Option α)
Turn a sequence into a weak sequence
Equations
- Stream'.WSeq.ofSeq = (fun (x1 : α → Option α) (x2 : Stream'.Seq α) => x1 <$> x2) some
Equations
- Stream'.WSeq.coeSeq = { coe := Stream'.WSeq.ofSeq }
Equations
- Stream'.WSeq.coeList = { coe := Stream'.WSeq.ofList }
Equations
The empty weak sequence
Equations
Equations
- Stream'.WSeq.inhabited = { default := Stream'.WSeq.nil }
Prepend an element to a weak sequence
Equations
Compute for one tick, without producing any elements
Equations
Destruct a weak sequence, to (eventually possibly) produce either
none
for nil
or some (a, s)
if an element is produced.
Equations
- One or more equations did not get rendered due to their size.
Recursion principle for weak sequences, compare with List.recOn
.
Equations
- s.recOn h1 h2 h3 = Stream'.Seq.recOn s h1 fun (o : Option α) => Option.recOn (motive := fun (x : Option α) => (s : Stream'.Seq (Option α)) → C (Stream'.Seq.cons x s)) o h3 h2
membership for weak sequences
Equations
- s.Mem a = Stream'.Seq.Mem s (some a)
Equations
- Stream'.WSeq.membership = { mem := Stream'.WSeq.Mem }
Alias of Stream'.WSeq.notMem_nil
.
Get the head of a weak sequence. This involves a possibly infinite computation.
Equations
- s.head = Computation.map (fun (x : Option (α × Stream'.WSeq α)) => Prod.fst <$> x) s.destruct
Encode a computation yielding a weak sequence into additional
think
constructors in a weak sequence
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
- s.tail = Stream'.WSeq.flatten ((fun (o : Option (α × Stream'.WSeq α)) => Option.recOn o Stream'.WSeq.nil Prod.snd) <$> s.destruct)
Convert s
to a list (if it is finite and completes in finite time).
Equations
- One or more equations did not get rendered due to their size.
Append two weak sequences. As with Seq.append
, this may not use
the second sequence if the first one takes forever to compute
Equations
Map a function over a weak sequence
Equations
The monadic return a
is a singleton list containing a
.
Equations
- Stream'.WSeq.ret a = ↑[a]
Unfortunately, WSeq
is not a lawful monad, because it does not satisfy the monad laws exactly,
only up to sequence equivalence. Furthermore, even quotienting by the equivalence is not sufficient,
because the join operation involves lists of quotient elements, with a lifted equivalence relation,
and pure quotients cannot handle this type of construction.
Equations
- One or more equations did not get rendered due to their size.
auxiliary definition of tail over weak sequences
Equations
auxiliary definition of drop over weak sequences
Equations
- Stream'.WSeq.drop.aux 0 = Computation.pure
- Stream'.WSeq.drop.aux n.succ = fun (a : Option (α × Stream'.WSeq α)) => Stream'.WSeq.tail.aux a >>= Stream'.WSeq.drop.aux n
auxiliary definition of destruct_append
over weak sequences
auxiliary definition of destruct_join
over weak sequences