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
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
Streams in monadic code.
- toStream : collection → stream
Streams are used to implement parallel
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' ...