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

class Lake.Sync (m : Type u → Type v) (n : outParam (Type u' → Type w)) (k : outParam (Type u → Type u')) : Type (max (max (u + 1) v) w)

• sync : {α : Type u} → m α → n (k α)

  Run the monadic action as a synchronous task.

class Lake.Async (m : Type u → Type v) (n : outParam (Type u' → Type w)) (k : outParam (Type u → Type u')) : Type (max (max (u + 1) v) w)

• async : {α : Type u} → m α → n (k α)

  Run the monadic action as an asynchronous task.

class Lake.Await (k : Type u → Type v) (m : outParam (Type u → Type w)) : Type (max (max (u + 1) v) w)

• await : {α : Type u} → k α → m α

  Wait for an (a)synchronous task to finish.

Standard Instances

instance Lake.instSyncIdTask : Lake.Sync Id Id Task

Equations

• Lake.instSyncIdTask = { sync := fun {α : Type u_1} => Task.pure }

instance Lake.instSyncBaseIOBaseIOTask : Lake.Sync BaseIO BaseIO Lake.BaseIOTask

Equations

• Lake.instSyncBaseIOBaseIOTask = { sync := fun {α : Type} => Functor.map Task.pure }

instance Lake.instSyncReaderTReaderT {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {k : Type u_1 → Type u_1} {ρ : Type u_1} [Lake.Sync m n k] : Lake.Sync (ReaderT ρ m) (ReaderT ρ n) k

Equations

• Lake.instSyncReaderTReaderT = { sync := fun {α : Type u_1} (x : ReaderT ρ m α) (r : ρ) => Lake.sync (x r) }

instance Lake.instSyncExceptTExceptT {m : Type u_1 → Type u_2} {n : Type u_3 → Type u_4} {k : Type u_1 → Type u_3} {ε : Type u_1} [Lake.Sync m n k] : Lake.Sync (ExceptT ε m) n (ExceptT ε k)

Equations

• Lake.instSyncExceptTExceptT = { sync := fun {α : Type u_1} (x : ExceptT ε m α) => cast ⋯ (Lake.sync (ExceptT.run x)) }

instance Lake.instSyncOptionTOptionT {m : Type u_1 → Type u_2} {n : Type u_3 → Type u_4} {k : Type u_1 → Type u_3} [Lake.Sync m n k] : Lake.Sync (OptionT m) n (OptionT k)

Equations

• Lake.instSyncOptionTOptionT = { sync := fun {α : Type u_1} (x : OptionT m α) => cast ⋯ (Lake.sync (OptionT.run x)) }

instance Lake.instSyncEIOBaseIOEIOTask {ε : Type} : Lake.Sync (EIO ε) BaseIO (Lake.EIOTask ε)

Equations

• Lake.instSyncEIOBaseIOEIOTask = { sync := fun {α : Type} (x : EIO ε α) => Lake.sync (ExceptT.mk (EIO.toBaseIO x)) }

instance Lake.instSyncOptionIOBaseIOOptionIOTask : Lake.Sync Lake.OptionIO BaseIO Lake.OptionIOTask

Equations

• Lake.instSyncOptionIOBaseIOOptionIOTask = { sync := fun {α : Type} (x : Lake.OptionIO α) => Lake.sync (OptionT.mk (Lake.OptionIO.toBaseIO x)) }

instance Lake.instAsyncIdTask : Lake.Async Id Id Task

Equations

• Lake.instAsyncIdTask = { async := fun {α : Type u_1} => Task.pure }

instance Lake.instAsyncBaseIOBaseIOTask : Lake.Async BaseIO BaseIO Lake.BaseIOTask

Equations

• Lake.instAsyncBaseIOBaseIOTask = { async := fun {α : Type} (act : BaseIO α) => BaseIO.asTask act }

instance Lake.instAsyncReaderTReaderT {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {k : Type u_1 → Type u_1} {ρ : Type u_1} [Lake.Async m n k] : Lake.Async (ReaderT ρ m) (ReaderT ρ n) k

Equations

• Lake.instAsyncReaderTReaderT = { async := fun {α : Type u_1} (x : ReaderT ρ m α) (r : ρ) => Lake.async (x r) }

instance Lake.instAsyncExceptTExceptT {m : Type u_1 → Type u_2} {n : Type u_3 → Type u_4} {k : Type u_1 → Type u_3} {ε : Type u_1} [Lake.Async m n k] : Lake.Async (ExceptT ε m) n (ExceptT ε k)

Equations

• Lake.instAsyncExceptTExceptT = { async := fun {α : Type u_1} (x : ExceptT ε m α) => cast ⋯ (Lake.async (ExceptT.run x)) }

instance Lake.instAsyncOptionTOptionT {m : Type u_1 → Type u_2} {n : Type u_3 → Type u_4} {k : Type u_1 → Type u_3} [Lake.Async m n k] : Lake.Async (OptionT m) n (OptionT k)

Equations

• Lake.instAsyncOptionTOptionT = { async := fun {α : Type u_1} (x : OptionT m α) => cast ⋯ (Lake.async (OptionT.run x)) }

instance Lake.instAsyncEIOBaseIOEIOTask {ε : Type} : Lake.Async (EIO ε) BaseIO (Lake.EIOTask ε)

Equations

• Lake.instAsyncEIOBaseIOEIOTask = { async := fun {α : Type} (x : EIO ε α) => Lake.async (ExceptT.mk (EIO.toBaseIO x)) }

instance Lake.instAsyncOptionIOBaseIOOptionIOTask : Lake.Async Lake.OptionIO BaseIO Lake.OptionIOTask

Equations

• Lake.instAsyncOptionIOBaseIOOptionIOTask = { async := fun {α : Type} (x : Lake.OptionIO α) => Lake.async (OptionT.mk (Lake.OptionIO.toBaseIO x)) }

instance Lake.instAwaitTaskId : Lake.Await Task Id

Equations

• Lake.instAwaitTaskId = { await := fun {α : Type u_1} => Task.get }

instance Lake.instAwaitEIOTaskEIO {ε : Type} : Lake.Await (Lake.EIOTask ε) (EIO ε)

Equations

• Lake.instAwaitEIOTaskEIO = { await := fun {α : Type} (x : Lake.EIOTask ε α) => liftM (IO.wait x) >>= liftM }

instance Lake.instAwaitOptionIOTaskOptionIO : Lake.Await Lake.OptionIOTask Lake.OptionIO

Equations

• Lake.instAwaitOptionIOTaskOptionIO = { await := fun {α : Type} (x : Lake.OptionIOTask α) => liftM (IO.wait x) >>= liftM }

instance Lake.instAwaitExceptTExceptT {k : Type u_1 → Type u_2} {m : Type u_1 → Type u_3} {ε : Type u_1} [Lake.Await k m] : Lake.Await (ExceptT ε k) (ExceptT ε m)

Equations

• Lake.instAwaitExceptTExceptT = { await := fun {α : Type u_1} (x : ExceptT ε k α) => ExceptT.mk (Lake.await (ExceptT.run x)) }

instance Lake.instAwaitOptionTOptionT {k : Type u_1 → Type u_2} {m : Type u_1 → Type u_3} [Lake.Await k m] : Lake.Await (OptionT k) (OptionT m)

Equations

• Lake.instAwaitOptionTOptionT = { await := fun {α : Type u_1} (x : OptionT k α) => OptionT.mk (Lake.await (OptionT.run x)) }

Combinators

class Lake.BindSync (m : Type u → Type v) (n : outParam (Type u' → Type w)) (k : outParam (Type u → Type u')) : Type (max (max (max (u + 1) u') v) w)

• bindSync : {α β : Type u} → Task.Priority → k α → (α → m β) → n (k β)

  Perform a synchronous action after another (a)synchronous task completes successfully.

class Lake.BindAsync (n : Type u → Type v) (k : Type u → Type u) : Type (max (u + 1) v)

• bindAsync : {α β : Type u} → k α → (α → n (k β)) → n (k β)

  Perform a asynchronous task after another (a)synchronous task completes successfully.

class Lake.SeqAsync (n : outParam (Type u → Type v)) (k : Type u → Type u) : Type (max (u + 1) v)

• seqAsync : {α β : Type u} → k (α → β) → k α → n (k β)

  Combine two (a)synchronous tasks, applying the result of the second one to the first one.

class Lake.SeqLeftAsync (n : outParam (Type u → Type v)) (k : Type u → Type u) : Type (max (u + 1) v)

• seqLeftAsync : {α β : Type u} → k α → k β → n (k α)

  Combine two (a)synchronous tasks, returning the result of the first one.

class Lake.SeqRightAsync (n : outParam (Type u → Type v)) (k : Type u → Type u) : Type (max (u + 1) v)

• seqRightAsync : {α β : Type u} → k α → k β → n (k β)

  Combine two (a)synchronous tasks, returning the result of the second one.

class Lake.SeqWithAsync (n : outParam (Type u → Type v)) (k : Type u → Type u) : Type (max (u + 1) v)

• seqWithAsync : {γ α β : Type u} → (α → β → γ) → k α → k β → n (k γ)

  Combine two (a)synchronous tasks using f.

class Lake.ApplicativeAsync (n : outParam (Type u → Type v)) (k : Type u → Type u) extends Lake.SeqAsync , Lake.SeqLeftAsync , Lake.SeqRightAsync , Lake.SeqWithAsync : Type (max (u + 1) v)

Standard Instances

instance Lake.instBindSyncIdTask : Lake.BindSync Id Id Task

Equations

• Lake.instBindSyncIdTask = { bindSync := fun {α β : Type u_1} (x : Task.Priority) => flip fun (f : α → Id β) (x : Task α) => Task.map f x Task.Priority.default }

instance Lake.instBindSyncBaseIOBaseIOTask : Lake.BindSync BaseIO BaseIO Lake.BaseIOTask

Equations

• Lake.instBindSyncBaseIOBaseIOTask = { bindSync := fun {α β : Type} (x : Task.Priority) => flip fun (f : α → BaseIO β) (t : Task α) => BaseIO.mapTask f t Task.Priority.default }

instance Lake.instBindSyncEIOBaseIOETask {ε : Type} : Lake.BindSync (EIO ε) BaseIO (Lake.ETask ε)

Equations

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

instance Lake.instBindSyncOptionIOBaseIOOptionIOTask : Lake.BindSync Lake.OptionIO BaseIO Lake.OptionIOTask

Equations

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

instance Lake.instBindSyncReaderTReaderT {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {k : Type u_1 → Type u_1} {ρ : Type u_1} [Lake.BindSync m n k] : Lake.BindSync (ReaderT ρ m) (ReaderT ρ n) k

Equations

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

instance Lake.instBindSyncExceptTExceptT {m : Type u_1 → Type u_2} {n : Type u_3 → Type u_4} {k : Type u_1 → Type u_3} {ε : Type u_1} [Lake.BindSync m n k] [Pure m] : Lake.BindSync (ExceptT ε m) n (ExceptT ε k)

Equations

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

instance Lake.instBindSyncOptionTOptionT {m : Type u_1 → Type u_2} {n : Type u_3 → Type u_4} {k : Type u_1 → Type u_3} [Lake.BindSync m n k] [Pure m] : Lake.BindSync (OptionT m) n (OptionT k)

Equations

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

instance Lake.instBindAsyncIdTask : Lake.BindAsync Id Task

Equations

• Lake.instBindAsyncIdTask = { bindAsync := fun {α β : Type u_1} (x : Task α) (f : α → Task β) => Task.bind x f Task.Priority.default }

instance Lake.instBindAsyncBaseIOBaseIOTask : Lake.BindAsync BaseIO Lake.BaseIOTask

Equations

• Lake.instBindAsyncBaseIOBaseIOTask = { bindAsync := fun {α β : Type} (t : Task α) (f : α → BaseIO (Task β)) => BaseIO.bindTask t f Task.Priority.default }

instance Lake.instBindAsyncBaseIOEIOTask {ε : Type} : Lake.BindAsync BaseIO (Lake.EIOTask ε)

Equations

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

instance Lake.instBindAsyncBaseIOOptionIOTask : Lake.BindAsync BaseIO Lake.OptionIOTask

Equations

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

instance Lake.instBindAsyncReaderT {n : Type u_1 → Type u_2} {k : Type u_1 → Type u_1} {ρ : Type u_1} [Lake.BindAsync n k] : Lake.BindAsync (ReaderT ρ n) k

Equations

• Lake.instBindAsyncReaderT = { bindAsync := fun {α β : Type u_1} (ka : k α) (f : α → ReaderT ρ n (k β)) (r : ρ) => Lake.bindAsync ka fun (a : α) => f a r }

instance Lake.instBindAsyncExceptT {n : Type u_1 → Type u_2} {k : Type u_1 → Type u_1} {ε : Type u_1} [Lake.BindAsync n k] [Pure n] [Pure k] : Lake.BindAsync n (ExceptT ε k)

Equations

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

instance Lake.instBindAsyncOptionT {n : Type u_1 → Type u_2} {k : Type u_1 → Type u_1} [Lake.BindAsync n k] [Pure n] [Pure k] : Lake.BindAsync n (OptionT k)

Equations

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

instance Lake.instApplicativeAsyncIdTask : Lake.ApplicativeAsync Id Task

Equations

• Lake.instApplicativeAsyncIdTask = Lake.ApplicativeAsync.mk

instance Lake.instApplicativeAsyncBaseIOBaseIOTask : Lake.ApplicativeAsync BaseIO Lake.BaseIOTask

Equations

• Lake.instApplicativeAsyncBaseIOBaseIOTask = Lake.ApplicativeAsync.mk

instance Lake.instApplicativeAsyncExceptT {n : Type u_1 → Type u_2} {k : Type u_1 → Type u_1} {ε : Type u_1} [Lake.ApplicativeAsync n k] : Lake.ApplicativeAsync n (ExceptT ε k)

Equations

• Lake.instApplicativeAsyncExceptT = Lake.ApplicativeAsync.mk

instance Lake.instApplicativeAsyncOptionT {n : Type u_1 → Type u_2} {k : Type u_1 → Type u_1} [Lake.ApplicativeAsync n k] : Lake.ApplicativeAsync n (OptionT k)

Equations

• Lake.instApplicativeAsyncOptionT = Lake.ApplicativeAsync.mk

List/Array Utilities

Sequencing (A)synchronous Tasks

def Lake.seqLeftList1Async {n : Type u_1 → Type u_2} {k : Type u_1 → Type u_1} {α : Type u_1} [Lake.SeqLeftAsync n k] [Monad n] (last : k α) (tasks : List (k α)) : n (k α)

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

def Lake.seqLeftListAsync {n : Type → Type u_1} {k : Type → Type} [Lake.SeqLeftAsync n k] [Monad n] [Pure k] (tasks : List (k PUnit)) : n (k PUnit)

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

def Lake.seqRightListAsync {n : Type → Type u_1} {k : Type → Type} [Lake.SeqRightAsync n k] [Monad n] [Pure k] (tasks : List (k PUnit)) : n (k PUnit)

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

def Lake.seqLeftArrayAsync {n : Type → Type u_1} {k : Type → Type} [Lake.SeqLeftAsync n k] [Monad n] [Pure k] (tasks : Array (k PUnit)) : n (k PUnit)

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.

def Lake.seqRightArrayAsync {n : Type → Type u_1} {k : Type → Type} [Lake.SeqRightAsync n k] [Monad n] [Pure k] (tasks : Array (k PUnit)) : n (k PUnit)

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

Folding (A)synchronous Tasks

def Lake.foldLeftListAsync {n : Type u_1 → Type u_2} {k : Type u_1 → Type u_1} [Lake.SeqWithAsync n k] [Monad n] [Pure k] {α : Type u_1} {β : Type u_1} (f : α → β → β) (init : β) (tasks : List (k α)) : n (k β)

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

def Lake.foldLeftArrayAsync {n : Type u_1 → Type u_2} {k : Type u_1 → Type u_1} [Lake.SeqWithAsync n k] [Monad n] [Pure k] {α : Type u_1} {β : Type u_1} (f : α → β → β) (init : β) (tasks : Array (k α)) : n (k β)

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)

def Lake.foldRightListAsync {n : Type u_1 → Type u_2} {k : Type u_1 → Type u_1} [Lake.SeqWithAsync n k] [Monad n] [Pure k] {β : Type u_1} {α : Type u_1} (f : β → α → β) (init : β) (tasks : List (k α)) : n (k β)

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

def Lake.foldRightArrayAsync {n : Type u_1 → Type u_2} {k : Type u_1 → Type u_1} [Lake.SeqWithAsync n k] [Monad n] [Pure k] {β : Type u_1} {α : Type u_1} (f : β → α → β) (init : β) (tasks : Array (k α)) : n (k β)

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