IO.Async.Service

Definitions

record Service : Type -> List Type -> (req : Type) -> (req -> Type) -> Type

  A `Service` describes an asynchronous, effectful convertion from
  "requests" to (dependently typed) "responses" with the potential
  of failing with one of the given error types.
  
  A `Service` is a resource that should be properly released once it
  is no longer needed.

Totality: total
Visibility: public export
Constructor: 

MkService : Async e [] () -> ((r : req) -> Async e errs (resp r)) -> Service e errs req resp

Projections:

.close : Service e errs req resp -> Async e [] ()

.send : Service e errs req resp -> (r : req) -> Async e errs (resp r)

Hint: 

Resource (Async e) (Service e es a p)

.close : Service e errs req resp -> Async e [] ()

Totality: total
Visibility: public export

close : Service e errs req resp -> Async e [] ()

Totality: total
Visibility: public export

.send : Service e errs req resp -> (r : req) -> Async e errs (resp r)

Totality: total
Visibility: public export

send : Service e errs req resp -> (r : req) -> Async e errs (resp r)

Totality: total
Visibility: public export

service : {default 100 _ : Nat} -> (0 p : (a -> Type)) -> s -> (s -> (v : a) -> Async e es (s, p v)) -> Async e fs (Service e es a p)

  Sets up a stateful service that runs continuously in the background
  until it is finally closed.

Visibility: export

stateless : {default 100 _ : Nat} -> (0 p : (a -> Type)) -> ((v : a) -> Async e es (p v)) -> Async e fs (Service e es a p)

  Sets up a stateless service that runs continuously in the background
  until it is finally closed.

Visibility: export

stateful : {default 100 _ : Nat} -> (0 p : (a -> Type)) -> s -> (s -> (v : a) -> (s, p v)) -> Async e fs (Service e es a p)

  Sets up a stateful service that runs continuously in the background
  until it is finally closed.

Visibility: export