This module Defines the asynchronous monadic interface for Lake. The interface is composed of three major abstract monadic types:
m
: The monad of the synchronous action (e.g.,IO
).n
: The monad of the (a)synchronous task manager (e.g.,BaseIO
).k
: The monad of the (a)synchronous task (e.g.,IOTask
).
The definitions within this module provide the basic utilities for converting between these monads and combining them in different ways.
Async / Await Abstraction #
Standard Instances #
Equations
- Lake.instSyncIdTask = { sync := fun {α : Type u_1} => Task.pure }
Equations
- Lake.instSyncBaseIOBaseIOTask = { sync := fun {α : Type} => Functor.map Task.pure }
Equations
- Lake.instSyncEIOBaseIOEIOTask = { sync := fun {α : Type} (x : EIO ε α) => Lake.sync (ExceptT.mk (EIO.toBaseIO x)) }
Equations
- Lake.instSyncOptionIOBaseIOOptionIOTask = { sync := fun {α : Type} (x : Lake.OptionIO α) => Lake.sync (OptionT.mk (Lake.OptionIO.toBaseIO x)) }
Equations
- Lake.instAsyncIdTask = { async := fun {α : Type u_1} => Task.pure }
Equations
- Lake.instAsyncBaseIOBaseIOTask = { async := fun {α : Type} (act : BaseIO α) => BaseIO.asTask act }
Equations
- Lake.instAsyncReaderTReaderT = { async := fun {α : Type u_1} (x : ReaderT ρ m α) (r : ρ) => Lake.async (x r) }
Equations
- Lake.instAsyncExceptTExceptT = { async := fun {α : Type u_1} (x : ExceptT ε m α) => cast ⋯ (Lake.async (ExceptT.run x)) }
Equations
- Lake.instAsyncOptionTOptionT = { async := fun {α : Type u_1} (x : OptionT m α) => cast ⋯ (Lake.async (OptionT.run x)) }
Equations
- Lake.instAsyncEIOBaseIOEIOTask = { async := fun {α : Type} (x : EIO ε α) => Lake.async (ExceptT.mk (EIO.toBaseIO x)) }
Equations
- Lake.instAsyncOptionIOBaseIOOptionIOTask = { async := fun {α : Type} (x : Lake.OptionIO α) => Lake.async (OptionT.mk (Lake.OptionIO.toBaseIO x)) }
Equations
- Lake.instAwaitTaskId = { await := fun {α : Type u_1} => Task.get }
Equations
- Lake.instAwaitOptionIOTaskOptionIO = { await := fun {α : Type} (x : Lake.OptionIOTask α) => liftM (IO.wait x) >>= liftM }
Equations
- Lake.instAwaitExceptTExceptT = { await := fun {α : Type u_1} (x : ExceptT ε k α) => ExceptT.mk (Lake.await (ExceptT.run x)) }
Equations
- Lake.instAwaitOptionTOptionT = { await := fun {α : Type u_1} (x : OptionT k α) => OptionT.mk (Lake.await (OptionT.run x)) }
Combinators #
- bindSync : {α β : Type u} → Task.Priority → k α → (α → m β) → n (k β)
Perform a synchronous action after another (a)synchronous task completes successfully.
Instances
Instances
Standard Instances #
Equations
- Lake.instBindSyncIdTask = { bindSync := fun {α β : Type u_1} (x : Task.Priority) => flip fun (f : α → Id β) (x : Task α) => Task.map f x Task.Priority.default }
Equations
- Lake.instBindSyncBaseIOBaseIOTask = { bindSync := fun {α β : Type} (x : Task.Priority) => flip fun (f : α → BaseIO β) (t : Task α) => BaseIO.mapTask f t Task.Priority.default }
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lake.instBindAsyncIdTask = { bindAsync := fun {α β : Type u_1} (x : Task α) (f : α → Task β) => Task.bind x f Task.Priority.default }
Equations
- Lake.instBindAsyncBaseIOBaseIOTask = { bindAsync := fun {α β : Type} (t : Task α) (f : α → BaseIO (Task β)) => BaseIO.bindTask t f Task.Priority.default }
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lake.instBindAsyncReaderT = { bindAsync := fun {α β : Type u_1} (ka : k α) (f : α → ReaderT ρ n (k β)) (r : ρ) => Lake.bindAsync ka fun (a : α) => f a r }
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lake.instApplicativeAsyncIdTask = Lake.ApplicativeAsync.mk
Equations
- Lake.instApplicativeAsyncBaseIOBaseIOTask = Lake.ApplicativeAsync.mk
Equations
- Lake.instApplicativeAsyncExceptT = Lake.ApplicativeAsync.mk
Equations
- Lake.instApplicativeAsyncOptionT = Lake.ApplicativeAsync.mk
List/Array Utilities #
Sequencing (A)synchronous Tasks #
Combine all (a)synchronous tasks in a List
from right to left into a single task ending last
.
Equations
- Lake.seqLeftList1Async last [] = pure last
- Lake.seqLeftList1Async last (t :: ts) = do let x ← Lake.seqLeftList1Async t ts Lake.seqLeftAsync last x
Instances For
Combine all (a)synchronous tasks in a List
from right to left into a single task.
Equations
- Lake.seqLeftListAsync x = match x with | [] => pure (pure ()) | t :: ts => Lake.seqLeftList1Async t ts
Instances For
Combine all (a)synchronous tasks in a List
from left to right into a single task.
Equations
- Lake.seqRightListAsync x = match x with | [] => pure (pure ()) | t :: ts => List.foldlM Lake.seqRightAsync t ts
Instances For
Combine all (a)synchronous tasks in a Array
from right to left into a single task.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Combine all (a)synchronous tasks in a Array
from left to right into a single task.
Equations
- Lake.seqRightArrayAsync tasks = if h : 0 < Array.size tasks then Array.foldlM Lake.seqRightAsync (Array.get tasks { val := 0, isLt := h }) tasks 0 else pure (pure ())
Instances For
Folding (A)synchronous Tasks #
Fold a List
of (a)synchronous tasks from right to left (i.e., a right fold) into a single task.
Equations
- Lake.foldLeftListAsync f init tasks = List.foldrM (Lake.seqWithAsync f) (pure init) tasks
Instances For
Fold an Array
of (a)synchronous tasks from right to left (i.e., a right fold) into a single task.
Equations
- Lake.foldLeftArrayAsync f init tasks = Array.foldrM (Lake.seqWithAsync f) (pure init) tasks (Array.size tasks)
Instances For
Fold a List
of (a)synchronous tasks from left to right (i.e., a left fold) into a single task.
Equations
- Lake.foldRightListAsync f init tasks = List.foldlM (Lake.seqWithAsync f) (pure init) tasks
Instances For
Fold an Array
of (a)synchronous tasks from left to right (i.e., a left fold) into a single task.
Equations
- Lake.foldRightArrayAsync f init tasks = Array.foldlM (Lake.seqWithAsync f) (pure init) tasks 0