Concurrent type alias

@[reducible, inline]

abbrev Control.Concurrent.Concurrent (α : Type) : Type

A computation that produces a $\text{Task}\ \alpha$ without blocking the calling OS thread.

$$\text{Concurrent}\ \alpha \triangleq \text{BaseIO}\ (\text{Task}\ \alpha)$$

Compose with BaseIO.bindTask to chain continuations as tasks. Any function returning Concurrent α is non-blocking by construction.

Equations

• Control.Concurrent.Concurrent α = BaseIO (Task α)

MVar internals

MVar structure

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

A synchronisation variable that is either empty or holds a value.

$\text{MVar}$ is the fundamental building block for concurrent data structures. All blocking is promise-based: waiting tasks are dormant promises, not blocked OS threads. This allows scaling to millions of concurrent tasks.

Constraint: Blocking operations (take, read, swap, etc.) require [Nonempty α] for IO.Promise construction.

Modelled after Haskell's Control.Concurrent.MVar.

• state : Std.Mutex (MVarState α)

Construction

def Control.Concurrent.MVar.new {α : Type} (a : α) : BaseIO (MVar α)

Create a new $\text{MVar}$ containing value $a$.

$$\text{new} : \alpha \to \text{BaseIO}\ (\text{MVar}\ \alpha)$$

Equations

• Control.Concurrent.MVar.new a = do let __do_lift ← Std.Mutex.new { value := some a, takers := ∅, putters := ∅ } pure { state := __do_lift }

def Control.Concurrent.MVar.newEmpty (α : Type) : BaseIO (MVar α)

Create a new empty $\text{MVar}$.

$$\text{newEmpty} : \text{BaseIO}\ (\text{MVar}\ \alpha)$$

Equations

• Control.Concurrent.MVar.newEmpty α = do let __do_lift ← Std.Mutex.new { value := none, takers := ∅, putters := ∅ } pure { state := __do_lift }

Internal helpers

Core async operations (non-blocking)

def Control.Concurrent.MVar.take {α : Type} [Nonempty α] (mv : MVar α) : BaseIO (Task α)

Take the value from the MVar, leaving it empty. If the MVar is empty, the caller becomes a dormant promise until a put fills it.

$$\text{take} : \text{MVar}\ \alpha \to \text{BaseIO}\ (\text{Task}\ \alpha)$$

Fairness: Takers are served in FIFO order from Std.Queue.

Equations

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

def Control.Concurrent.MVar.put {α : Type} (mv : MVar α) (a : α) : BaseIO (Task Unit)

Put a value into the MVar. If the MVar is full, the caller becomes a dormant promise until a take empties it.

$$\text{put} : \text{MVar}\ \alpha \to \alpha \to \text{BaseIO}\ (\text{Task}\ \text{Unit})$$

Fairness: Putters are served in FIFO order from Std.Queue.

Equations

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

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

Read the value without removing it. If empty, waits like take then puts the value back.

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

Equations

• mv.read = do let takeTask ← mv.take BaseIO.bindTask takeTask fun (val : α) => do let putTask ← mv.put val pure (Task.map (fun (x : Unit) => val) putTask)

def Control.Concurrent.MVar.swap {α : Type} [Nonempty α] (mv : MVar α) (newVal : α) : BaseIO (Task α)

Swap the value in the MVar: take the old, put the new.

$$\text{swap} : \text{MVar}\ \alpha \to \alpha \to \text{BaseIO}\ (\text{Task}\ \alpha)$$

Returns the old value.

Equations

• mv.swap newVal = do let takeTask ← mv.take BaseIO.bindTask takeTask fun (old : α) => do let putTask ← mv.put newVal pure (Task.map (fun (x : Unit) => old) putTask)

def Control.Concurrent.MVar.withMVar {α β : Type} [Nonempty α] (mv : MVar α) (f : α → BaseIO (α × β)) : BaseIO (Task β)

Apply a function $f$ to the MVar contents and return a result.

$$\text{withMVar} : \text{MVar}\ \alpha \to (\alpha \to \text{BaseIO}\ (\alpha \times \beta)) \to \text{BaseIO}\ (\text{Task}\ \beta)$$

Takes the value, applies $f$, puts back $\pi_1(f(a))$, returns $\pi_2(f(a))$. If $f$ throws, the MVar remains empty (matching Haskell semantics).

Equations

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

def Control.Concurrent.MVar.modify {α β : Type} [Nonempty α] (mv : MVar α) (f : α → BaseIO (α × β)) : BaseIO (Task β)

Modify the MVar contents and return a result.

$$\text{modify} : \text{MVar}\ \alpha \to (\alpha \to \text{BaseIO}\ (\alpha \times \beta)) \to \text{BaseIO}\ (\text{Task}\ \beta)$$

Equations

• mv.modify f = mv.withMVar f

def Control.Concurrent.MVar.modify_ {α : Type} [Nonempty α] (mv : MVar α) (f : α → BaseIO α) : BaseIO (Task Unit)

Modify the MVar contents without returning a result.

$$\text{modify\_} : \text{MVar}\ \alpha \to (\alpha \to \text{BaseIO}\ \alpha) \to \text{BaseIO}\ (\text{Task}\ \text{Unit})$$

Equations

• mv.modify_ f = mv.withMVar fun (a : α) => do let a' ← f a pure (a', ())

Try operations (non-blocking, immediate)

def Control.Concurrent.MVar.tryTake {α : Type} (mv : MVar α) : BaseIO (Option α)

Try to take the value. Returns some v immediately if full, none if empty.

$$\text{tryTake} : \text{MVar}\ \alpha \to \text{BaseIO}\ (\text{Option}\ \alpha)$$

Equations

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

def Control.Concurrent.MVar.tryPut {α : Type} (mv : MVar α) (a : α) : BaseIO Bool

Try to put a value. Returns true if successful, false if full.

$$\text{tryPut} : \text{MVar}\ \alpha \to \alpha \to \text{BaseIO}\ \text{Bool}$$

Equations

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

def Control.Concurrent.MVar.tryRead {α : Type} (mv : MVar α) : BaseIO (Option α)

Try to read the value without removing it.

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

Equations

• mv.tryRead = (Control.Concurrent.MVar.state✝ mv).atomically do let __do_lift ← get pure (Control.Concurrent.MVarState.value✝ __do_lift)

def Control.Concurrent.MVar.isEmpty {α : Type} (mv : MVar α) : BaseIO Bool

Check if the MVar is empty. This is a snapshot — may be stale by the time you act on it.

$$\text{isEmpty} : \text{MVar}\ \alpha \to \text{BaseIO}\ \text{Bool}$$

Equations

• mv.isEmpty = (Control.Concurrent.MVar.state✝ mv).atomically do let __do_lift ← get pure (Control.Concurrent.MVarState.value✝ __do_lift).isNone

Sync wrappers (convenience — blocks OS thread)

def Control.Concurrent.MVar.takeSync {α : Type} [Nonempty α] (mv : MVar α) : BaseIO α

Take the value, blocking the OS thread until available.

$$\text{takeSync} : \text{MVar}\ \alpha \to \text{BaseIO}\ \alpha$$

Prefer take (async) for scalable code.

Equations

• mv.takeSync = do let __do_lift ← mv.take IO.wait __do_lift

def Control.Concurrent.MVar.putSync {α : Type} (mv : MVar α) (a : α) : BaseIO Unit

Put a value, blocking the OS thread until the MVar is empty.

$$\text{putSync} : \text{MVar}\ \alpha \to \alpha \to \text{BaseIO}\ \text{Unit}$$

Prefer put (async) for scalable code.

Equations

• mv.putSync a = do let __do_lift ← mv.put a IO.wait __do_lift

def Control.Concurrent.MVar.readSync {α : Type} [Nonempty α] (mv : MVar α) : BaseIO α

Read the value, blocking the OS thread until available.

$$\text{readSync} : \text{MVar}\ \alpha \to \text{BaseIO}\ \alpha$$

Prefer read (async) for scalable code.

Equations

• mv.readSync = do let __do_lift ← mv.read IO.wait __do_lift

Fairness properties (documented)

FIFO ordering: Elements dequeued from Std.Queue come out in insertion order. MVar always enqueues at the back and dequeues from the front, so waiters are served in FIFO order.

take_resolves_on_put: If an MVar is empty with a taker waiting, a subsequent put resolves the head taker's promise with the put value.

no_lost_wakeups: Every put on an empty MVar either fills it or wakes exactly one taker. Every take on a full MVar either empties it or wakes exactly one putter.