Documentation

Std.Internal.Async.Basic

Asynchronous Programming Primitives #

This module provides a layered approach to asynchronous programming, combining monadic types, type classes, and concrete task types that work together in a cohesive system.

Monadic Types #

These types provide a good way to to chain and manipulate context. These can contain a Task, enabling manipulation of both asynchronous and synchronous code.

Concurrent Units of Work #

These are the concrete computational units that exist within the monadic contexts. These types should not be created directly.

Relation #

These types are related by two functions in the type classes MonadAsync and MonadAwait: async and await. The async function extracts a concrete asynchronous task from a computation within the monadic context. In effect, it runs the computation in the background and returns a task handle that can be awaited later. On the other hand, the await function takes a task and re-inserts it into the monadic context, allowing its result to be composed using monadic bind and also pausing to wait for that result. This relationship between async and await enables precise control over when a computation begins and when its result is used. You can spawn multiple asynchronous tasks using async, perform other operations in the meantime, and later rejoin the computation flow by awaiting their results.

These functions should not be used directly. Instead, prefer higher-level combinators such as race, raceAll, concurrently, background and concurrentlyAll. The best way to think about how to write your async code, it to avoid using the concurrent units of work, and only use it when integrating with non async code that uses them.

class Std.Internal.IO.Async.MonadAwait (t m : TypeType) extends Monad m :

Typeclass for monads that can "await" a computation of type t α in a monad m until the result is available.

  • map {α β : Type} : (αβ)m αm β
  • mapConst {α β : Type} : αm βm α
  • pure {α : Type} : αm α
  • seq {α β : Type} : m (αβ)(Unitm α)m β
  • seqLeft {α β : Type} : m α(Unitm β)m α
  • seqRight {α β : Type} : m α(Unitm β)m β
  • bind {α β : Type} : m α(αm β)m β
  • await {α : Type} : t αm α

    Awaits the result of t α and returns it inside the m monad.

Instances
    class Std.Internal.IO.Async.MonadAsync (t m : TypeType) extends Monad m :

    Represents monads that can launch computations asynchronously of type t in a monad m.

    Instances
      @[defaultInstance 1000]
      Equations
      @[defaultInstance 1000]
      Equations
      • One or more equations did not get rendered due to their size.
      @[defaultInstance 1000]
      Equations
      • One or more equations did not get rendered due to their size.
      @[defaultInstance 1000]
      Equations
      • One or more equations did not get rendered due to their size.
      @[reducible, inline]

      A Task that may resolve to either a value of type α or an error value of type ε.

      Equations
      Instances For
        @[inline]
        def Std.Internal.IO.Async.ETask.pure {α ε : Type} (x : α) :
        ETask ε α

        Construct an ETask that is already resolved with value x.

        Equations
        Instances For
          @[inline]
          def Std.Internal.IO.Async.ETask.map {α β ε : Type} (f : αβ) (x : ETask ε α) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) :
          ETask ε β

          Creates a new ETask that will run after x has finished. If x:

          • errors, return an ETask that resolves to the error.
          • succeeds, return an ETask that resolves to f x.
          Equations
          Instances For
            @[inline]
            def Std.Internal.IO.Async.ETask.bind {ε α β : Type} (x : ETask ε α) (f : αETask ε β) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) :
            ETask ε β

            Creates a new ETask that will run after x has completed. If x:

            • errors, return an ETask that resolves to the error.
            • succeeds, run f on the result of x and return the ETask produced by f.
            Equations
            Instances For
              @[inline]
              def Std.Internal.IO.Async.ETask.bindEIO {ε α β : Type} (x : ETask ε α) (f : αEIO ε (ETask ε β)) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) :
              EIO ε (ETask ε β)

              Similar to bind, however f has access to the EIO monad. If f throws an error, the returned ETask resolves to that error.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[inline]
                def Std.Internal.IO.Async.ETask.mapEIO {α ε β : Type} (f : αEIO ε β) (x : ETask ε α) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) :
                BaseIO (ETask ε β)

                Similar to bind, however f has access to the EIO monad. If f throws an error, the returned ETask resolves to that error.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[inline]
                  def Std.Internal.IO.Async.ETask.block {ε α : Type} (x : ETask ε α) :
                  EIO ε α

                  Block until the ETask in x finishes and returns its value. Propagates any error encountered during execution.

                  Equations
                  Instances For
                    @[inline]

                    Create an ETask that resolves to the value of the promise x.

                    Equations
                    Instances For
                      @[inline]

                      Create an ETask that resolves to the pure value of the promise x.

                      Equations
                      Instances For
                        @[inline]

                        Obtain the IO.TaskState of x.

                        Equations
                        Instances For
                          Equations
                          • One or more equations did not get rendered due to their size.
                          @[reducible, inline]

                          A Task that may resolve to a value or an error value of type IO.Error. Alias for ETask IO.Error.

                          Equations
                          Instances For
                            @[inline]
                            def Std.Internal.IO.Async.AsyncTask.mapIO {α β : Type} (f : αIO β) (x : AsyncTask α) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) :

                            Similar to map, however f has access to the IO monad. If f throws an error, the returned AsyncTask resolves to that error.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              @[inline]

                              Construct an AsyncTask that is already resolved with value x.

                              Equations
                              Instances For
                                @[inline]
                                def Std.Internal.IO.Async.AsyncTask.bind {α β : Type} (x : AsyncTask α) (f : αAsyncTask β) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) :

                                Create a new AsyncTask that will run after x has finished. If x:

                                • errors, return an AsyncTask that resolves to the error.
                                • succeeds, run f on the result of x and return the AsyncTask produced by f.
                                Equations
                                Instances For
                                  @[inline]
                                  def Std.Internal.IO.Async.AsyncTask.map {α β : Type} (f : αβ) (x : AsyncTask α) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) :

                                  Create a new AsyncTask that will run after x has finished. If x:

                                  • errors, return an AsyncTask that resolves to the error.
                                  • succeeds, return an AsyncTask that resolves to f x.
                                  Equations
                                  Instances For
                                    @[inline]
                                    def Std.Internal.IO.Async.AsyncTask.bindIO {α β : Type} (x : AsyncTask α) (f : αIO (AsyncTask β)) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) :

                                    Similar to bind, however f has access to the IO monad. If f throws an error, the returned AsyncTask resolves to that error.

                                    Equations
                                    Instances For
                                      @[inline]
                                      def Std.Internal.IO.Async.AsyncTask.mapTaskIO {α β : Type} (f : αIO β) (x : AsyncTask α) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) :

                                      Similar to map, however f has access to the IO monad. If f throws an error, the returned AsyncTask resolves to that error.

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

                                        Block until the AsyncTask in x finishes.

                                        Equations
                                        Instances For
                                          @[inline]

                                          Create an AsyncTask that resolves to the value of x.

                                          Equations
                                          Instances For
                                            @[inline]

                                            Obtain the IO.TaskState of x.

                                            Equations
                                            Instances For

                                              A MaybeTask α represents a computation that either:

                                              • Is immediately available as an α value, or
                                              • Is an asynchronous computation that will eventually produce an α value.
                                              Instances For
                                                @[inline]

                                                Gets the value of the MaybeTask by blocking.

                                                Equations
                                                Instances For
                                                  @[inline]
                                                  def Std.Internal.IO.Async.MaybeTask.bind {α β : Type} (t : MaybeTask α) (f : αMaybeTask β) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) :

                                                  Sequences two computations, allowing the second to depend on the value computed by the first.

                                                  Equations
                                                  Instances For
                                                    @[inline]

                                                    Join the MaybeTask to an Task.

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

                                                      An asynchronous computation that never fails.

                                                      Equations
                                                      Instances For
                                                        @[inline]

                                                        Converts a BaseIO into a BaseAsync

                                                        Equations
                                                        Instances For
                                                          @[inline]

                                                          Converts a BaseAsync into a BaseIO

                                                          Equations
                                                          Instances For
                                                            @[inline]

                                                            Creates a BaseAsync computation that immediately returns the given value.

                                                            Equations
                                                            Instances For
                                                              @[inline]
                                                              def Std.Internal.IO.Async.BaseAsync.map {α β : Type} (f : αβ) (self : BaseAsync α) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) :

                                                              Maps the result of a BaseAsync computation with a function.

                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                @[inline]
                                                                def Std.Internal.IO.Async.BaseAsync.bind {α β : Type} (self : BaseAsync α) (f : αBaseAsync β) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) :

                                                                Sequences two computations, allowing the second to depend on the value computed by the first.

                                                                Equations
                                                                Instances For
                                                                  Equations
                                                                  Instances For
                                                                    @[inline]

                                                                    Waits for the result of the BaseAsync computation, blocking if necessary.

                                                                    Equations
                                                                    Instances For
                                                                      @[inline]

                                                                      Lifts a BaseAsync computation into a Task that can be awaited and joined.

                                                                      Equations
                                                                      Instances For
                                                                        @[inline]

                                                                        Creates a BaseAsync that awaits the completion of the given Task α.

                                                                        Equations
                                                                        Instances For
                                                                          @[inline]

                                                                          Returns the BaseAsync computation inside a Task α, so it can be awaited.

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

                                                                            An asynchronous computation that may produce an error of type ε.

                                                                            Equations
                                                                            Instances For
                                                                              @[inline]
                                                                              def Std.Internal.IO.Async.EAsync.pure {α ε : Type} (a : α) :
                                                                              EAsync ε α

                                                                              Creates an EAsync computation that immediately returns the given value.

                                                                              Equations
                                                                              Instances For
                                                                                @[inline]
                                                                                def Std.Internal.IO.Async.EAsync.map {α β ε : Type} (f : αβ) (self : EAsync ε α) :
                                                                                EAsync ε β

                                                                                Maps the result of an EAsync computation with a pure function.

                                                                                Equations
                                                                                Instances For
                                                                                  @[inline]
                                                                                  def Std.Internal.IO.Async.EAsync.bind {ε α β : Type} (self : EAsync ε α) (f : αEAsync ε β) :
                                                                                  EAsync ε β

                                                                                  Sequences two computations, allowing the second to depend on the value computed by the first.

                                                                                  Equations
                                                                                  • One or more equations did not get rendered due to their size.
                                                                                  Instances For
                                                                                    @[inline]
                                                                                    def Std.Internal.IO.Async.EAsync.lift {ε α : Type} (x : EIO ε α) :
                                                                                    EAsync ε α

                                                                                    Lifts an EIO action into an EAsync computation.

                                                                                    Equations
                                                                                    Instances For
                                                                                      @[inline]
                                                                                      def Std.Internal.IO.Async.EAsync.wait {ε α : Type} (self : EAsync ε α) :
                                                                                      EIO ε α

                                                                                      Waits for the result of the EAsync computation, blocking if necessary.

                                                                                      Equations
                                                                                      Instances For
                                                                                        @[inline]

                                                                                        Lifts an EAsync computation into an ETask that can be awaited and joined.

                                                                                        Equations
                                                                                        Instances For
                                                                                          @[inline]
                                                                                          def Std.Internal.IO.Async.EAsync.throw {ε α : Type} (e : ε) :
                                                                                          EAsync ε α

                                                                                          Raises an error of type ε within the EAsync monad.

                                                                                          Equations
                                                                                          Instances For
                                                                                            @[inline]
                                                                                            def Std.Internal.IO.Async.EAsync.tryCatch {ε α : Type} (x : EAsync ε α) (f : εEAsync ε α) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) :
                                                                                            EAsync ε α

                                                                                            Handles errors in an EAsync computation by running a handler if one occurs.

                                                                                            Equations
                                                                                            • One or more equations did not get rendered due to their size.
                                                                                            Instances For
                                                                                              def Std.Internal.IO.Async.EAsync.tryFinally' {ε α β : Type} (x : EAsync ε α) (f : Option αEAsync ε β) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) :
                                                                                              EAsync ε (α × β)

                                                                                              Runs an action, ensuring that some other action always happens afterward.

                                                                                              Equations
                                                                                              • One or more equations did not get rendered due to their size.
                                                                                              Instances For
                                                                                                @[inline]
                                                                                                def Std.Internal.IO.Async.EAsync.await {ε α : Type} (x : ETask ε α) :
                                                                                                EAsync ε α

                                                                                                Creates an EAsync computation that awaits the completion of the given ETask ε α.

                                                                                                Equations
                                                                                                Instances For
                                                                                                  @[inline]

                                                                                                  Returns the EAsync computation inside an ETask ε α, so it can be awaited.

                                                                                                  Equations
                                                                                                  Instances For
                                                                                                    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
                                                                                                    • 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
                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                    @[inline]
                                                                                                    def Std.Internal.IO.Async.EAsync.forIn {ε β : Type} [i : Inhabited ε] (init : β) (f : UnitβEAsync ε (ForInStep β)) (prio : Task.Priority := Task.Priority.default) :
                                                                                                    EAsync ε β
                                                                                                    Equations
                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                    Instances For
                                                                                                      @[specialize #[]]
                                                                                                      partial def Std.Internal.IO.Async.EAsync.forIn.loop {ε β : Type} (f : UnitβEAsync ε (ForInStep β)) (prio : Task.Priority := Task.Priority.default) (promise : IO.Promise (Except ε β)) (b : β) :
                                                                                                      EAsync ε (ETask ε Unit)
                                                                                                      Equations
                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                      @[reducible, inline]

                                                                                                      An asynchronous computation that may produce an error of type IO.Error..

                                                                                                      Equations
                                                                                                      Instances For
                                                                                                        @[inline, specialize #[]]
                                                                                                        def Std.Internal.IO.Async.background {m t : TypeType} {α : Type} [Monad m] [MonadAsync t m] (prio : Task.Priority := Task.Priority.default) :
                                                                                                        m αm Unit

                                                                                                        This function transforms the operation inside the monad m into a task and let it run in the background.

                                                                                                        Equations
                                                                                                        Instances For
                                                                                                          @[inline, specialize #[]]
                                                                                                          def Std.Internal.IO.Async.concurrently {m t : TypeType} {α β : Type} [Monad m] [MonadAwait t m] [MonadAsync t m] (x : m α) (y : m β) (prio : Task.Priority := Task.Priority.default) :
                                                                                                          m (α × β)

                                                                                                          Runs two computations concurrently and returns both results as a pair.

                                                                                                          Equations
                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                          Instances For
                                                                                                            @[inline, specialize #[]]
                                                                                                            def Std.Internal.IO.Async.race {m t : TypeType} {α : Type} [MonadLiftT BaseIO m] [MonadAwait Task m] [MonadAsync t m] [MonadAwait t m] [Monad m] [Inhabited α] (x y : m α) (prio : Task.Priority := Task.Priority.default) :
                                                                                                            m α

                                                                                                            Runs two computations concurrently and returns the result of the one that finishes first. The other result is lost and the other task is not cancelled, so the task will continue the execution until the end.

                                                                                                            Equations
                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                            Instances For
                                                                                                              @[inline, specialize #[]]
                                                                                                              def Std.Internal.IO.Async.concurrentlyAll {m t : TypeType} {α : Type} [Monad m] [MonadAwait t m] [MonadAsync t m] (xs : Array (m α)) (prio : Task.Priority := Task.Priority.default) :
                                                                                                              m (Array α)

                                                                                                              Runs all computations in an Array concurrently and returns all results as an array.

                                                                                                              Equations
                                                                                                              Instances For
                                                                                                                @[inline, specialize #[]]
                                                                                                                def Std.Internal.IO.Async.raceAll {m : TypeType} {c : Type u_1} {α : Type} {t : TypeType} [ForM m c (m α)] [MonadLiftT BaseIO m] [MonadAwait Task m] [MonadAsync t m] [MonadAwait t m] [Monad m] [Inhabited α] (xs : c) (prio : Task.Priority := Task.Priority.default) :
                                                                                                                m α

                                                                                                                Runs all computations concurrently and returns the result of the first one to finish. All other results are lost, and the tasks are not cancelled, so they'll continue their executing until the end.

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