# Documentation

Init.Data.Channel

structure IO.Channel.State (α : Type) :

Internal state of an Channel.

We maintain the invariant that at all times either consumers or values is empty.

Instances For
instance IO.Channel.instInhabitedState :
{a : Type} →
Equations
• IO.Channel.instInhabitedState = { default := { values := default, consumers := default, closed := default } }
def IO.Channel (α : Type) :

FIFO channel with unbounded buffer, where recv? returns a Task.

A channel can be closed. Once it is closed, all sends are ignored, and recv? returns none once the queue is empty.

Equations
instance IO.instNonemptyChannel {α : Type} :
Equations
def IO.Channel.new {α : Type} :

Creates a new Channel.

Equations
def IO.Channel.send {α : Type} (v : α) (ch : ) :

Sends a message on an Channel.

This function does not block.

Equations
• One or more equations did not get rendered due to their size.
def IO.Channel.close {α : Type} (ch : ) :

Closes an Channel.

Equations
• One or more equations did not get rendered due to their size.
def IO.Channel.recv? {α : Type} (ch : ) :

Receives a message, without blocking. The returned task waits for the message. Every message is only received once.

Returns none if the channel is closed and the queue is empty.

Equations
• One or more equations did not get rendered due to their size.
partial def IO.Channel.forAsync {α : Type} (f : α) (ch : ) :

ch.forAsync f calls f for every messages received on ch.

Note that if this function is called twice, each forAsync only gets half the messages.

def IO.Channel.recvAllCurrent {α : Type} (ch : ) :

Receives all currently queued messages from the channel.

Those messages are dequeued and will not be returned by recv?.

Equations

Type tag for synchronous (blocking) operations on a Channel.

Equations
def IO.Channel.sync {α : Type} (ch : ) :

Accesses synchronous (blocking) version of channel operations.

For example, ch.sync.recv? blocks until the next message, and for msg in ch.sync do ... iterates synchronously over the channel. These functions should only be used in dedicated threads.

Equations
• = ch
def IO.Channel.Sync.recv? {α : Type} (ch : ) :

Synchronously receives a message from the channel.

Every message is only received once. Returns none if the channel is closed and the queue is empty.

Equations
• = do let __do_lift ← IO.wait __do_lift
instance IO.instForInSync {m : TypeType u_1} {α : Type} [inst : ] :
ForIn m () α

for msg in ch.sync do ... receives all messages in the channel until it is closed.

Equations
• IO.instForInSync = { forIn := fun {β} [] ch b f => }