Migrating mental model from Scala to Lean

lean_concurrency.md

Lean Parallelism and Concurrency for Cats-Effect/fs2 Users

Transient notes for someone fluent in cats-effect/fs2 who wants to write efficient, idiomatic Lean. This is based on Lean 4.29 sources and Std as installed in this workspace.

Executive Model

Lean's concurrency model is much closer to "native OS threads plus runtime tasks" than to cats-effect's fiber runtime.

In cats-effect, IO describes a computation, fibers are lightweight, cancellation is structured, and the runtime owns compute/blocking pools. In Lean, IO α is the effect monad, but asynchronous work is represented explicitly by Task α, which is scheduled on a runtime-managed pool of OS threads. A Task is closer to Scala Future or Rust JoinHandle than to a cats-effect Fiber.

The default Lean stack:

• IO α: effectful computation that may throw IO.Error.
• BaseIO α: infallible effectful computation.
• EIO ε α: effectful computation with typed errors.
• Task α: asynchronous computation handle.
• IO.asTask, BaseIO.asTask: start an effectful action eagerly in a task.
• Task.spawn: start a pure Unit → α computation.
• IO.Ref α: mutable cell with atomic pointer operations.
• Std.Mutex α: shared mutable state guarded by a C++/OS mutex.
• IO.Promise α: one-shot completion source for a Task.
• Std.Channel α: multi-producer/multi-consumer FIFO channel.
• Std.Broadcast, Std.Notify: higher-level synchronization primitives.

The most important migration warning:

Cats-effect code often assumes that blocking is tracked by the runtime. Lean does not generally know that a task is blocking unless it is blocking on Task.get/IO.wait. If you block on an OS mutex, file descriptor, process, or long synchronous call inside a regular task, you occupy a worker thread. Use dedicated task priority for long-running or blocking work.

Vocabulary Mapping

This mapping is approximate. Lean is not a cats-effect clone.

Cats-effect / fs2 concept	Lean concept	Notes
IO[A]	IO α	Effect monad. Lean IO is not a fiber runtime API.
Sync[F]	Monad, MonadLiftT, IO, BaseIO, EIO	Lean usually writes concrete monads or lightweight typeclass constraints.
Async[F]	Task, IO.asTask, IO.Promise, internal Async APIs	Async APIs exist, but much is lower-level or under Std.Internal.
Fiber[F, E, A]	Task α	No built-in structured fiber scope.
Deferred[F, A]	IO.Promise α	One-shot completion source. Result is a Task.
Ref[F, A]	IO.Ref α	Atomic update via modify/modifyGet; no public CAS.
Mutex / Semaphore	Std.Mutex, channels, custom state	Std.Mutex is a typed state cell plus C++ mutex.
Queue[F, A]	Std.Channel α, Std.CloseableChannel α	Bounded/unbounded/zero-buffer variants.
Topic / broadcast	Std.Broadcast	Broadcast channel with per-receiver state.
parMapN / parTraverse	spawn tasks and IO.wait/Task.get; write combinators	Lean has primitives, not the same rich combinator set.
race / select	IO.waitAny, internal Selectable.one	Public IO.waitAny works on tasks; richer selector machinery is internal.
Stream[F, A]	ForIn, iterators, channels, custom loops	No direct fs2 equivalent in core Std.
Resource / bracket	try/finally, MonadFinally	Use try ... finally ... for cleanup.
uncancelable / masks	no direct equivalent	Cancellation is cooperative and comparatively weak.
IO.blocking	Task.Priority.dedicated by convention	Dedicated tasks are the closest standard lever.

IO, BaseIO, and EIO

Lean splits effects by error behavior:

BaseIO α       -- cannot throw
EIO ε α        -- can throw ε
IO α           -- can throw IO.Error

IO is an executable effect monad. It is not, by itself, an async/fiber runtime like cats-effect IO. To run work concurrently, create tasks explicitly.

Typical effectful task:

def work (n : Nat) : IO Nat := do
  IO.println s!"working on {n}"
  pure (n + 1)

def start : BaseIO (Task (Except IO.Error Nat)) := do
  (work 41).asTask

Because IO can fail, IO.asTask returns Task (Except IO.Error α). For infallible actions, BaseIO.asTask returns Task α.

A useful pattern is to normalize at boundaries:

def waitIO (t : Task (Except IO.Error α)) : IO α := do
  IO.ofExcept (← IO.wait t)

Task.get is pure-looking but blocks the current thread. In IO, prefer IO.wait t, which makes the blocking explicit in the type.

Tasks Are Eager Handles

IO.asTask act starts act when the surrounding BaseIO action is run. Dropping the task handle does not necessarily stop the underlying action. The source docs say actions should explicitly call IO.checkCanceled if they should react to cancellation.

This is very different from cats-effect structured concurrency. If you start a task, you own the lifetime discipline.

Lean tasks are scheduled by priority:

Task.Priority.default   -- 0
Task.Priority.max       -- 8
Task.Priority.dedicated -- 9

Regular priorities 0..8 use the standard task pool. Higher priorities spawn a dedicated OS thread. Higher numeric regular priority is scheduled before lower priority.

Use Task.Priority.dedicated for long-running or blocking work:

def readAllDedicated (p : System.FilePath) : BaseIO (Task (Except IO.Error String)) :=
  (IO.FS.readFile p).asTask Task.Priority.dedicated

Do not use (sync := true) for work that can block or do significant computation. Lean's docs say sync := true continuations should be cheap and non-blocking.

Scheduler Details

Lean's task manager has:

• a queue per regular priority 0..8;
• a maximum regular worker count initialized from LEAN_NUM_THREADS or hardware concurrency;
• dedicated workers for priority > Task.Priority.max;
• dependency tracking for Task.map/Task.bind;
• a special compensation path for Task.get.

If a worker blocks on Task.get, the runtime temporarily increases the maximum standard worker count by one and may spawn another worker. This avoids starvation when pool tasks wait on other Lean tasks.

This compensation is specific to task waiting. It does not happen for:

• Std.Mutex.lock;
• arbitrary C/FFI blocking calls;
• blocking file/process APIs;
• Channel.Sync.recv once it reaches an underlying wait;
• long CPU loops that do not yield or finish.

So the cats-effect mental model:

IO.blocking(thunk)

roughly becomes:

thunk.asTask Task.Priority.dedicated

There is no automatic "blocking region" marker with runtime migration. You choose the task priority when you start the work.

On FreeBSD and Linux, the regular task pool consists of native OS threads. std::thread, std::mutex, std::condition_variable, and std::shared_mutex behavior is inherited from the C++ standard library and platform threading primitives. On Linux this typically bottoms out in pthreads and futex-like parking. On FreeBSD it bottoms out in the platform pthread implementation. Lean does not add a JVM-like monitor layer.

Parallel Map and Traverse

There is no direct parTraverse in core Lean with cats-effect ergonomics, but the basic pattern is small:

def parMapArray (xs : Array α) (f : α → IO β)
    (prio := Task.Priority.default) : IO (Array β) := do
  let mut tasks := #[]
  for x in xs do
    tasks := tasks.push (← (f x).asTask prio)

  let mut out := #[]
  for t in tasks do
    out := out.push (← IO.ofExcept (← IO.wait t))
  pure out

This starts all tasks eagerly, then waits in order. Results preserve input order. Failure handling is manual: because each task returns Except IO.Error β, decide whether to fail fast, collect errors, cancel siblings, or keep going.

A bounded parallel traversal can be built with Std.Channel, a worker pool, and an output ref/channel. For many Lean programs, a simple array of tasks is enough. If you need fs2-style bounded concurrency, write a small domain-specific combinator.

Cost implications:

• each task is a heap object plus scheduling overhead;
• regular tasks consume pool capacity while running;
• waiting on Task.get/IO.wait has scheduler compensation only for Lean tasks;
• dedicated tasks create/detach OS threads, so do not use them for millions of tiny jobs;
• sync := true avoids queueing a continuation but must remain cheap.

Cancellation

Lean cancellation is cooperative and much weaker than cats-effect cancellation.

Available pieces:

IO.cancel task        -- request cancellation
IO.checkCanceled      -- task checks its own cancellation flag
IO.CancelToken        -- separate cooperative shared token

Dropping the last reference to some task structures can request cancellation, but user code should not treat this like cats-effect finalizer-safe cancellation. The docs repeatedly say tasks should explicitly call IO.checkCanceled to react.

Typical polling loop:

partial def loop : IO Unit := do
  if ← IO.checkCanceled then
    return ()
  -- do a bounded chunk of work
  loop

For APIs you design, pass an IO.CancelToken or periodically check IO.checkCanceled. For blocking foreign calls, cancellation will not magically interrupt the OS operation unless that API supports it and you wire it up yourself.

Use try/finally for cleanup:

def withLockLike [MonadFinally m] (acquire : m Unit) (release : m Unit) (body : m α) : m α := do
  try
    acquire
    body
  finally
    release

This is closer to bracket than to CE's full cancelation masks.

IO.Ref: The Fast Atomic Cell

IO.Ref α is ST.Ref IO.RealWorld α. It is a real runtime heap object with one mutable pointer slot. The Lean Prop fields in its declaration are erased; the runtime object is the actual ref cell.

Use it for:

• counters and metrics;
• small shared state;
• memoization flags;
• one-cell coordination;
• cheap atomic pure updates.

Important operations:

IO.mkRef init
ref.get
ref.set x
ref.swap x
ref.modify f
ref.modifyGet f

modifyGet is the closest standard tool to cats-effect Ref.modify:

let old ← ref.modifyGet fun s =>
  let s' := s + 1
  (s, s')

Runtime behavior:

• single-threaded refs are normal pointer load/store plus reference counting;
• multi-threaded/global refs use atomic pointer exchange;
• modify/modifyGet use take then set;
• while a ref is taken, competing get/take spin until it is set again.

There is no public general CAS API. IO.Ref is great for short pure updates. Do not put expensive or effectful logic in a ref update. For that, use Std.Mutex.

Std.Mutex: Lean's Shared-State Workhorse

Std.Mutex α is an IO.Ref α plus a BaseMutex.

def useMutex : BaseIO Nat := do
  let m ← Std.Mutex.new 0
  m.atomically do
    let n ← get
    set (n + 1)
    pure n

The runtime BaseMutex is a Lean external object wrapping C++ std::mutex. lock blocks the OS thread. Uncontended performance is whatever your C++ library and OS provide. Lean does not integrate mutex blocking with the task manager.

Use Std.Mutex for:

• larger state transitions;
• effect-polymorphic code inside AtomicT;
• coordination where spinning would be bad;
• invariants across multiple fields.

Keep critical sections short. Avoid calling long-running IO, blocking waits, or task joins while holding the mutex unless you have designed for it.

Related primitives:

• Std.RecursiveMutex α: reentrant version.
• Std.SharedMutex α: multiple readers or one writer.
• Std.Condvar: condition variable for use with BaseMutex/Mutex.

IO.Promise: Deferred

IO.Promise α is close to Deferred[IO, A].

def promiseExample : BaseIO Nat := do
  let p ← IO.Promise.new
  p.resolve 42
  IO.wait (p.resultD 0)

Important details:

• Promise.resolve only wins once.
• Promise.result? : Task (Option α) resolves to none if the promise is dropped unresolved.
• Promise.result! can panic/block forever if not resolved; prefer result? or resultD.

Promises are useful for hand-built async protocols, channels, and callbacks from FFI.

Std.Channel: Lean's Queue and Coordination Primitive

Std.Channel α is a multi-producer/multi-consumer FIFO with:

• unbounded buffering: capacity := none;
• zero-buffer rendezvous: capacity := some 0;
• bounded buffering: capacity := some n.

Async API:

let ch ← Std.Channel.new (α := Nat) (some 16)
let sendTask ← ch.send 1
let recvTask ← ch.recv

send/recv return tasks that complete when the operation can complete. The synchronous view blocks:

let sync := ch.sync
sync.send 1
let x ← sync.recv

For completion, use Std.CloseableChannel α:

let ch ← Std.CloseableChannel.new (α := String) (some 64)
-- producers send
-- close when done
ch.close
for msg in ch.sync do
  IO.println msg

CloseableChannel.Sync has a ForIn instance: for msg in ch.sync do ... receives until close.

Cost model:

• channel state is protected by Std.Mutex;
• blocked senders/receivers are represented with IO.Promise;
• async send/recv generally allocate tasks/promises when they cannot complete immediately;
• synchronous send/recv waits on tasks and therefore blocks the current thread.

This is a good Lean-native replacement for many fs2 Queue and producer/consumer patterns. It is not an fs2 Stream: it does not provide fusion, chunking, resource scopes, or rich combinators.

Std.Broadcast and Std.Notify

Std.Broadcast is a broadcast channel inspired by Tokio. It lets multiple receivers observe a stream of messages, with bounded buffering and receiver positions. Use it when Channel's work-queue semantics are wrong because each message should go to many consumers.

Std.Notify is a lightweight event signal:

• no payload;
• no buffering;
• if nobody is waiting, notification is lost;
• can notify one or all waiters;
• supports selector-style waiting internally.

This is closer to a condition/event primitive than to a queue.

Async and Selectable APIs

Lean 4.29 has a Std.Internal.IO.Async stack with:

• BaseAsync, EAsync, Async;
• MonadAsync, MonadAwait;
• task wrappers such as ETask;
• Selectable.one / selector-based multiplexing;
• AsyncRead, AsyncWrite, AsyncStream classes.

The module itself says to prefer higher-level combinators such as race, raceAll, concurrently, background, and concurrentlyAll. Some of this lives under Std.Internal, so treat it as less stable than IO, Task, Mutex, and Channel.

As a cats-effect user, think of this area as the emerging Lean-native async vocabulary, not as a drop-in Async[F] hierarchy.

Publicly stable fallback:

• race completed tasks with IO.waitAny;
• coordinate custom event sources with IO.Promise;
• use Std.Channel for many producer/consumer workflows.

Iteration and Streams

Lean's everyday loop abstraction is ForIn, not fs2 Stream.

for x in xs do
  ...

This desugars through ForIn.forIn, which supports monadic loop bodies, break, continue, and local mutable state. Arrays and many collections have efficient ForIn instances.

For effectful data sources:

• CloseableChannel.Sync supports for msg in ch.sync do ... until close.
• Channel.Sync supports infinite receive loops.
• Init.Data.Iterators provides iterator infrastructure for collections.
• You can define ForIn for your own source type.

If you want fs2-like streaming, expect to build or choose a small abstraction. Lean's standard tools favor explicit loops, channels, and tasks over a universal stream algebra.

Common Patterns

Fire Two IO Actions in Parallel

def both (fa : IO α) (fb : IO β) : IO (α × β) := do
  let ta ← fa.asTask
  let tb ← fb.asTask
  let a ← IO.ofExcept (← IO.wait ta)
  let b ← IO.ofExcept (← IO.wait tb)
  pure (a, b)

This starts both eagerly. If fa fails, this does not automatically cancel fb; add that policy yourself if needed.

Race Tasks

def firstFinished (tasks : List (Task α)) (h : tasks.length > 0) : BaseIO α := do
  IO.waitAny tasks h

For IO tasks, the result type is usually Except IO.Error α, so decide how to handle the winner's error and whether to cancel losers.

Shared Counter

def inc (r : IO.Ref Nat) : BaseIO Nat := do
  r.modifyGet fun n =>
    let n' := n + 1
    (n', n')

Use IO.Ref for this, not Mutex.

Shared Map with Larger Update

abbrev Table := Std.HashMap String Nat

def addHit (m : Std.Mutex Table) (key : String) : BaseIO Unit := do
  m.atomically do
    modify fun table =>
      table.insert key ((table.getD key 0) + 1)

Use Mutex when the state transition is bigger or easier to express as ordinary state code.

Worker Pool with Channel

Sketch:

def worker (jobs : Std.CloseableChannel.Sync Job) : IO Unit := do
  for job in jobs do
    process job

def runPool (n : Nat) (jobs : Array Job) : IO Unit := do
  let ch ← Std.CloseableChannel.new (α := Job) (some 128)
  let mut workers := #[]
  for _ in [:n] do
    workers := workers.push (← (worker ch.sync).asTask)

  for job in jobs do
    discard <| EIO.toIO (fun e => IO.userError (toString e)) (ch.sync.send job)
  discard <| EIO.toIO (fun e => IO.userError (toString e)) ch.close

  for t in workers do
    discard <| IO.ofExcept (← IO.wait t)

For blocking process, start workers with Task.Priority.dedicated or isolate blocking calls in dedicated tasks.

Cost Checklist

When choosing a primitive, ask:

• Is the operation pure and tiny? Use IO.Ref.modifyGet.
• Is it a multi-field invariant? Use Std.Mutex.
• Is it producer/consumer coordination? Use Std.Channel or Std.CloseableChannel.
• Does every consumer need every event? Use Std.Broadcast.
• Is it just an edge-triggered signal? Use Std.Notify.
• Is it long-running or blocking? Use Task.Priority.dedicated.
• Do you need cancellation? Design it explicitly and poll IO.checkCanceled or a token.
• Do you need structured concurrency? Build a small scope abstraction for your application.

Platform Notes: FreeBSD and Linux

Lean's regular task pool and dedicated tasks are native threads. The runtime uses C++ threading abstractions:

• std::thread;
• std::mutex;
• std::recursive_mutex;
• std::shared_mutex;
• std::condition_variable;
• atomics for refs, reference counts, and runtime internals.

On Linux, the C++ library typically maps mutex/condition-variable blocking to pthreads and futex-like kernel parking. On FreeBSD, it maps to FreeBSD's pthread implementation. Lean itself does not add managed-runtime lock optimizations like the JVM, nor cats-effect-style blocking pool migration.

For portable performance:

• keep regular task work CPU-bound and finite;
• use dedicated priority for blocking or long-lived workers;
• avoid blocking while holding Std.Mutex;
• use bounded channels for backpressure;
• avoid spawning huge numbers of dedicated tasks;
• prefer Task.map/Task.bind over Task.get for dependencies when convenient.

Mental Model Shift

The cats-effect/fs2 habit is to describe a graph of effects and let the runtime manage fibers, cancelation, fairness, and blocking shifts. In Lean, you more often write explicit concurrency:

• start tasks;
• pick priorities;
• wait or compose task dependencies;
• protect state with refs/mutexes;
• coordinate with promises/channels;
• write cleanup and cancellation protocols directly.

That explicitness is not accidental. Lean is designed first as a theorem prover and systems language with a small runtime, not as a full managed effect runtime. The payoff is that the cost model is fairly direct once you know the primitives: tasks are OS-thread scheduled work items, mutexes are OS mutexes, refs are atomic pointer cells, and channels are mutex/promise-based coordination structures.