IO.Async.Channel

Definitions

data SendRes : Type

Totality: total
Visibility: public export
Constructors:

Sent : SendRes

SentAndClosed : SendRes

Closed : SendRes

Hints:

Eq SendRes

Ord SendRes

Show SendRes

record Channel : Type -> Type

  A concurrent, bounded channel holding values of type `a`.
  
  This is an important primitive for implementing single
  consumer, multiple producer services.
  
  Note: Unlike with `IO.Async.BQueue`, which can have multiple
        consumers, this will only accpet a single consumer,
        silently overwriting an old consumer in case a new one
        calls.

Totality: total
Visibility: export
Constructor: 

C : IORef (ST a) -> Channel a

Projection: 

.ref : Channel a -> IORef (ST a)

channel : Lift1 World f => Nat -> f (Channel a)

  Creates a new bounded queue of the given capacity.

Totality: total
Visibility: export

channelOf : Lift1 World f => (0 a : Type) -> Nat -> f (Channel a)

  Utility alias for `channel` taking the type of stored values
  as an explicit argument.

Totality: total
Visibility: export

send : Channel a -> a -> Async e es SendRes

  Sends a value through a channel potentially blocking the
  calling fiber until there is some capacity.
  
  This returns
    * `Sent` if the data was received and the channel is still open after sending
    * `SentAndClosed` if the data was received and the channel is now closed
    * `Closed` if the data could not be sent since the channel is closed.

Totality: total
Visibility: export

receive : Channel a -> Async e es (Maybe a)

  Extracts the next value from a channel potentially blocking
  the calling fiber until such a value is available.
  
  This returns `Nothing` if the channel has been closed and
  no pending values are left.

Totality: total
Visibility: export

close : Channel a -> Async e es ()

  Gracefully closes the channel: No more data can be sent
  (`send` will return immedately with `Closed` from now on),
  put pending data can still be received.

Totality: total
Visibility: export