Documentation

Lake.Util.Async

This module Defines the asynchronous monadic interface for Lake. The interface is composed of three major abstract monadic types:

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.

Instances
    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
      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 #

        Equations
        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 {α} x 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
        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] :
        Equations
        Equations
        Equations
        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 {α} x 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
        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] :
        Equations
        Equations
        Equations
        Equations
        • Lake.instAwaitEIOTaskEIO = { await := fun {α} x => 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
        instance Lake.instAwaitOptionTOptionT {k : Type u_1 → Type u_2} {m : Type u_1 → Type u_3} [Lake.Await k m] :
        Equations

        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.Priorityk α(αm β) → n (k β)

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

        Instances
          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
            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
              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
                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
                  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
                    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 #

                        Equations
                        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.
                        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
                        • Lake.instBindSyncReaderTReaderT = { bindSync := fun {α β} prio ka f r => Lake.bindSync prio ka fun a => f a r }
                        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] :
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Equations
                        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.
                        instance Lake.instBindAsyncReaderT {n : Type u_1 → Type u_2} {k : Type u_1 → Type u_1} {ρ : Type u_1} [Lake.BindAsync n k] :
                        Equations
                        • Lake.instBindAsyncReaderT = { bindAsync := fun {α β} ka f 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] :
                        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] :
                        Equations
                        • One or more equations did not get rendered due to their size.
                        instance Lake.instApplicativeAsyncExceptT {n : Type u_1 → Type u_2} {k : Type u_1 → Type u_1} {ε : Type u_1} [Lake.ApplicativeAsync n 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] :
                        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
                        Instances For
                          def Lake.seqLeftListAsync {n : TypeType u_1} {k : TypeType} [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
                          Instances For
                            def Lake.seqRightListAsync {n : TypeType u_1} {k : TypeType} [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
                            Instances For
                              def Lake.seqLeftArrayAsync {n : TypeType u_1} {k : TypeType} [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.
                              Instances For
                                def Lake.seqRightArrayAsync {n : TypeType u_1} {k : TypeType} [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
                                Instances For

                                  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
                                  Instances For
                                    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
                                    Instances For
                                      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
                                      Instances For
                                        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
                                        Instances For