Async operations should be first-class citizens in Vera, modelled as an algebraic effect. An <Async> effect with async and await operations fits naturally:
fn fetch_both(@String, @String -> @Tuple<Json, Json>)
requires(true)
ensures(true)
effects(<Http, Async>)
{
let @Future<Json> = async(http_get(@String.0));
let @Future<Json> = async(http_get(@String.1));
let @Json = await(@Future<Json>.1);
let @Json = await(@Future<Json>.0);
Tuple(@Json.1, @Json.0)
}
Key design points:
async(expr) wraps an effectful computation in a Future<T>, starting it concurrently
await(@Future<T>.n) suspends until the future resolves
- The
<Async> effect must be declared, making concurrency explicit
- Handlers can provide different scheduling strategies (thread pool, event loop, sequential)
- Avoids coloured-function problems because algebraic effects already separate description from execution
Spec reference: spec/00-introduction.md § 0.8 "Asynchronous Promises/Futures"
Async operations should be first-class citizens in Vera, modelled as an algebraic effect. An
<Async>effect withasyncandawaitoperations fits naturally:Key design points:
async(expr)wraps an effectful computation in aFuture<T>, starting it concurrentlyawait(@Future<T>.n)suspends until the future resolves<Async>effect must be declared, making concurrency explicitSpec reference:
spec/00-introduction.md§ 0.8 "Asynchronous Promises/Futures"