21.12.1.1. Running Asynchronous Computations🔗

Asynchronous computations can be run from IO by either waiting or blocking. When a thread waits on an asynchronous computation, the asynchronous computation is run on the thread that is waiting. When a thread blocks on an asynchronous computation or task, the computation is run on a worker thread in an ordinary task with the specified priority, and the calling thread calls Task.get to block on the result. Because Async is a defined alias for EAsync, generalized field notation can be used to call EAsync.wait on a term with type Async.

Std.Async.EAsync.wait {ε α : Type} (self : EAsync ε α) : EIO ε α
Std.Async.EAsync.wait {ε α : Type}
  (self : EAsync ε α) : EIO ε α

Std.Async.BaseAsync.wait {α : Type} (self : BaseAsync α) : BaseIO α
Std.Async.BaseAsync.wait {α : Type}
  (self : BaseAsync α) : BaseIO α

Std.Async.Async.block {α : Type} (x : Async α)
  (prio : Task.Priority := Task.Priority.default) : IO α
Std.Async.Async.block {α : Type}
  (x : Async α)
  (prio : Task.Priority :=
    Task.Priority.default) :
  IO α

Std.Async.EAsync.block {ε α : Type} (x : EAsync ε α)
  (prio : Task.Priority := Task.Priority.default) : EIO ε α
Std.Async.EAsync.block {ε α : Type}
  (x : EAsync ε α)
  (prio : Task.Priority :=
    Task.Priority.default) :
  EIO ε α

Std.Async.ETask.block {ε α : Type} (x : ETask ε α) : EIO ε α
Std.Async.ETask.block {ε α : Type}
  (x : ETask ε α) : EIO ε α

Std.Async.AsyncTask.block {α : Type} (x : AsyncTask α) : IO α
Std.Async.AsyncTask.block {α : Type}
  (x : AsyncTask α) : IO α

Asynchronous computations can also be run as ordinary Tasks in IO.

Std.Async.Async.toIO {α : Type} (x : Async α) : IO (AsyncTask α)
Std.Async.Async.toIO {α : Type}
  (x : Async α) : IO (AsyncTask α)

Std.Async.EAsync.toEIO {ε α : Type} (x : EAsync ε α) : EIO ε (ETask ε α)
Std.Async.EAsync.toEIO {ε α : Type}
  (x : EAsync ε α) : EIO ε (ETask ε α)

Std.Async.BaseAsync.toBaseIO {α : Type} (x : BaseAsync α) :
  BaseIO (Task α)
Std.Async.BaseAsync.toBaseIO {α : Type}
  (x : BaseAsync α) : BaseIO (Task α)

Std.Async.EAsync.asTask {ε α : Type} (x : EAsync ε α)
  (prio : Task.Priority := Task.Priority.default) : EIO ε (ETask ε α)
Std.Async.EAsync.asTask {ε α : Type}
  (x : EAsync ε α)
  (prio : Task.Priority :=
    Task.Priority.default) :
  EIO ε (ETask ε α)

Std.Async.BaseAsync.asTask {α : Type} (x : BaseAsync α)
  (prio : Task.Priority := Task.Priority.default) : BaseIO (Task α)
Std.Async.BaseAsync.asTask {α : Type}
  (x : BaseAsync α)
  (prio : Task.Priority :=
    Task.Priority.default) :
  BaseIO (Task α)

Compared to IO.asTask, EAsync.asTask schedules an asynchronous task. While tasks from IO.asTask are synchronous, occupying their worker thread until completed, tasks from EAsync.asTask release their worker threads at suspension points and are reinvoked as needed by the libuv event loop.

21.12.1.2. Managing Tasks🔗

The typical interface to asynchronous tasks is via the MonadAsync and MonadAwait instances for a monad. Their respective methods MonadAsync.async and MonadAwait.await are exported from Std.Async. Typically, the main thread of execution will create some number of asynchronous tasks, then await their results when needed to make progress. The async and await functions are not built in to the Lean compiler, and they don't trigger a whole-program transformation. They just create or consume tasks that are associated with underlying promises in the correct manner for the framework.

Std.Async.MonadAwait (t m : Type → Type) : Type 1
Std.Async.MonadAwait (t m : Type → Type) :
  Type 1

Std.Async.MonadAwait.mk

await : {α : Type} → t α → m α

Std.Async.MonadAsync (t m : Type → Type) : Type 1
Std.Async.MonadAsync (t m : Type → Type) :
  Type 1

Std.Async.MonadAsync.mk

async : {α : Type} → m α → optParam Task.Priority Task.Priority.default → m (t α)

To launch an asynchronous task whose value will never be needed, use background.

Std.Async.background {m t : Type → Type} {α : Type} [Monad m]
  [MonadAsync t m] (action : m α)
  (prio : Task.Priority := Task.Priority.default) : m Unit
Std.Async.background {m t : Type → Type}
  {α : Type} [Monad m] [MonadAsync t m]
  (action : m α)
  (prio : Task.Priority :=
    Task.Priority.default) :
  m Unit

In addition to instances for the Async monads and tasks, the library includes instances that allow reader and state monad transformers to be used with async and await.

("green", "sweet")

21.12.1.3. Transforming and Inspecting Tasks🔗

The eventual result of an asynchronous task can be transformed without first awaiting it. AsyncTask.map applies a function to a task's result, while AsyncTask.bindIO and AsyncTask.mapTaskIO sequence further IO work onto it. In each case, an error in the original task propagates to the transformed task.

Std.Async.AsyncTask.map {α β : Type} (f : α → β) (x : AsyncTask α)
  (prio : Task.Priority := Task.Priority.default)
  (sync : Bool := false) : AsyncTask β
Std.Async.AsyncTask.map {α β : Type}
  (f : α → β) (x : AsyncTask α)
  (prio : Task.Priority :=
    Task.Priority.default)
  (sync : Bool := false) : AsyncTask β

Std.Async.AsyncTask.bindIO {α β : Type} (x : AsyncTask α)
  (f : α → IO (AsyncTask β))
  (prio : Task.Priority := Task.Priority.default)
  (sync : Bool := false) : BaseIO (AsyncTask β)
Std.Async.AsyncTask.bindIO {α β : Type}
  (x : AsyncTask α)
  (f : α → IO (AsyncTask β))
  (prio : Task.Priority :=
    Task.Priority.default)
  (sync : Bool := false) :
  BaseIO (AsyncTask β)

Std.Async.AsyncTask.mapTaskIO {α β : Type} (f : α → IO β)
  (x : AsyncTask α) (prio : Task.Priority := Task.Priority.default)
  (sync : Bool := false) : BaseIO (AsyncTask β)
Std.Async.AsyncTask.mapTaskIO {α β : Type}
  (f : α → IO β) (x : AsyncTask α)
  (prio : Task.Priority :=
    Task.Priority.default)
  (sync : Bool := false) :
  BaseIO (AsyncTask β)

A task's progress can be inspected without blocking by retrieving its IO.TaskState.

Std.Async.ETask.getState {ε α : Type} (x : ETask ε α) :
  BaseIO IO.TaskState
Std.Async.ETask.getState {ε α : Type}
  (x : ETask ε α) : BaseIO IO.TaskState

Std.Async.AsyncTask.getState {α : Type} (x : AsyncTask α) :
  BaseIO IO.TaskState
Std.Async.AsyncTask.getState {α : Type}
  (x : AsyncTask α) : BaseIO IO.TaskState

A MaybeTask is either an immediately-available value or a task that will produce one. It can be converted to an ordinary Task, have its value read by blocking, be mapped over, and have a Task of a MaybeTask collapsed into a single Task.

Std.Async.MaybeTask.toTask {α : Type} : MaybeTask α → Task α
Std.Async.MaybeTask.toTask {α : Type} :
  MaybeTask α → Task α

Std.Async.MaybeTask.get {α : Type} : MaybeTask α → α
Std.Async.MaybeTask.get {α : Type} :
  MaybeTask α → α

Std.Async.MaybeTask.map {α β : Type} (f : α → β)
  (prio : Task.Priority := Task.Priority.default)
  (sync : Bool := false) : MaybeTask α → MaybeTask β
Std.Async.MaybeTask.map {α β : Type}
  (f : α → β)
  (prio : Task.Priority :=
    Task.Priority.default)
  (sync : Bool := false) :
  MaybeTask α → MaybeTask β

Std.Async.MaybeTask.joinTask {α : Type} (t : Task (MaybeTask α)) :
  Task α
Std.Async.MaybeTask.joinTask {α : Type}
  (t : Task (MaybeTask α)) : Task α

21.12.1.4. Conversions🔗

An existing Task, IO.Promise, or Except value can be converted into an Async computation. These conversions make it possible to call code that produces a Task or IO.Promise, such as a wrapper around a callback-based API or a hand-written asynchronous primitive, directly from within an Async program. The corresponding conversions from Task and Except are also available for EAsync and BaseAsync; the conversions from IO.Promise are specific to Async because a dropped promise is reported as an IO.Error.

An IO.Promise can be dropped before it is ever resolved, for example if the code that was expected to resolve it is canceled or abandoned and the last reference to the promise goes away. After that, the promise can never be resolved. Because reference counts are deterministic, the runtime detects this the moment it happens, rather than at some unpredictable later time. Async.ofPromise and Async.ofPurePromise detect a dropped promise and produce an Async error rather than panicking; the message can be supplied via their error parameter, and defaults to the promise linked to the Async was dropped.

Std.Async.Async.ofTask {α : Type} (task : Task α) : Async α
Std.Async.Async.ofTask {α : Type}
  (task : Task α) : Async α

Std.Async.EAsync.ofTask {ε α : Type} (x : ETask ε α) : EAsync ε α
Std.Async.EAsync.ofTask {ε α : Type}
  (x : ETask ε α) : EAsync ε α

Std.Async.EAsync.ofETask {ε α : Type} (x : ETask ε α) : EAsync ε α
Std.Async.EAsync.ofETask {ε α : Type}
  (x : ETask ε α) : EAsync ε α

Std.Async.BaseAsync.ofTask {α : Type} (x : Task α) : BaseAsync α
Std.Async.BaseAsync.ofTask {α : Type}
  (x : Task α) : BaseAsync α

Std.Async.Async.ofIOTask {α : Type} (task : IO (Task α)) : Async α
Std.Async.Async.ofIOTask {α : Type}
  (task : IO (Task α)) : Async α

Std.Async.Async.ofAsyncTask {α : Type} (task : AsyncTask α) : Async α
Std.Async.Async.ofAsyncTask {α : Type}
  (task : AsyncTask α) : Async α

Std.Async.Async.ofPromise {α : Type}
  (task : IO (IO.Promise (Except IO.Error α)))
  (error : String := "the promise linked to the Async was dropped") :
  Async α
Std.Async.Async.ofPromise {α : Type}
  (task :
    IO (IO.Promise (Except IO.Error α)))
  (error : String :=
    "the promise linked to the Async was dropped") :
  Async α

Std.Async.Async.ofPurePromise {α : Type} (task : IO (IO.Promise α))
  (error : String := "the promise linked to the Async was dropped") :
  Async α
Std.Async.Async.ofPurePromise {α : Type}
  (task : IO (IO.Promise α))
  (error : String :=
    "the promise linked to the Async was dropped") :
  Async α

ETask.ofPromise! converts a promise to a task directly, panicking if the promise is dropped rather than producing an error.

Std.Async.ETask.ofPromise! {ε α : Type} (x : IO.Promise (Except ε α)) :
  ETask ε α
Std.Async.ETask.ofPromise! {ε α : Type}
  (x : IO.Promise (Except ε α)) :
  ETask ε α

Std.Async.Async.ofExcept {α : Type} (except : Except IO.Error α) :
  Async α
Std.Async.Async.ofExcept {α : Type}
  (except : Except IO.Error α) : Async α

Std.Async.EAsync.ofExcept {ε α : Type} (except : Except ε α) :
  EAsync ε α
Std.Async.EAsync.ofExcept {ε α : Type}
  (except : Except ε α) : EAsync ε α

Std.Async.BaseAsync.ofExcept {α : Type} (except : Except Empty α) :
  BaseAsync α
Std.Async.BaseAsync.ofExcept {α : Type}
  (except : Except Empty α) : BaseAsync α

21.12.3.1. Selection Protocol🔗

Event selection begins by randomizing the order of the selectables. It consults each selector's non-blocking poll Selector.tryFn until one of them returns some. This is the winning selectable; its code is invoked and no further work is needed. On this fast path, only one selector is ever consumed, so there is no risk of data loss or double delivery.

If no selector was resolved in the first iteration (that is, each tryFn returned none), then it is necessary to wait until one of the selectors is resolved. Waiting consists of first registering a waiter with each selector; the first selector that has data wins the race via the waiters. The winning selector consumes its event, invokes code to clean up the other waiting selectors, computes the selectable's value, and resolves an overall promise that Selectable.one is blocked on.

More specifically, this is done by creating an atomic flag (indicating that a winner has been selected) and a promise for the result of Selectable.one. A registration loop processes each selectable in the array:

1. The system checks whether the flag is now set, indicating that a prior selector has won the race. If so, the loop terminates.

2. A waiter is registered with the selector using Selector.registerFn. This registration process may not consume data; it merely registers interest in data should it become available. The waiter includes a reference to the atomic flag along with a promise that can be resolved with the selector's data. The selector must call race on the waiter when the event has occurred, but it may only consume data if it wins the race.

3. A task is created that observes the waiter's promise. When the promise is resolved, indicating that it has won the race, this completion callback is invoked with none if the promise was dropped (e.g. due to cancellation or unregistering); in this case, it should do nothing. If it is invoked with some around the result, then it must run an Async computation that: a. propagates any error indicated by the data source's result, b. blocks until the entire registration loop is complete, c. unregisters the waiter from every selectable in the array using its Selector.unregisterFn, and d. runs the winning selectable's code, resolving the result promise.

When the registration loop is complete, an internal promise is resolved that unblocks the winning waiter's callback. This block ensures that all registration occurs before all cleanup.

Finally, Selectable.one awaits the overall result promise, which will be resolved as soon as there is a winning callback.

Std.Async.Waiter (α : Type) : Type
Std.Async.Waiter (α : Type) : Type

promise : IO.Promise (Except IO.Error α)

Std.Async.Waiter.race {m : Type → Type} {α β : Type} [Monad m]
  [MonadLiftT (ST IO.RealWorld) m] (w : Waiter α) (lose : m β)
  (win : IO.Promise (Except IO.Error α) → m β) : m β
Std.Async.Waiter.race {m : Type → Type}
  {α β : Type} [Monad m]
  [MonadLiftT (ST IO.RealWorld) m]
  (w : Waiter α) (lose : m β)
  (win :
    IO.Promise (Except IO.Error α) →
      m β) :
  m β

Std.Async.Waiter.withPromise {α β : Type} (w : Waiter α)
  (p : IO.Promise (Except IO.Error β)) : Waiter β
Std.Async.Waiter.withPromise {α β : Type}
  (w : Waiter α)
  (p : IO.Promise (Except IO.Error β)) :
  Waiter β