structure Control.Concurrent.Chan (α : Type) : Type

An unbounded FIFO channel, modelled after Haskell's Chan.

Supports dup: duplicated channels share writes but read independently. All blocking uses promises (non-blocking by type via BaseIO (Task α)).

$$\text{Chan.new} : \text{BaseIO}\ (\text{Chan}\ \alpha)$$

• readState : Std.Mutex (ChanReadState α)
• writeState : Std.Mutex (ChanWriteState α)

def Control.Concurrent.Chan.new (α : Type) : BaseIO (Chan α)

Create a new empty channel.

$$\text{new} : \text{BaseIO}\ (\text{Chan}\ \alpha)$$

Equations

• Control.Concurrent.Chan.new α = do let rs ← Std.Mutex.new { buffer := ∅, waiters := ∅ } let ws ← Std.Mutex.new { subscribers := #[rs] } pure { readState := rs, writeState := ws }

def Control.Concurrent.Chan.write {α : Type} (ch : Chan α) (val : α) : BaseIO Unit

Write a value to the channel. The value is delivered to all current subscribers (the original channel and any dups).

$$\text{write} : \text{Chan}\ \alpha \to \alpha \to \text{BaseIO}\ \text{Unit}$$

Equations

• One or more equations did not get rendered due to their size.

def Control.Concurrent.Chan.read {α : Type} [Nonempty α] (ch : Chan α) : BaseIO (Task α)

Read the next value from the channel. If the channel is empty, the caller becomes a dormant promise until a writer delivers a value.

$$\text{read} : \text{Chan}\ \alpha \to \text{BaseIO}\ (\text{Task}\ \alpha)$$

Never blocks an OS thread.

Equations

• One or more equations did not get rendered due to their size.

def Control.Concurrent.Chan.dup {α : Type} (ch : Chan α) : BaseIO (Chan α)

Duplicate a channel. The new channel will receive all future writes to the original channel, but has its own independent read position.

Values written before dup that haven't been read yet are NOT visible on the new channel (matching Haskell's dupChan semantics).

$$\text{dup} : \text{Chan}\ \alpha \to \text{BaseIO}\ (\text{Chan}\ \alpha)$$

Equations

• One or more equations did not get rendered due to their size.

def Control.Concurrent.Chan.tryRead {α : Type} (ch : Chan α) : BaseIO (Option α)

Try to read without blocking. Returns none if the channel is empty.

$$\text{tryRead} : \text{Chan}\ \alpha \to \text{BaseIO}\ (\text{Option}\ \alpha)$$

Equations

• One or more equations did not get rendered due to their size.