IO.Async.Util

Definitions

0 Handler : Type -> Type -> Type -> Type

Totality: total
Visibility: public export

injectIO : Has x es => IO (Either x a) -> Async e es a

  Inject an `IO (Either e a)` computation into an `Async` monad dealing
  with several possible errors.

Totality: total
Visibility: export

embed : Lazy (Async e es a) -> Outcome es a -> Async e es a

Totality: total
Visibility: export

join : Fiber es a -> Async e fs (Outcome es a)

  Semantically blocks the current fiber until the given fiber
  produces and outcome, and returns the outcome produced.

Totality: total
Visibility: export

wait : Fiber es a -> Async e fs ()

  Awaits the termination of a fiber ignoring its outcome.

Totality: total
Visibility: export

cancel : Fiber es a -> Async e fs ()

  Cancels the given fiber.
  
  This will semantically block the current fiber, until the target has
  completed.

Totality: total
Visibility: export

primAsync_ : ((Result es a -> IO1 ()) -> IO1 ()) -> Async e es a

  Like `primAsync` but does not provide a hook for canceling.

Totality: total
Visibility: export

never : Async e es a

  A (cancelable) asynchronous computation that will never produce a
  result

Totality: total
Visibility: export

awaitOnce : Once World a -> Async e es a

  Awaits the completion of a `Once a`.

Totality: total
Visibility: export

await : Deferred World a -> Async e es a

  Awaits the completion of a `Deferred a`.

Totality: total
Visibility: export

racePair : Async e es a -> Async e fs b -> Async e gs (Either (Outcome es a, Fiber fs b) (Fiber es a, Outcome fs b))

  A low-level primitive for racing the evaluation of two fibers that returns the [[Outcome]]
  of the winner and the [[Fiber]] of the loser. The winner of the race is considered to be
  the first fiber that completes with an outcome.
  
  `racePair` is a cancelation-unsafe function; it is recommended to use the safer variants.

Totality: total
Visibility: export

joinWith : Fiber es a -> Lazy (Async e es a) -> Async e es a

  Awaits the completion of the bound fiber and returns its result once it completes.
  
  If the fiber completes with [[Outcome.Succeeded]], the successful value is returned. If the
  fiber completes with [[Outcome.Errored]], the error is raised. If the fiber completes with
  [[Outcome.Canceled]], `onCancel` is run.

Totality: total
Visibility: export

joinWithNeutral : Monoid a => Fiber es a -> Async e es a

  Like `joinWith`, returning the `neutral` value of the `Monoid` in case of
  cancelation.

Totality: total
Visibility: export

cancelable : Async e es a -> Async e [] () -> Async e es (Maybe a)

Totality: total
Visibility: export

raceOutcome : Async e es a -> Async e fs b -> Async e gs (Either (Outcome es a) (Outcome fs b))

  Races the evaluation of two fibers that returns the [[Outcome]] of the winner. The winner
  of the race is considered to be the first fiber that completes with an outcome. The loser
  of the race is canceled before returning.
  
  @param fa
    the effect for the first racing fiber
  @param fb
    the effect for the second racing fiber
  
  @see
    [[race]] for a simpler variant that returns the successful outcome.

Totality: total
Visibility: export

race2 : Async e es a -> Async e es b -> (a -> c) -> (b -> c) -> Lazy c -> Async e es c

  Races the evaluation of several fibers, returning the result
  of the winnner. The other fibers are canceled as soon as one of the
  fibers produced an outcome.
  case of cancelation.
  
  The semantics of [[race]] are described by the following rules:
  
    1. If the winner completes with [[Outcome.Succeeded]], the race returns the successful
       value. The loser is canceled before returning.
    2. If the winner completes with [[Outcome.Errored]], the race raises the error.
       The loser is canceled before returning.
    3. If the winner completes with [[Outcome.Canceled]], the race cancels
       the loser and returns its result, fires an error, or returns `Nothing`
       its outcome is `Canceled`.
  
  @param fa
    the effect for the first racing fiber
  @param fb
    the effect for the second racing fiber
  
  @see
    [[raceOutcome]] for a variant that returns the outcome of the winner.

Totality: total
Visibility: export

hrace : All (Async e es) ts -> Async e es (Maybe (HSum ts))

  This generalizes `race2` to an arbitrary heterogeneous list.

Totality: total
Visibility: export

race : Lazy a -> List (Async e es a) -> Async e es a

  A more efficient, monomorphic version of `hrace` with slightly
  different semantics: The winner decides the outcome of the are
  even if it has been cancele.

Totality: total
Visibility: export

race_ : List (Async e es ()) -> Async e es ()

  Runs several non-productive fibers in parallel, terminating
  as soon as the first one completes.

Totality: total
Visibility: export

bothOutcome : Async e es a -> Async e fs b -> Async e gs (Outcome es a, Outcome fs b)

  Races the evaluation of two fibers and returns the [[Outcome]] of both. If the race is
  canceled before one or both participants complete, then then whichever ones are incomplete
  are canceled.
  
  @param fa
    the effect for the first racing fiber
  @param fb
    the effect for the second racing fiber
  
  @see
    [[both]] for a simpler variant that returns the results of both fibers.
  

Totality: total
Visibility: export

both : Async e es a -> Async e es b -> Async e es (Maybe (a, b))

  Races the evaluation of two fibers and returns the result of both.
  
  The following rules describe the semantics of [[both]]:
  
    1. If the winner completes with [[Outcome.Succeeded]], the race waits for the loser to
       complete.
    2. If the winner completes with [[Outcome.Errored]], the race raises the
       error. The loser is canceled.
    3. If the winner completes with [[Outcome.Canceled]],
       the loser and the race are canceled as well.
    4. If the loser completes with
       [[Outcome.Succeeded]], the race returns the successful value of both fibers.
    5. If the
       loser completes with [[Outcome.Errored]], the race returns the error.
    6. If the loser
       completes with [[Outcome.Canceled]], the race is canceled.
    7. If the race is canceled
       before one or both participants complete, then whichever ones are incomplete are
       canceled.
  
  @param fa
    the effect for the first racing fiber
  @param fb
    the effect for the second racing fiber
  
  @see
    [[bothOutcome]] for a variant that returns the [[Outcome]] of both fibers.

Totality: total
Visibility: export

par : All (Async e es) ts -> Async e es (Maybe (HList ts))

  Runs the given heterogeneous list of asynchronous computations
  in parallel, collecting the results again in a heterogeneous list.

Totality: total
Visibility: export

parseq : List (Async e es a) -> Async e es (Maybe (List a))

  Runs the given list of computations in parallel.
  
  This fails with an error, as soon as the first computation
  fails, and it returns `Nothing` as soon as the first computation
  is canceled.

Totality: total
Visibility: export

parTraverse : (a -> Async e es b) -> List a -> Async e es (Maybe (List b))

  Traverses a list of values effectfully in parallel.
  
  This returns `Nothing` if one of the fibers was canceled.

Totality: total
Visibility: export

lazy : Lazy a -> Async e es a

  Wraps a lazy value in an `Async`.

Totality: total
Visibility: export

sleep : TimerH e => Clock Duration -> Async e es ()

  Delay a computation by the given number of nanoseconds.

Totality: total
Visibility: export

waitTill : TimerH e => Clock Monotonic -> Async e es ()

  Delay a computation by the given number of nanoseconds.

Totality: total
Visibility: export

delay : TimerH e => Clock Duration -> Async e es a -> Async e es a

  Delay a computation by the given number of nanoseconds.

Totality: total
Visibility: export

.ns : Nat -> Clock Duration

  Converts a number to nanoseconds

Totality: total
Visibility: export

.us : Nat -> Clock Duration

  Converts a number of microseconds to nanoseconds

Totality: total
Visibility: export

.s : Nat -> Clock Duration

  Converts a number of seconds to nanoseconds

Totality: total
Visibility: export

.ms : Nat -> Clock Duration

  Converts a number of milliseconds to nanoseconds

Totality: total
Visibility: export

.min : Nat -> Clock Duration

  Converts a number of minutes to nanoseconds

Totality: total
Visibility: export

.h : Nat -> Clock Duration

  Converts a number of hours to nanoseconds

Totality: total
Visibility: export

.d : Nat -> Clock Duration

  Converts a number of days to nanoseconds

Totality: total
Visibility: export

delta : HasIO io => io () -> io (Clock Duration)

  Runs an IO action, returning the time delta it took to run.

Totality: total
Visibility: export

syncApp : Async SyncST [] () -> IO ()

Visibility: export

traverseList : (a -> Async e es b) -> List a -> Async e es (List b)

  A stack-safe alternative to `traverse`, specialized for `List`.

Totality: total
Visibility: export