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.
Concrete Task Types: Concrete units of work that can be executed within these contexts.

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.

BaseAsync: A monadic type for infallible asynchronous computations
EAsync: A monadic type for asynchronous computations that may fail with an error of type ε
Async: A monadic type for IO-based asynchronous computations that may fail with IO.Error (alias for EAsync IO.Error)

Concurrent Units of Work #

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

Task: A computation that will resolve to a value of type α,
ETask: A task that may fail with an error of type ε.
AsyncTask: A task that may fail with an IO.Error (alias for ETask IO.Error).

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 : Type → Type) 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 (α → β) → (Unit → m α) → m β
seqLeft {α β : Type} : m α → (Unit → m β) → m α
seqRight {α β : Type} : m α → (Unit → m β) → 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 : Type → Type) extends Monad m :

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

map {α β : Type} : (α → β) → m α → m β
mapConst {α β : Type} : α → m β → m α
pure {α : Type} : α → m α
seq {α β : Type} : m (α → β) → (Unit → m α) → m β
seqLeft {α β : Type} : m α → (Unit → m β) → m α
seqRight {α β : Type} : m α → (Unit → m β) → m β
bind {α β : Type} : m α → (α → m β) → m β
async {α : Type} (x : m α) (prio : Task.Priority := Task.Priority.default) : m (t α)
Starts an asynchronous computation in another monad.

Instances

@[defaultInstance 1000]

instance Std.Internal.IO.Async.instMonadAwaitStateTOfMonad {m t : Type → Type} {n : Type} [Monad m] [MonadAwait t m] :

MonadAwait t (StateT n m)

Equations

Std.Internal.IO.Async.instMonadAwaitStateTOfMonad = { toMonad := StateT.instMonad, await := fun {α : Type} => liftM ∘ Std.Internal.IO.Async.await }

@[defaultInstance 1000]

instance Std.Internal.IO.Async.instMonadAwaitExceptTOfMonad {m t : Type → Type} {n : Type} [Monad m] [MonadAwait t m] :

MonadAwait t (ExceptT n m)

Equations

Std.Internal.IO.Async.instMonadAwaitExceptTOfMonad = { toMonad := ExceptT.instMonad, await := fun {α : Type} => liftM ∘ Std.Internal.IO.Async.await }

@[defaultInstance 1000]

instance Std.Internal.IO.Async.instMonadAwaitReaderTOfMonad {m t : Type → Type} {n : Type} [Monad m] [MonadAwait t m] :

MonadAwait t (ReaderT n m)

Equations

Std.Internal.IO.Async.instMonadAwaitReaderTOfMonad = { toMonad := ReaderT.instMonad, await := fun {α : Type} => liftM ∘ Std.Internal.IO.Async.await }

@[defaultInstance 1000]

instance Std.Internal.IO.Async.instMonadAwaitStateRefT' {t m : Type → Type} {s n : Type} [MonadAwait t m] :

MonadAwait t (StateRefT' s n m)

Equations

Std.Internal.IO.Async.instMonadAwaitStateRefT' = { toMonad := StateRefT'.instMonad, await := fun {α : Type} => liftM ∘ Std.Internal.IO.Async.await }

@[defaultInstance 1000]

instance Std.Internal.IO.Async.instMonadAwaitStateT {t m : Type → Type} {s : Type} [MonadAwait t m] :

MonadAwait t (StateT s m)

Equations

Std.Internal.IO.Async.instMonadAwaitStateT = { toMonad := StateT.instMonad, await := fun {α : Type} => liftM ∘ Std.Internal.IO.Async.await }

@[defaultInstance 1000]

instance Std.Internal.IO.Async.instMonadAsyncReaderT {t m : Type → Type} {n : Type} [MonadAsync t m] :

MonadAsync t (ReaderT n m)

Equations

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

@[defaultInstance 1000]

instance Std.Internal.IO.Async.instMonadAsyncStateRefT' {t m : Type → Type} {s n : Type} [MonadAsync t m] :

MonadAsync t (StateRefT' s n m)

Equations

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

@[defaultInstance 1000]

instance Std.Internal.IO.Async.instMonadAsyncStateTOfFunctor {t m : Type → Type} {s : Type} [Functor t] [inst : MonadAsync t m] :

MonadAsync t (StateT s m)

Equations

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

@[reducible, inline]

abbrev Std.Internal.IO.Async.ETask (ε α : Type) :

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

Equations

Std.Internal.IO.Async.ETask ε α = ExceptT ε Task α

Instances For

@[inline]

def Std.Internal.IO.Async.ETask.pure {α ε : Type} (x : α) :

ETask ε α

Construct an ETask that is already resolved with value x.

Equations

Std.Internal.IO.Async.ETask.pure x = { get := Except.ok x }

@[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

Std.Internal.IO.Async.ETask.map f x prio sync = Task.map (fun (x : Except ε α) => f <$> x) x prio sync

@[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

x.bind f prio sync = Task.bind x (fun (x : Except ε α) => match x with | Except.ok a => f a | Except.error e => { get := Except.error e }) prio sync

@[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.

@[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.

@[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

x.block = match x.get with | Except.ok a => pure a | Except.error e => EStateM.Result.error e

@[inline]

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

ETask ε α

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

Equations

Std.Internal.IO.Async.ETask.ofPromise x = x.result!

@[inline]

def Std.Internal.IO.Async.ETask.ofPurePromise {α ε : Type} (x : IO.Promise α) :

ETask ε α

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

Equations

Std.Internal.IO.Async.ETask.ofPurePromise x = Task.map pure x.result! Task.Priority.default true

@[inline]

def Std.Internal.IO.Async.ETask.getState {ε α : Type} (x : ETask ε α) :

BaseIO IO.TaskState

Obtain the IO.TaskState of x.

Equations

x.getState = IO.getTaskState x

instance Std.Internal.IO.Async.ETask.instFunctor {ε : Type} :

Functor (ETask ε)

Equations

Std.Internal.IO.Async.ETask.instFunctor = { map := fun {α β : Type} (f : α → β) (x : Std.Internal.IO.Async.ETask ε α) => Std.Internal.IO.Async.ETask.map f x }

instance Std.Internal.IO.Async.ETask.instMonad {ε : Type} :

Monad (ETask ε)

Equations

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

@[reducible, inline]

abbrev Std.Internal.IO.Async.AsyncTask (α : Type) :

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

Equations

Std.Internal.IO.Async.AsyncTask = Std.Internal.IO.Async.ETask IO.Error

Instances For

@[inline]

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

BaseIO (AsyncTask β)

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.

@[inline]

def Std.Internal.IO.Async.AsyncTask.pure {α : Type} (x : α) :

Construct an AsyncTask that is already resolved with value x.

Equations

Std.Internal.IO.Async.AsyncTask.pure x = { get := Except.ok x }

@[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

x.bind f prio sync = Task.bind x (fun (x : Except IO.Error α) => match x with | Except.ok a => f a | Except.error e => { get := Except.error e }) prio sync

@[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

Std.Internal.IO.Async.AsyncTask.map f x prio sync = Task.map (fun (x : Except IO.Error α) => f <$> x) x prio sync

@[inline]

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

BaseIO (AsyncTask β)

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

Equations

x.bindIO f prio sync = IO.bindTask x (fun (x : Except IO.Error α) => match x with | Except.ok a => f a | Except.error e => EStateM.Result.error e) prio sync

@[inline]

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

BaseIO (AsyncTask β)

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.

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

IO α

Block until the AsyncTask in x finishes.

Equations

x.block = match x.get with | Except.ok a => pure a | Except.error e => EStateM.Result.error e

@[inline]

def Std.Internal.IO.Async.AsyncTask.ofPromise {α : Type} (x : IO.Promise (Except IO.Error α)) :

Create an AsyncTask that resolves to the value of x.

Equations

Std.Internal.IO.Async.AsyncTask.ofPromise x = x.result!

@[inline]

def Std.Internal.IO.Async.AsyncTask.ofPurePromise {α : Type} (x : IO.Promise α) :

Create an AsyncTask that resolves to the value of x.

Equations

Std.Internal.IO.Async.AsyncTask.ofPurePromise x = Task.map pure x.result! Task.Priority.default true

@[inline]

def Std.Internal.IO.Async.AsyncTask.getState {α : Type} (x : AsyncTask α) :

BaseIO IO.TaskState

Obtain the IO.TaskState of x.

Equations

x.getState = IO.getTaskState x

inductive Std.Internal.IO.Async.MaybeTask (α : Type) :

A MaybeTask α represents a computation that either:

Is immediately available as an α value, or
Is an asynchronous computation that will eventually produce an α value.

pure {α : Type} : α → MaybeTask α
ofTask {α : Type} : Task α → MaybeTask α

Instances For

@[inline]

def Std.Internal.IO.Async.MaybeTask.toTask {α : Type} :

MaybeTask α → Task α

Constructs an Task from a MaybeTask.

Equations

(Std.Internal.IO.Async.MaybeTask.pure a).toTask = { get := a }
(Std.Internal.IO.Async.MaybeTask.ofTask t).toTask = t

@[inline]

def Std.Internal.IO.Async.MaybeTask.get {α : Type} :

MaybeTask α → α

Gets the value of the MaybeTask by blocking.

Equations

(Std.Internal.IO.Async.MaybeTask.pure a).get = a
(Std.Internal.IO.Async.MaybeTask.ofTask t).get = t.get

@[inline]

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

MaybeTask α → MaybeTask β

Maps a function over a MaybeTask.

Equations

Std.Internal.IO.Async.MaybeTask.map f prio sync (Std.Internal.IO.Async.MaybeTask.pure a) = Std.Internal.IO.Async.MaybeTask.pure (f a)
Std.Internal.IO.Async.MaybeTask.map f prio sync (Std.Internal.IO.Async.MaybeTask.ofTask t) = Std.Internal.IO.Async.MaybeTask.ofTask (Task.map f t prio sync)

@[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

(Std.Internal.IO.Async.MaybeTask.pure a).bind f prio sync = f a
(Std.Internal.IO.Async.MaybeTask.ofTask t_1).bind f prio sync = Std.Internal.IO.Async.MaybeTask.ofTask (t_1.bind (fun (x : α) => (f x).toTask) prio sync)

@[inline]

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

Join the MaybeTask to an Task.

Equations

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

instance Std.Internal.IO.Async.MaybeTask.instFunctor :

Functor MaybeTask

Equations

Std.Internal.IO.Async.MaybeTask.instFunctor = { map := fun {α β : Type} (f : α → β) => Std.Internal.IO.Async.MaybeTask.map f }

instance Std.Internal.IO.Async.MaybeTask.instMonad :

Monad MaybeTask

Equations

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

def Std.Internal.IO.Async.BaseAsync (α : Type) :

An asynchronous computation that never fails.

Equations

Std.Internal.IO.Async.BaseAsync α = BaseIO (Std.Internal.IO.Async.MaybeTask α)

Instances For

@[inline]

def Std.Internal.IO.Async.BaseAsync.mk {α : Type} (x : BaseIO (MaybeTask α)) :

Converts a BaseIO into a BaseAsync

Equations

Std.Internal.IO.Async.BaseAsync.mk x = x

@[inline]

def Std.Internal.IO.Async.BaseAsync.toRawBaseIO {α : Type} (x : BaseAsync α) :

BaseIO (MaybeTask α)

Converts a BaseAsync into a BaseIO

Equations

x.toRawBaseIO = x

@[inline]

def Std.Internal.IO.Async.BaseAsync.toBaseIO {α : Type} (x : BaseAsync α) :

BaseIO (Task α)

Converts a BaseAsync to a BaseIO Task.

Equations

x.toBaseIO = Std.Internal.IO.Async.MaybeTask.toTask <$> x.toRawBaseIO

@[inline]

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

Creates a new BaseAsync out of a Task.

Equations

Std.Internal.IO.Async.BaseAsync.ofTask x = Std.Internal.IO.Async.BaseAsync.mk (pure (Std.Internal.IO.Async.MaybeTask.ofTask x))

@[inline]

def Std.Internal.IO.Async.BaseAsync.pure {α : Type} (a : α) :

Creates a BaseAsync computation that immediately returns the given value.

Equations

Std.Internal.IO.Async.BaseAsync.pure a = Std.Internal.IO.Async.BaseAsync.mk (pure (Std.Internal.IO.Async.MaybeTask.pure a))

@[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.

@[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

self.bind f prio sync = Std.Internal.IO.Async.BaseAsync.mk do let x ← self.toRawBaseIO (Std.Internal.IO.Async.BaseAsync.bind.bindAsyncTask prio sync x f).toRawBaseIO

def Std.Internal.IO.Async.BaseAsync.bind.bindAsyncTask {α β : Type} (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) (t : MaybeTask α) (f : α → BaseAsync β) :

Equations

One or more equations did not get rendered due to their size.
Std.Internal.IO.Async.BaseAsync.bind.bindAsyncTask prio sync (Std.Internal.IO.Async.MaybeTask.pure a) f = Std.Internal.IO.Async.BaseAsync.mk (f a).toRawBaseIO

@[inline]

def Std.Internal.IO.Async.BaseAsync.lift {α : Type} (x : BaseIO α) :

Lifts a BaseIO action into a BaseAsync computation.

Equations

Std.Internal.IO.Async.BaseAsync.lift x = Std.Internal.IO.Async.BaseAsync.mk (EStateM.pure ∘ Std.Internal.IO.Async.MaybeTask.pure =<< x)

@[inline]

def Std.Internal.IO.Async.BaseAsync.wait {α : Type} (self : BaseAsync α) :

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

Equations

self.wait = pure ∘ Task.get =<< self.toBaseIO

@[inline]

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

BaseIO (Task α)

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

Equations

x.asTask prio = do let res ← x.toRawBaseIO.asTask prio pure (Std.Internal.IO.Async.MaybeTask.joinTask res)

@[inline]

def Std.Internal.IO.Async.BaseAsync.await {α : Type} (t : Task α) :

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

Equations

Std.Internal.IO.Async.BaseAsync.await t = Std.Internal.IO.Async.BaseAsync.mk (pure (Std.Internal.IO.Async.MaybeTask.ofTask t))

@[inline]

def Std.Internal.IO.Async.BaseAsync.async {α : Type} (self : BaseAsync α) (prio : Task.Priority := Task.Priority.default) :

BaseAsync (Task α)

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

Equations

self.async prio = Std.Internal.IO.Async.BaseAsync.lift (self.asTask prio)

instance Std.Internal.IO.Async.BaseAsync.instFunctor :

Functor BaseAsync

Equations

Std.Internal.IO.Async.BaseAsync.instFunctor = { map := fun {α β : Type} (f : α → β) (self : Std.Internal.IO.Async.BaseAsync α) => Std.Internal.IO.Async.BaseAsync.map f self }

instance Std.Internal.IO.Async.BaseAsync.instMonad :

Monad BaseAsync

Equations

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

instance Std.Internal.IO.Async.BaseAsync.instMonadLiftBaseIO :

MonadLift BaseIO BaseAsync

Equations

Std.Internal.IO.Async.BaseAsync.instMonadLiftBaseIO = { monadLift := fun {α : Type} => Std.Internal.IO.Async.BaseAsync.lift }

instance Std.Internal.IO.Async.BaseAsync.instMonadAwaitTask :

MonadAwait Task BaseAsync

Equations

Std.Internal.IO.Async.BaseAsync.instMonadAwaitTask = { toMonad := Std.Internal.IO.Async.BaseAsync.instMonad, await := fun {α : Type} => Std.Internal.IO.Async.BaseAsync.await }

instance Std.Internal.IO.Async.BaseAsync.instMonadAsyncTask :

MonadAsync Task BaseAsync

Equations

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

instance Std.Internal.IO.Async.BaseAsync.instInhabited {α : Type} [Inhabited α] :

Inhabited (BaseAsync α)

Equations

Std.Internal.IO.Async.BaseAsync.instInhabited = { default := Std.Internal.IO.Async.BaseAsync.mk (pure (Std.Internal.IO.Async.MaybeTask.pure default)) }

def Std.Internal.IO.Async.EAsync (ε α : Type) :

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

Equations

Std.Internal.IO.Async.EAsync ε α = Std.Internal.IO.Async.BaseAsync (Except ε α)

Instances For

@[inline]

def Std.Internal.IO.Async.EAsync.toBaseIO {ε α : Type} (x : EAsync ε α) :

BaseIO (ETask ε α)

Converts a EAsync to a ETask.

Equations

x.toBaseIO = Std.Internal.IO.Async.MaybeTask.toTask <$> Std.Internal.IO.Async.BaseAsync.toRawBaseIO x

@[inline]

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

EAsync ε α

Creates a new EAsync out of a RTask.

Equations

Std.Internal.IO.Async.EAsync.ofTask x = Std.Internal.IO.Async.BaseAsync.mk (pure (Std.Internal.IO.Async.MaybeTask.ofTask x))

@[inline]

def Std.Internal.IO.Async.EAsync.toEIO {ε α : Type} (x : EAsync ε α) :

EIO ε (ETask ε α)

Converts a BaseAsync to a EIO ETask.

Equations

x.toEIO = Std.Internal.IO.Async.MaybeTask.toTask <$> liftM (Std.Internal.IO.Async.BaseAsync.toRawBaseIO x)

@[inline]

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

EAsync ε α

Creates a new EAsync out of a ETask.

Equations

Std.Internal.IO.Async.EAsync.ofETask x = Std.Internal.IO.Async.BaseAsync.mk (Std.Internal.IO.Async.BaseAsync.ofTask x)

@[inline]

def Std.Internal.IO.Async.EAsync.pure {α ε : Type} (a : α) :

EAsync ε α

Creates an EAsync computation that immediately returns the given value.

Equations

Std.Internal.IO.Async.EAsync.pure a = Std.Internal.IO.Async.BaseAsync.mk (Std.Internal.IO.Async.BaseAsync.pure (Except.ok a))

@[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

Std.Internal.IO.Async.EAsync.map f self = Std.Internal.IO.Async.BaseAsync.mk (Std.Internal.IO.Async.BaseAsync.map (Except.map f) self)

@[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.

@[inline]

def Std.Internal.IO.Async.EAsync.lift {ε α : Type} (x : EIO ε α) :

EAsync ε α

Lifts an EIO action into an EAsync computation.

Equations

Std.Internal.IO.Async.EAsync.lift x = Std.Internal.IO.Async.BaseAsync.mk (Std.Internal.IO.Async.BaseAsync.lift x.toBaseIO)

@[inline]

def Std.Internal.IO.Async.EAsync.wait {ε α : Type} (self : EAsync ε α) :

EIO ε α

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

Equations

self.wait = do let result ← liftM (Std.Internal.IO.Async.BaseAsync.wait self) match result with | Except.ok a => pure a | Except.error e => EStateM.Result.error e

@[inline]

def Std.Internal.IO.Async.EAsync.asTask {ε α : Type} (x : EAsync ε α) (prio : Task.Priority := Task.Priority.default) :

EIO ε (ETask ε α)

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

Equations

x.asTask prio = liftM (Std.Internal.IO.Async.BaseAsync.asTask x prio)

@[inline]

def Std.Internal.IO.Async.EAsync.throw {ε α : Type} (e : ε) :

EAsync ε α

Raises an error of type ε within the EAsync monad.

Equations

Std.Internal.IO.Async.EAsync.throw e = Std.Internal.IO.Async.BaseAsync.mk (Std.Internal.IO.Async.BaseAsync.pure (Except.error e))

@[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.

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.

@[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

Std.Internal.IO.Async.EAsync.await x = Std.Internal.IO.Async.BaseAsync.mk (Std.Internal.IO.Async.BaseAsync.ofTask x)

@[inline]

def Std.Internal.IO.Async.EAsync.async {ε α : Type} (self : EAsync ε α) (prio : Task.Priority := Task.Priority.default) :

EAsync ε (ETask ε α)

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

Equations

self.async prio = Std.Internal.IO.Async.EAsync.lift (self.asTask prio)

instance Std.Internal.IO.Async.EAsync.instFunctor {ε : Type} :

Functor (EAsync ε)

Equations

Std.Internal.IO.Async.EAsync.instFunctor = { map := fun {α β : Type} => Std.Internal.IO.Async.EAsync.map }

instance Std.Internal.IO.Async.EAsync.instMonad {ε : Type} :

Monad (EAsync ε)

Equations

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

instance Std.Internal.IO.Async.EAsync.instMonadLiftEIO {ε : Type} :

MonadLift (EIO ε) (EAsync ε)

Equations

Std.Internal.IO.Async.EAsync.instMonadLiftEIO = { monadLift := fun {α : Type} => Std.Internal.IO.Async.EAsync.lift }

instance Std.Internal.IO.Async.EAsync.instMonadExcept {ε : Type} :

MonadExcept ε (EAsync ε)

Equations

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

instance Std.Internal.IO.Async.EAsync.instMonadExceptOf {ε : Type} :

MonadExceptOf ε (EAsync ε)

Equations

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

instance Std.Internal.IO.Async.EAsync.instMonadFinally {ε : Type} :

MonadFinally (EAsync ε)

Equations

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

instance Std.Internal.IO.Async.EAsync.instOrElse {ε α : Type} :

OrElse (EAsync ε α)

Equations

Std.Internal.IO.Async.EAsync.instOrElse = { orElse := MonadExcept.orElse }

instance Std.Internal.IO.Async.EAsync.instInhabited {ε α : Type} [Inhabited ε] :

Inhabited (EAsync ε α)

Equations

Std.Internal.IO.Async.EAsync.instInhabited = { default := Std.Internal.IO.Async.BaseAsync.mk (Std.Internal.IO.Async.BaseAsync.pure default) }

instance Std.Internal.IO.Async.EAsync.instMonadAwaitETask {ε : Type} :

MonadAwait (ETask ε) (EAsync ε)

Equations

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

instance Std.Internal.IO.Async.EAsync.instMonadAwaitTask {ε : Type} :

MonadAwait Task (EAsync ε)

Equations

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

instance Std.Internal.IO.Async.EAsync.instMonadAwaitAsyncTaskError :

MonadAwait AsyncTask (EAsync IO.Error)

Equations

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

instance Std.Internal.IO.Async.EAsync.instMonadAwaitPromise {ε : Type} :

MonadAwait IO.Promise (EAsync ε)

Equations

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

instance Std.Internal.IO.Async.EAsync.instMonadAsyncETask {ε : Type} :

MonadAsync (ETask ε) (EAsync ε)

Equations

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

instance Std.Internal.IO.Async.EAsync.instMonadAsyncAsyncTaskError :

MonadAsync AsyncTask (EAsync IO.Error)

Equations

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

instance Std.Internal.IO.Async.EAsync.instMonadLiftBaseIO {ε : Type} :

MonadLift BaseIO (EAsync ε)

Equations

Std.Internal.IO.Async.EAsync.instMonadLiftBaseIO = { monadLift := fun {α : Type} (x : BaseIO α) => Std.Internal.IO.Async.BaseAsync.mk ((pure ∘ Except.ok) <$> x) }

instance Std.Internal.IO.Async.EAsync.instMonadLiftEIO_1 {ε : Type} :

MonadLift (EIO ε) (EAsync ε)

Equations

Std.Internal.IO.Async.EAsync.instMonadLiftEIO_1 = { monadLift := fun {α : Type} (x : EIO ε α) => Std.Internal.IO.Async.BaseAsync.mk (pure <$> x.toBaseIO) }

instance Std.Internal.IO.Async.EAsync.instMonadLiftBaseAsync {ε : Type} :

MonadLift BaseAsync (EAsync ε)

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.

@[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)

instance Std.Internal.IO.Async.EAsync.instForInLoopUnitOfInhabited {ε : Type} [Inhabited ε] :

ForIn (EAsync ε) Lean.Loop Unit

Equations

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

@[reducible, inline]

abbrev Std.Internal.IO.Async.Async (α : Type) :

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

Equations

Std.Internal.IO.Async.Async α = Std.Internal.IO.Async.EAsync IO.Error α

Instances For

@[inline]

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

IO (AsyncTask α)

Converts a Async to a AsyncTask.

Equations

x.toIO = Std.Internal.IO.Async.MaybeTask.toTask <$> liftM (Std.Internal.IO.Async.BaseAsync.toRawBaseIO x)

@[defaultInstance 1000]

instance Std.Internal.IO.Async.Async.instMonadAsyncAsyncTask :

MonadAsync AsyncTask Async

Equations

Std.Internal.IO.Async.Async.instMonadAsyncAsyncTask = inferInstanceAs (Std.Internal.IO.Async.MonadAsync (Std.Internal.IO.Async.ETask IO.Error) (Std.Internal.IO.Async.EAsync IO.Error))

instance Std.Internal.IO.Async.Async.instMonadAwaitAsyncTask :

MonadAwait AsyncTask Async

Equations

Std.Internal.IO.Async.Async.instMonadAwaitAsyncTask = inferInstanceAs (Std.Internal.IO.Async.MonadAwait Std.Internal.IO.Async.AsyncTask (Std.Internal.IO.Async.EAsync IO.Error))

instance Std.Internal.IO.Async.Async.instMonadAwaitPromise :

MonadAwait IO.Promise Async

Equations

Std.Internal.IO.Async.Async.instMonadAwaitPromise = inferInstanceAs (Std.Internal.IO.Async.MonadAwait IO.Promise (Std.Internal.IO.Async.EAsync IO.Error))

@[inline, specialize #[]]

def Std.Internal.IO.Async.background {m t : Type → Type} {α : 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

Std.Internal.IO.Async.background prio = discard ∘ fun (x : m α) => Std.Internal.IO.Async.async x prio

@[inline, specialize #[]]

def Std.Internal.IO.Async.concurrently {m t : Type → Type} {α β : 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.

@[inline, specialize #[]]

def Std.Internal.IO.Async.race {m t : Type → Type} {α : 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.

@[inline, specialize #[]]

def Std.Internal.IO.Async.concurrentlyAll {m t : Type → Type} {α : 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

Std.Internal.IO.Async.concurrentlyAll xs prio = do let tasks ← Array.mapM (fun (x : m α) => Std.Internal.IO.Async.async x prio) xs Array.mapM Std.Internal.IO.Async.await tasks

@[inline, specialize #[]]

def Std.Internal.IO.Async.raceAll {m : Type → Type} {c : Type u_1} {α : Type} {t : Type → Type} [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.