Documentation

Init.Data.Stream

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)) :

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'
    ...
  • toStream : collectionstream
Instances
    class Stream (stream : Type u) (value : outParam (Type v)) :
    Type (max u v)
    • next? : streamOption (value × stream)
    Instances
      def Stream.forIn {ρ : Type u_1} {α : Type u_2} {m : Type u_3 → Type u_4} {β : Type u_3} [Stream ρ α] [Monad m] (s : ρ) (b : β) (f : αβm (ForInStep β)) :
      m β
      Equations
        Instances For
          partial def Stream.forIn.visit {ρ : Type u_1} {α : Type u_2} {m : Type u_3 → Type u_4} {β : Type u_3} [Stream ρ α] [Monad m] (f : αβm (ForInStep β)) (s : ρ) (b : β) :
          m β
          @[instance 100]
          instance instForInOfStream {ρ : Type u_1} {α : Type u_2} {m : Type u_3 → Type u_4} [Stream ρ α] :
          ForIn m ρ α
          Equations
            instance instToStreamList {α : Type u_1} :
            ToStream (List α) (List α)
            Equations
              instance instToStreamArraySubarray {α : Type u_1} :
              Equations
                instance instToStreamSubarray {α : Type u_1} :
                Equations
                  instance instStreamProd {ρ : Type u_1} {α : Type u_2} {γ : Type u_3} {β : Type u_4} [Stream ρ α] [Stream γ β] :
                  Stream (ρ × γ) (α × β)
                  Equations
                    instance instStreamList {α : Type u_1} :
                    Stream (List α) α
                    Equations
                      instance instStreamSubarray {α : Type u_1} :
                      Equations