Idris2Doc : IO.Async.Fiber

IO.Async.Fiber

(source)
Definitions
record ExecutionContext : Type
  A context for submitting and running commands asynchronously.

  Totality: total
  Visibility: public export
  Constructor: 
EC : TokenGen -> (IO () -> IO ()) -> Nat -> ExecutionContext

  Projections:
  
.limit : ExecutionContext -> Nat
  
.submit : ExecutionContext -> IO () -> IO ()
  
.tokenGen : ExecutionContext -> TokenGen

  Hint: 
ExecutionContext => TokenGen
.tokenGen : ExecutionContext -> TokenGen
  Totality: total
  Visibility: public export
tokenGen : ExecutionContext -> TokenGen
  Totality: total
  Visibility: public export
.submit : ExecutionContext -> IO () -> IO ()
  Totality: total
  Visibility: public export
submit : ExecutionContext -> IO () -> IO ()
  Totality: total
  Visibility: public export
.limit : ExecutionContext -> Nat
  Totality: total
  Visibility: public export
limit : ExecutionContext -> Nat
  Totality: total
  Visibility: public export
ecToTokenGen : ExecutionContext => TokenGen
  Totality: total
  Visibility: export
record Fiber : List Type -> Type -> Type
  A fiber is a synchronous (sequential) computation producing
  an outcome of type `Outcome es a` eventually.
  
  We can register a callback at a fiber to get informed about its
  termination, and we can externally interrupt a running fiber
  by canceling it.

  Totality: total
  Visibility: public export
  Constructor: 
MkFiber : Token -> (Token -> (Outcome es a -> IO ()) -> IO ()) -> (Token -> IO ()) -> IO () -> Fiber es a

  Projections:
  
.cancel : Fiber es a -> IO ()
  
.observe : Fiber es a -> Token -> (Outcome es a -> IO ()) -> IO ()
  
.stopObserving : Fiber es a -> Token -> IO ()
  
.token : Fiber es a -> Token
.token : Fiber es a -> Token
  Totality: total
  Visibility: public export
token : Fiber es a -> Token
  Totality: total
  Visibility: public export
.observe : Fiber es a -> Token -> (Outcome es a -> IO ()) -> IO ()
  Totality: total
  Visibility: public export
observe : Fiber es a -> Token -> (Outcome es a -> IO ()) -> IO ()
  Totality: total
  Visibility: public export
.stopObserving : Fiber es a -> Token -> IO ()
  Totality: total
  Visibility: public export
stopObserving : Fiber es a -> Token -> IO ()
  Totality: total
  Visibility: public export
.cancel : Fiber es a -> IO ()
  Totality: total
  Visibility: public export
cancel : Fiber es a -> IO ()
  Totality: total
  Visibility: public export
data Async : List Type -> Type -> Type
  `Async es a` is a monad for describing asynchronous computations
  producing a result of type `Outcome es a` eventually.

  Totality: total
  Visibility: export
  Constructors:
  
Term : Outcome es a -> Async es a
  
Sync : Cancelability -> IO (Result es a) -> Async es a
  
Start : Cancelability -> Async es a -> Async fs (Fiber es a)
  
Shift : ExecutionContext -> Async es ()
  
Self : Async es Token
  
Cancel : Async es ()
  
GetEC : Async es ExecutionContext
  
Asnc : Cancelability -> ((Outcome es a -> IO ()) -> IO (Maybe (Async [] ()))) -> Async es a
  
Bind : Cancelability -> Async es a -> (Outcome es a -> Async fs b) -> Async fs b

  Hints:
  
Applicative (Async es)
  
Functor (Async es)
  
HasIO (Async es)
  
Monad (Async es)
succeed : a -> Async es a
  Totality: total
  Visibility: export
sync : IO (Result es a) -> Async es a
  Totality: total
  Visibility: export
uncancelable : Async fs a -> Async fs a
  Totality: total
  Visibility: export
cancelable : Async fs a -> Async fs a
  Totality: total
  Visibility: export
strictCancelable : Async fs a -> Async fs a
  Totality: total
  Visibility: export
canceled : Async es ()
  Totality: total
  Visibility: export
self : Async es Token
  Returns the unique token of the currently running fiber.

  Totality: total
  Visibility: export
cancelableAsync : ((Outcome es a -> IO ()) -> IO (Async [] ())) -> Async es a
  Totality: total
  Visibility: export
async : ((Outcome es a -> IO ()) -> IO ()) -> Async es a
  Totality: total
  Visibility: export
join : Fiber es a -> Async fs (Outcome es a)
  Totality: total
  Visibility: export
joinResult : Fiber es a -> Async es a
  Totality: total
  Visibility: export
cancel : Fiber es a -> Async fs ()
  Totality: total
  Visibility: export
start : Async es a -> Async fs (Fiber es a)
  Runs an asynchronous computation in the background on a new fiber.
  
  The resulting fiber can be canceled from the current fiber, and
  we can semantically block the current fiber to wait for the background
  computation to complete.
  
  See also `cancel` and `join`.

  Totality: total
  Visibility: export
background : Async es a -> Async fs ()
  Asynchronously runs a computation on a new fiber.
  
  While we can no longer observe the computation's result, it will still
  be canceled if the current fiber terminates.

  Totality: total
  Visibility: export
fail : HSum es -> Async es a
  Totality: total
  Visibility: export
throw : Has e es => e -> Async es a
  Totality: total
  Visibility: export
injectEither : Has e es => Either e a -> Async es a
  Inject an `Either e a` computation into an `Async` monad dealing
  with several possible errors.

  Totality: total
  Visibility: export
injectIO : Has e es => IO (Either e a) -> Async es a
  Inject an `IO (Either e a)` computation into an `Async` monad dealing
  with several possible errors.

  Totality: total
  Visibility: export
handleErrors : (HSum es -> Async fs a) -> Async es a -> Async fs a
  Totality: total
  Visibility: export
mapErrors : (HSum es -> HSum fs) -> Async es a -> Async fs a
  Totality: total
  Visibility: export
weakenErrors : Async [] a -> Async fs a
  Totality: total
  Visibility: export
dropErrs : Async es () -> Async [] ()
  Totality: total
  Visibility: export
0 Handler : Type -> Type -> Type
  Totality: total
  Visibility: public export
handle : All (Handler a) es -> Async es a -> Async [] a
  Totality: total
  Visibility: export
liftErrors : Async es a -> Async fs (Result es a)
  Totality: total
  Visibility: export
liftError : Async [e] a -> Async fs (Either e a)
  Totality: total
  Visibility: export
guaranteeCase : Async es a -> (Outcome es a -> Async [] ()) -> Async es a
  Totality: total
  Visibility: export
onCancel : Async es a -> Async [] () -> Async es a
  Totality: total
  Visibility: export
onAbort : Async es a -> Async [] () -> Async es a
  Guarantees to run the given cleanup hook in case a fiber
  has been canceled or failed with an error.
  
  See `guarantee` for additional information.

  Totality: total
  Visibility: export
finally : Async es a -> Async [] () -> Async es a
  Guarantees to run the given cleanup hook in case
  the given computation finishes with an outcome.
  
  See `guarantee` for additional information.

  Totality: total
  Visibility: export
forget : Async es a -> Async [] ()
  Totality: total
  Visibility: export
consume : Async es a -> (Outcome es a -> IO ()) -> Async [] ()
  Totality: total
  Visibility: export
bracketCase : Async es a -> (a -> Async es b) -> ((a, Outcome es b) -> Async [] ()) -> Async es b
  Totality: total
  Visibility: export
bracket : Async es a -> (a -> Async es b) -> (a -> Async [] ()) -> Async es b
  Totality: total
  Visibility: export
raceF : List (Async es (Fiber es a)) -> Async es a
  Semantically blocks the current fiber until one
  of the given fibers has produced an outcome, in which
  the others are canceled immediately.
  
  This is useful if you for instance have several abort conditions
  such as a timer and a signal from the operating system, and want
  to stop your process as soon as the first of the conditions
  occurs.

  Totality: total
  Visibility: export
race : List (Async es a) -> Async es a
  Alias for `raceF . traverse start`.

  Totality: total
  Visibility: export
raceAny : All (Async es) ts -> Async es (HSum ts)
  Runs a heterogeneous list of asynchronous computations in parallel,
  keeping only the one that finishes first.

  Totality: total
  Visibility: export
parF : All (Async es . Fiber es) ts -> Async es (HList ts)
  Accumulates the results of the given heterogeneous list of
  fibers in a heterogeneous list.

  Totality: total
  Visibility: export
par : All (Async es) ts -> Async es (HList ts)
  Runs the given computations in parallel and collects the outcomes
  in a heterogeneous list.

  Totality: total
  Visibility: export
runAsyncWith : ExecutionContext => Async es a -> (Outcome es a -> IO ()) -> IO ()
  Visibility: export
runAsync : ExecutionContext => Async es a -> IO ()
  Visibility: export