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 #

source

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.

Instances

source

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.

Instances

source

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.

Instances

Standard Instances #

source

instance Lake.instSyncIdTask :

Lake.Sync Id Id Task

source

instance Lake.instSyncBaseIOBaseIOTask :

Lake.Sync BaseIO BaseIO Lake.BaseIOTask

source

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

source

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)

source

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)

source

instance Lake.instSyncEIOBaseIOEIOTask {ε : Type} :

Lake.Sync (EIO ε) BaseIO (Lake.EIOTask ε)

source

instance Lake.instSyncOptionIOBaseIOOptionIOTask :

Lake.Sync Lake.OptionIO BaseIO Lake.OptionIOTask

source

instance Lake.instAsyncIdTask :

Lake.Async Id Id Task

source

instance Lake.instAsyncBaseIOBaseIOTask :

Lake.Async BaseIO BaseIO Lake.BaseIOTask

source

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

source

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)

source

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)

source

instance Lake.instAsyncEIOBaseIOEIOTask {ε : Type} :

Lake.Async (EIO ε) BaseIO (Lake.EIOTask ε)

source

instance Lake.instAsyncOptionIOBaseIOOptionIOTask :

Lake.Async Lake.OptionIO BaseIO Lake.OptionIOTask

source

instance Lake.instAwaitTaskId :

Lake.Await Task Id

source

instance Lake.instAwaitEIOTaskEIO {ε : Type} :

Lake.Await (Lake.EIOTask ε) (EIO ε)

source

instance Lake.instAwaitOptionIOTaskOptionIO :

Lake.Await Lake.OptionIOTask Lake.OptionIO

source

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)

source

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)

Combinators #

source

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.

Instances

source

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.

Instances

source

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 ot the first one.

Instances

source

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.

Instances

source

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.

Instances

source

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.

Instances

source

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)

Instances

Standard Instances #

source

instance Lake.instBindSyncIdTask :

Lake.BindSync Id Id Task

source

instance Lake.instBindSyncBaseIOBaseIOTask :

Lake.BindSync BaseIO BaseIO Lake.BaseIOTask

source

instance Lake.instBindSyncEIOBaseIOETask {ε : Type} :

Lake.BindSync (EIO ε) BaseIO (Lake.ETask ε)

source

instance Lake.instBindSyncOptionIOBaseIOOptionIOTask :

Lake.BindSync Lake.OptionIO BaseIO Lake.OptionIOTask

source

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

source

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)

source

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)

source

instance Lake.instBindAsyncIdTask :

Lake.BindAsync Id Task

source

instance Lake.instBindAsyncBaseIOBaseIOTask :

Lake.BindAsync BaseIO Lake.BaseIOTask

source

instance Lake.instBindAsyncBaseIOEIOTask {ε : Type} :

Lake.BindAsync BaseIO (Lake.EIOTask ε)

source

instance Lake.instBindAsyncBaseIOOptionIOTask :

Lake.BindAsync BaseIO Lake.OptionIOTask

source

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

source

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)

source

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)

source

instance Lake.instApplicativeAsyncIdTask :

Lake.ApplicativeAsync Id Task

source

instance Lake.instApplicativeAsyncBaseIOBaseIOTask :

Lake.ApplicativeAsync BaseIO Lake.BaseIOTask

source

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)

source

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)

List/Array Utilities #

Sequencing (A)synchronous Tasks #

source

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

Instances For

source

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.

Instances For

source

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.

Instances For

source

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.

Instances For

source

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.

Instances For

Folding (A)synchronous Tasks #

source

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.

Instances For

source

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.

Instances For

source

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.

Instances For

source

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.

Instances For