Remark: we considered using the following alternative design
structure Stream (α : Type u) where
stream : Type u
next? : stream → Option (α × stream)
class ToStream (collection : Type u) (value : outParam (Type v)) where
toStream : collection → Stream value
where Stream
is not a class, and its state is encapsulated.
The key problem is that the type Stream α
"lives" in a universe higher than α
.
This is a problem because we want to use Stream
s in monadic code.
- toStream : collection → stream
Streams are used to implement parallel for
statements.
Example:
for x in xs, y in ys do
...
is expanded into
let mut s := toStream ys
for x in xs do
match Stream.next? s with
| none => break
| some (y, s') =>
s := s'
...