def Std.Internal.IO.Async.AsyncTask (α : Type u) : Type u

A Task that may resolve to a value or an IO.Error.

Equations

• Std.Internal.IO.Async.AsyncTask α = Task (Except IO.Error α)

Instances For

• Std.Internal.IO.Async.AsyncTask.instPure

@[inline]

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

Construct an AsyncTask that is already resolved with value x.

Equations

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

instance Std.Internal.IO.Async.AsyncTask.instPure : Pure AsyncTask

Equations

• Std.Internal.IO.Async.AsyncTask.instPure = { pure := fun {α : Type ?u.5} => Std.Internal.IO.Async.AsyncTask.pure }

@[inline]

def Std.Internal.IO.Async.AsyncTask.bind {α : Type u_1} {β : Type u_2} (x : AsyncTask α) (f : α → AsyncTask β) : AsyncTask β

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 = Task.bind x fun (r : Except IO.Error α) => match r with | Except.ok a => f a | Except.error e => { get := Except.error e }

@[inline]

def Std.Internal.IO.Async.AsyncTask.map {α : Type u_1} {β : Type u_2} (f : α → β) (x : AsyncTask α) : AsyncTask β

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

• errors, return an AsyncTask that reolves to the error.
• succeeds, return an AsyncTask that resolves to f x.

Equations

• Std.Internal.IO.Async.AsyncTask.map f x = Task.map (fun (r : Except IO.Error α) => match r with | Except.ok a => Except.ok (f a) | Except.error e => Except.error e) x

@[inline]

def Std.Internal.IO.Async.AsyncTask.bindIO {α : Type u_1} {β : Type} (x : AsyncTask α) (f : α → IO (AsyncTask β)) : 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 = IO.bindTask x fun (r : Except IO.Error α) => match r with | Except.ok a => f a | Except.error e => EStateM.Result.error e

@[inline]

def Std.Internal.IO.Async.AsyncTask.mapIO {α : Type u_1} {β : Type} (f : α → IO β) (x : AsyncTask α) : 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

• Std.Internal.IO.Async.AsyncTask.mapIO f x = IO.mapTask (fun (r : Except IO.Error α) => match r with | Except.ok a => f a | Except.error e => EStateM.Result.error e) x

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 α)) : AsyncTask α

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 α) : AsyncTask α

Create an AsyncTask that resolves to the value of x.

Equations

• Std.Internal.IO.Async.AsyncTask.ofPurePromise x = Task.map pure x.result

@[inline]

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

Obtain the IO.TaskState of x.

Equations

• x.getState = IO.getTaskState x