Skip to content

feat: describe Async#866

Open
david-christiansen wants to merge 6 commits into
mainfrom
async-monad
Open

feat: describe Async#866
david-christiansen wants to merge 6 commits into
mainfrom
async-monad

Conversation

@david-christiansen

Copy link
Copy Markdown
Collaborator

This PR adds a chapter about the Async monad and fixes some minor issues elsewhere.

This PR adds a chapter about the Async monad and fixes some minor
issues elsewhere.
@david-christiansen david-christiansen added the HTML available HTML has been generated for this PR label Jun 22, 2026
@github-actions

Copy link
Copy Markdown
Contributor

Preview for this PR is ready! 🎉 (also as a proofreading version). built with commit 22fca31.

Comment thread Manual/IO/Async.lean

Each of these monads has a corresponding type of asynchronous tasks that it can coordinate.
These tasks can be thought of as handles to an in-flight computation.
Calling {name}`async` on a monadic action creates a task that runs in the current thread until it suspends, and calling {name}`await` on a task results in a monadic action that waits for the task to complete.

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

async can run the computation on another thread, as it uses BaseIO.asTask internally without the sync flag

Comment thread Manual/IO/Async.lean

During selection, errors might occur at any stage of {ref "async-select"}[the protocol].
Errors thrown by a selector during the initial {name Selector.tryFn}`tryFn` loop terminate the selection immediately.
An error thrown from a {name Selector.registerFn}`registerFn` or {name Selector.unregisterFn}`unregisterFn`, by contrast, can leave selectors that were already registered without a matching call to {name Selector.unregisterFn}`unregisterFn`.

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

HTML available HTML has been generated for this PR

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants