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 Streams in monadic code.

class ToStream (collection : Type u) (stream : outParam (Type u)) : Type u

• 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'
    ...

class Stream (stream : Type u) (value : outParam (Type v)) : Type (maxuv)

• next? : stream → Option (value × stream)

def Stream.forIn {ρ : Type u_1} {α : Type u_2} {m : Type u_3 → Type u_4} {β : Type u_3} [inst : Stream ρ α] [inst : Monad m] (s : ρ) (b : β) (f : α → β → m (ForInStep β)) : m β

Equations

• Stream.forIn s b f = let x := { default := pure b }; Stream.forIn.visit f s b

partial def Stream.forIn.visit {ρ : Type u_1} {α : Type u_2} {m : Type u_3 → Type u_4} {β : Type u_3} [inst : Stream ρ α] [inst : Monad m] (f : α → β → m (ForInStep β)) (s : ρ) (b : β) : m β

instance instForIn {ρ : Type u_1} {α : Type u_2} {m : Type u_3 → Type u_4} [inst : Stream ρ α] : ForIn m ρ α

Equations

• instForIn = { forIn := fun {β} [Monad m] => Stream.forIn }

instance instToStreamList {α : Type u_1} : ToStream (List α) (List α)

Equations

• instToStreamList = { toStream := fun c => c }

instance instToStreamArraySubarray {α : Type u_1} : ToStream (Array α) (Subarray α)

Equations

• instToStreamArraySubarray = { toStream := fun a => Array.toSubarray a 0 (Array.size a) }

instance instToStreamSubarray {α : Type u_1} : ToStream (Subarray α) (Subarray α)

Equations

• instToStreamSubarray = { toStream := fun a => a }

instance instToStreamStringSubstring : ToStream String Substring

Equations

• instToStreamStringSubstring = { toStream := fun s => String.toSubstring s }

instance instToStreamRange : ToStream Std.Range Std.Range

Equations

• instToStreamRange = { toStream := fun r => r }

instance instStreamProdProd {ρ : Type u_1} {α : Type u_2} {γ : Type u_3} {β : Type u_4} [inst : Stream ρ α] [inst : Stream γ β] : Stream (ρ × γ) (α × β)

Equations

• One or more equations did not get rendered due to their size.

instance instStreamList {α : Type u_1} : Stream (List α) α

Equations

• instStreamList = { next? := fun x => match x with | [] => none | a :: as => some (a, as) }

instance instStreamSubarray {α : Type u_1} : Stream (Subarray α) α

Equations

• One or more equations did not get rendered due to their size.

instance instStreamRangeNat : Stream Std.Range Nat

Equations

• instStreamRangeNat = { next? := fun r => if r.start < r.stop then some (r.start, { start := r.start + r.step, stop := r.stop, step := r.step }) else none }

instance instStreamSubstringChar : Stream Substring Char

Equations

• One or more equations did not get rendered due to their size.