IO.Async.Core

Reexports

Definitions

0 IOToken : Type

Totality: total
Visibility: public export

0 Callback : List Type -> Type -> Type

Totality: total
Visibility: public export

record Fiber : List Type -> Type -> Type

  A fiber is a series of computations that will be run
  in strict sequence and will eventually terminate
  with a result of type `Outcome es a`: It will either
  produce a result of type `a`, an error of type `HSum es`,
  or - in case it was canceled early - end with `Canceled`.
  
  From the outside, a fiber can be observed by installing 
  a callback, which will be invoked as soon as the fiber has
  terminated with a result.
  
  In addition, a running fiber can be canceled, so that it
  aborts all computations at soon as possible. Canceling a fiber
  that has already completed is a no-op.

Totality: total
Visibility: public export
Constructor: 

MkFiber : IO1 () -> (IOToken -> Callback es a -> IO1 (IO1 ())) -> Fiber es a

Projections:

.cancel_ : Fiber es a -> IO1 ()

.observe_ : Fiber es a -> IOToken -> Callback es a -> IO1 (IO1 ())

Hint: 

Resource (Async e) (Fiber es a)

.cancel_ : Fiber es a -> IO1 ()

Totality: total
Visibility: public export

cancel_ : Fiber es a -> IO1 ()

Totality: total
Visibility: public export

.observe_ : Fiber es a -> IOToken -> Callback es a -> IO1 (IO1 ())

Totality: total
Visibility: public export

observe_ : Fiber es a -> IOToken -> Callback es a -> IO1 (IO1 ())

Totality: total
Visibility: public export

data Async : Type -> List Type -> Type -> Type

  Sum-type describing the computation running on a fiber.
  
  `Async` can be thought of a powerful alternative to `IO`
  that comes with error handling, capabilities for
  spawning additional `Async` computations (each running
  on its of `Fiber`), plus the ability for being canceled
  (from the inside or from other fibers).
  
  In order to *run* an `Async` computation, we an
  `IO.Async.Loop.EventLoop`, which takes care of running
  many fibers (each of which might spawn additional fibers)
  concurrently. Some event loops will even offer true parallelism,
  distributing the fibers to be run across several operating
  system threads.

Totality: total
Visibility: public export
Constructors:

Bind : Async e es a -> (a -> Async e es b) -> Async e es b

  Implements bind (`>>=`)

Val : a -> Async e es a

  A pure result

Err : HSum es -> Async e es a

  An error

Sync : IO (Result es a) -> Async e es a

  A wrapped synchronous/blocking IO action

Cancel : Async e es ()

  Cancels the curret fiber

OnCncl : Async e es a -> Async e [] () -> Async e es a

  Run the given cancel hook when cancelation is observed for `act`

UC : (IOToken -> Nat -> Async e es a) -> Async e es a

  Masks a fiber as uncanceble
  This takes a function argument which will get the running fiber's
  identifier token plus cancelation id in order to unmask certain
  inner regions, where cancellation can again be observed.
  See also `Poll`.

Attempt : Async e es a -> Async e fs (Result es a)

  Error handling: In case an error occured, it is wrapped in
  a `Left`, while a successful result is wrapped in a `Right`.
  Note, that we do not handle the `Canceled` case: Cancellation
  cannot be undone. In can be temporarily masked using `UC`, but
  after that, it will be observed as soon as possible.

Env : Async e es e

  Returns the context currently handling this fiber, giving us access
  to functionality specific to the running event loop.

Self : Async e es IOToken

  Returns the current fiber's unique identifier

Cede : Async e es ()

  Cedes control to the execution context
  Fibers are auto-ceded after a predefined number of evaluation steps
  to make sure other fibers get a chance to run even when the event loop
  is single-threaded. In addition, a fiber can make room for other
  fibers by invoking `cede` at strategic points.

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

  Runs the given computation concurrently to this one returning a
  `Fiber` representing the runnign computation.

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

  The asynchronous primitive. This allows us to register callbacks
  and await their invocation, thus blocking the current fiber until
  a result is ready. Being able to treat this as a regular
  IO-like computation is one of the main reasons why `Async` is such
  a powerful abstraction.
  
  The `IO1 ()` returned after installing a callback will be treated
  as a cancellation hook: It will be invoked if the current
  computation is canceled and cancellation can currently be observed.
  
  We use this data constructor whenever we'd like to wait for a
  result to be ready at a later time such as a timer, input from
  a pipe or socket, or data available from standard input.

APoll : IOToken -> Nat -> Async e es a -> Async e es a

  Temporarily undo a layer of uncancelability. See also `UC`.

Hints:

ELift1 World (Async e)

HasIO (Async e es)

MCancel (Async e)

MErr (Async e)

Resource (Async e) (Fiber es a)

terminal : Result es a -> Async e es a

  Lifts a pure `Result` into `Async`.

Totality: total
Visibility: export

sync : IO (Result es a) -> Async e es a

  Lifts an effectful `Result` into `Async`.

Totality: total
Visibility: export

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

  Asynchronous FFI: Wraps a callback handler into `Async`.
  
  The `IO1 ()` action returned after registering the callback will
  be used for cancelation and cleanup.

Totality: total
Visibility: export

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

  Starts a new fiber, running it concurrently to the current one

Totality: total
Visibility: export

cede : Async e es ()

  Cedes control back to the execution context.

Totality: total
Visibility: export

env : Async e es e

  Returns the environment provided by the event loop this
  fiber is currently running in.

Totality: total
Visibility: export

self : Async e es IOToken

  Returns this fiber's unique identifier.

Totality: total
Visibility: export