inductive IO.AsyncList (ε : Type u) (α : Type v) : Type (max u v)

An async IO list is like a lazy list but instead of being unevaluated Thunks, delayed suffixes are Tasks being evaluated asynchronously. A delayed suffix can signal the end of computation (successful or due to a failure) with a terminating value of type ε.

• cons: {ε : Type u} → {α : Type v} → α → IO.AsyncList ε α → IO.AsyncList ε α
• delayed: {ε : Type u} → {α : Type v} → Task (Except ε (IO.AsyncList ε α)) → IO.AsyncList ε α
• nil: {ε : Type u} → {α : Type v} → IO.AsyncList ε α

instance IO.AsyncList.instInhabitedAsyncList {ε : Type u_1} {α : Type u_2} : Inhabited (IO.AsyncList ε α)

Equations

• IO.AsyncList.instInhabitedAsyncList = { default := IO.AsyncList.nil }

partial def IO.AsyncList.append {ε : Type u_1} {α : Type u_2} : IO.AsyncList ε α → IO.AsyncList ε α → IO.AsyncList ε α

instance IO.AsyncList.instAppendAsyncList {ε : Type u_1} {α : Type u_2} : Append (IO.AsyncList ε α)

Equations

• IO.AsyncList.instAppendAsyncList = { append := IO.AsyncList.append }

def IO.AsyncList.ofList {α : Type u_1} {ε : Type u_2} : List α → IO.AsyncList ε α

Equations

• IO.AsyncList.ofList = List.foldr IO.AsyncList.cons IO.AsyncList.nil

instance IO.AsyncList.instCoeListAsyncList {α : Type u_1} {ε : Type u_2} : Coe (List α) (IO.AsyncList ε α)

Equations

• IO.AsyncList.instCoeListAsyncList = { coe := IO.AsyncList.ofList }

def IO.AsyncList.unfoldAsync {σ : Type} {ε : Type} {α : Type} (f : StateT σ (EIO ε) (Option α)) (init : σ) : BaseIO (IO.AsyncList ε α)

A stateful step computation f is applied iteratively, forming an async stream. The stream ends once f returns none for the first time.

For cooperatively cancelling an ongoing computation, we recommend referencing a cancellation token in f and checking it when appropriate.

Equations

• IO.AsyncList.unfoldAsync f init = do let tInit ← EIO.asTask (IO.AsyncList.unfoldAsync.step f init) pure (IO.AsyncList.delayed tInit)

partial def IO.AsyncList.unfoldAsync.step {σ : Type} {ε : Type} {α : Type} (f : StateT σ (EIO ε) (Option α)) (s : σ) : EIO ε (IO.AsyncList ε α)

partial def IO.AsyncList.getAll {ε : Type u_1} {α : Type u_2} : IO.AsyncList ε α → List α × Option ε

The computed, synchronous list. If an async tail was present, returns also its terminating value.

partial def IO.AsyncList.waitUntil {α : Type u_1} {ε : Type u_2} (p : α → Bool) : IO.AsyncList ε α → Task (List α × Option ε)

Spawns a Task returning the prefix of elements up to (including) the first element for which p is true. When p is not true of any element, it returns the entire list.

def IO.AsyncList.waitAll {ε : Type u_1} {α : Type u_2} : IO.AsyncList ε α → Task (List α × Option ε)

Spawns a Task waiting on all elements.

Equations

• IO.AsyncList.waitAll = IO.AsyncList.waitUntil fun (x : α) => false

partial def IO.AsyncList.waitFind? {α : Type u_1} {ε : Type u_2} (p : α → Bool) : IO.AsyncList ε α → Task (Except ε (Option α))

Spawns a Task acting like List.find? but which will wait for tail evaluation when necessary to traverse the list. If the tail terminates before a matching element is found, the task throws the terminating value.

partial def IO.AsyncList.getFinishedPrefix {ε : Type} {α : Type} : IO.AsyncList ε α → BaseIO (List α × Option ε)

Retrieve the already-computed prefix of the list. If computation has finished with an error, return it as well.

def IO.AsyncList.waitHead? {ε : Type u_1} {α : Type u_2} (as : IO.AsyncList ε α) : Task (Except ε (Option α))

Equations

• IO.AsyncList.waitHead? as = IO.AsyncList.waitFind? (fun (x : α) => true) as

partial def IO.AsyncList.cancel {ε : Type u_1} {α : Type u_2} : IO.AsyncList ε α → BaseIO Unit

Cancels all tasks in the list.