Context System

The context system replaces ambient state — globals, thread-locals, singletons, "magic" dependency injection — with typed, explicitly declared capabilities.

Two levels

Verum offers two complementary DI mechanisms.

Which contexts already exist

A context must be declared before using [...] will accept it — error<E605>: undefined context otherwise.

The ten you will reach for in ordinary code are Logger, Database, Auth, Config, Cache, Metrics, Tracer, Clock, FileSystem (all in core/context/standard.vr) and Random (core/context/random.vr). See stdlib → context.

Other contexts are available. List their declarations with:

grep -rcE '^ *(public |pub )?context +[A-Za-z_]' core/ --include='*.vr' \
  | grep -v ':0'

Thirty-three, in eight files. Besides the ten above: fourteen compile-time contexts in core/meta/contexts.vr — TypeInfo, AstAccess, CompileDiag, Hygiene, StageInfo, MacroState, MetaRuntime, MetaBench, BuildAssets, CodeSearch, DepGraph, ProjectInfo, Schema, SourceMap — three for autodiff (AutodiffContext, GradientTape, GradientAccumulation), three for distributed work (ClusterContext, RdmaContext, Supervision), plus PrecisionMode, ComputeDevice and Benchmark. Declare your own only after checking that list.

Every other name you meet in these pages — IO, Http, Store, Network and friends — is a context the example declares for itself. They are illustrative, not provided: writing using [Http] without a context Http { ... } in scope is an error. Declaring one is a single line:

context Http {
    fn get(url: Text) -> Result<Response, HttpError>;
}

Note also that IO is a context name in these examples, not the computational property IO. Properties (Pure, IO, Async, Fallible, Mutates) are inferred by the compiler and never appear in a using clause.

Level 1: static @injectable

Compile-time dependency injection with zero runtime cost.

@injectable(Scope.Singleton)
type Logger is { level: LogLevel };

fn process(msg: Message) {
    let log: &Logger = inject Logger;
    log.info(f"processing {msg.id}");
}

The inject Logger expression is resolved at compile time. The compiler walks the injector graph, stitches together singleton / request / transient instances per scope, and hands process the already-built &Logger.

Level 2: dynamic provide / using

Runtime DI with ~5–30 ns overhead (task-local lookup).

type UserId is (Int);
type User is { id: UserId, name: Text };

// Your own sink. `core.base.log` gives you the `Logger` PROTOCOL and
// `LogLevel` — not a concrete logger, so this is yours to write.
type ConsoleLogger is { min_level: LogLevel };

implement ConsoleLogger {
    fn info(&self, message: Text)  { print(f"[info] {message}"); }
    fn error(&self, message: Text) { print(f"[error] {message}"); }
}

type InMemoryDb is { only: User };

implement InMemoryDb {
    fn query(&self, id: UserId) -> User { self.only }
}

public context Logger {
    fn info(message: Text);
    fn error(message: Text);
}

public context Database {
    fn query(id: UserId) -> User;
}

fn fetch_user(id: UserId) -> User using [Logger, Database] {
    Logger.info("fetching user");
    Database.query(id)
}

fn main() {
    let log = ConsoleLogger { min_level: LogLevel.Info };
    let db  = InMemoryDb { only: User { id: UserId(42), name: "ada" } };
    provide Logger = log;
    provide Database = db in {
        let u = fetch_user(UserId(42));
        print(f"user={u.name}");
    };
}

Run it and you get:

[info] fetching user
user=ada

caution

provide does not check that the provider implements the context

The dispatch above resolves Logger.info by METHOD NAME on whatever value was provided. Delete the implement ConsoleLogger block and the programme still compiles, still runs, and still prints user=ada — the log line simply disappears, with no diagnostic.

Compare the block above with the same source minus its implementation:

sed '/^implement ConsoleLogger {/,/^}$/d' with_impl.vr > without_impl.vr

verum run with_impl.vr        # [info] fetching user
                              # user=ada          exit 0
verum run without_impl.vr     # user=ada          exit 0

Both exit 0. The only difference a reader sees is a line of output that is not there, which is why this is a caution rather than a footnote: a rename or a typo in a provider's method removes the call instead of failing the build.

A neighbouring case has the same root — provide handed a record literal of the context itself aborts the compiler with an internal error instead of a diagnostic.

Three syntactic facts worth noting against the stdlib's own contexts in core/context/standard.vr:

• context declarations carry public (or no visibility prefix) — not pub, and they do not end with a semicolon. The body is enclosed in { … } like any other item.
• Context methods do not take &self. They're called statically as Logger.info(msg) — the runtime looks up the installed backend from the current task-local context stack.
• print is a built-in, so fn main() does not need using [...]. User-defined contexts (Logger, Database, Clock, Metrics, RateLimiter, ...) do appear there whenever the function depends on them.

The provide ... in { ... } scope injects the value. using [Logger, Database] declares the contexts the function needs. Within the provided scope, Logger.info(...) routes to the installed backend.

Choosing between the two

Use static @injectable	Use dynamic provide/using
Singleton / well-known backends	Request-scoped or runtime-selected
Zero-overhead required	Flexible late binding acceptable
Protocols with a single sensible instance	Protocols with multiple viable instances

You can mix them. A Database context might be dynamically provided per-request; a Metrics context might be a compile-time singleton.

Context clause syntax

fn f() using [A, B, C] { ... }           // required contexts
fn f() using [A, !IO] { ... }            // required A, forbidden IO
fn f() using [A if cfg.debug] { ... }    // conditional
fn f() using [A.readonly()] { ... }      // transformed capability
fn f() using [A as primary] { ... }      // aliased
fn f() using [db: Database] { ... }      // named (identifier binding)

The full grammar allows five kinds of item in a context list:

extended_context_item = negative_context       (* !Context          *)
                      | conditional_context    (* Context if cond   *)
                      | transformed_context    (* Context.transform()*)
                      | named_context          (* name: Context  OR  Context as alias *)
                      | simple_context ;       (* Context           *)

Negative contexts

!Ctx means "this function may not use Ctx, and neither may anything it calls." A function that declares using [!Ctx] and calls one whose using clause includes Ctx violates the contract, and the compiler says so:

Function 'caller' calls 'callee' which requires context 'Zlog',
but 'Zlog' is excluded via `using [!Zlog]` in 'caller'

What the compiler does with that

It is an error, and the build fails. [context] unresolved_policy in Verum.toml chooses the severity, and all four settings now differ:

unresolved_policy	exit	diagnostic	message
absent (default)	non-zero	error	shown
"error"	non-zero	error	shown
"warn"	0	none	shown
"allow"	0	none	silent

The exclusion also names a real context: using [!Databse] is error<E605>: undefined context, not a silent no-op, so a typo cannot read as a guarantee.

This is how Verum encodes "pure" code:

using Pure = [!IO, !State<_>, !Random];

fn sum(xs: &List<Int>) -> Int using Pure {
    xs.iter().sum()
}

Context groups

using WebRequest = [Database, Logger, Cache, Metrics, Clock];

fn handle(req: Request) -> Response using [WebRequest] { ... }

Groups are just named lists. They compose.

Transformed contexts

A using entry may call methods on the context, and the function body then sees the RESULT of those calls rather than the context as provided:

context Store {
    fn read(key: Text) -> Maybe<Text>;
    fn write(key: Text, value: Text);
    fn readonly() -> Store;
}

fn analyse() using [Store.readonly()] { ... }

Each segment is an ordinary method on the context, and that is literally how it lowers: the compiler fetches the provided context, calls the named method on it, and installs the result as the context for the body. Segments chain left to right:

fn audited() using [Store.readonly().traced()] { ... }

There is no fixed list of transform names — whatever the context declares can be used. What a transform means is therefore up to the context that declares it: readonly() above returns a Store whose write is a no-op or a panic, and the language does not enforce that promise for you.

The method IS checked — this caution was stale

Calling a method the context does not declare is refused at compile time with its own diagnostic:

context Store { fn read(url: Text) -> Text; }
fn f(k: Text) -> Text using [Store] { Store.nonexistent(k) }
  -> error<E606>: context `Store` has no method `nonexistent`

The same file with only the declared Store.read compiles clean, so the refusal is the check firing and not the example failing for another reason. The page previously said the opposite; it was written before E606 existed.

Named and aliased contexts

Two instances of the same context type require disambiguation — use as or a prefixed name:

// Using `as` — the alias is the symbol inside the function body:
fn replicate(data: &Record)
    using [Database as primary, Database as replica]
{
    primary.write(data);
    replica.write(data);
}

// Using `name: Context` — the name is the symbol:
fn handle(req: Request)
    using [db: Database, log: Logger]
{
    log.info(f"req {req}");
    db.query(...)
}

Both forms are equivalent. Inside the function, the alias (or name) is what you call methods on; the bare context type (Database) is not in scope when there are aliases.

Conditional contexts (feature flags)

fn maybe_log(msg: &Text)
    using [Logger,
           Analytics if cfg.analytics_enabled,
           Metrics if cfg.metrics_enabled]
{
    Logger.info(msg);
    if cfg.analytics_enabled { Analytics.track(msg); }
    if cfg.metrics_enabled   { Metrics.increment("msgs"); }
}

cfg.flag is a compile-time boolean from verum.toml features. Compiling with --features analytics enables the conditional capability; without it the context is neither required nor emitted.

The condition can also be:

• identifier — a compile-time constant.
• cfg.identifier — a build feature.
• platform.linux, platform.windows, etc. — target platform.
• T: Bound — a type-constraint condition.
• Any Boolean combination of these with &&, ||, !, (…).

Propagation across async boundaries

Context stacks are task-local. Async and structured concurrency preserve them:

• spawn clones the parent's context stack.
• .await preserves the stack across the suspension.
• for await in a generator preserves stacks per yield.
• nursery inherits stacks into child tasks.
• Channel send/recv does not propagate — channels are data pipes, not capability pipes.

async fn handle(req: Request) using [Database, Logger] {
    nursery {
        spawn background_task();     // inherits Database + Logger
        primary_flow(req).await
    }
}

Context protocols

A context protocol is both a protocol (types implement it) and a context (functions request it). This is the dual role that lets Logger appear in both implement Logger for Console {} and using [Logger].

context protocol Clock {
    fn now(&self) -> Instant;
    fn elapsed(&self, since: Instant) -> Duration {
        self.now() - since
    }
}

Meta contexts — the compile-time mirror

The context system extends to compile-time programming: meta fn functions declare their capabilities with the same using [...] syntax as runtime functions, but the contexts are compiler-provided and execute at compile time with zero runtime cost.

// Runtime context — provider explicit at the call site
fn handle(req: Request) -> Response
    using [Database, Logger, Clock] { ... }

// Meta context — provider is the compiler, implicit
meta fn derive_eq<T>() -> TokenStream
    using [TypeInfo, AstAccess, CompileDiag] { ... }

Fourteen meta-specific contexts ship with the language: BuildAssets, TypeInfo, AstAccess, CompileDiag, MetaRuntime, MacroState, CodeSearch, ProjectInfo, SourceMap, Schema, DepGraph, MetaBench, StageInfo, Hygiene. Composite groups like MetaCore = [TypeInfo, AstAccess, CompileDiag] mirror the using WebRequest = [...] pattern for runtime contexts. See stdlib → meta for the full API surface.

Where contexts are erased

Contexts provided statically (via @injectable with compile-time resolution, or provide in a monomorphic call graph) are entirely erased — the generated code calls the concrete function directly.

Dynamically provided contexts cost one pointer load from task-local storage per access (~5–30 ns).

What contexts are not: a deliberate alternative to algebraic effects

The Verum context system is capability-based dependency injection, not an algebraic-effect system. The distinction is a conscious design choice, and worth unpacking because the two mechanisms are often conflated.

The effect-system tradition

In languages like Koka, Effekt, Eff, Frank, and OCaml 5, every interaction with the outside world (logging, I/O, non-determinism, mutable state, exceptions) is modelled as an effect operation that a surrounding handler interprets. Handlers can resume the suspended computation with a value, abort it, run it many times (supporting non-deterministic search), or compose with other handlers to stack interpretations. This subsumes dependency injection, exception handling, coroutines, generators, transactional state, and logic programming in a single elegant mechanism.

// Koka — Logger as an algebraic effect
effect log { fun info(msg: string): () }

fun greet(name: string): log () {
  info("greeting " ++ name)   // this might suspend!
}

fun main() {
  with handler {
    fun info(msg) { println(msg); resume(()) }   // handler chooses what to do
  }
  greet("world")
}

Why Verum does not do this

Effect operations are not ordinary function calls. An operation can in principle capture its own continuation, so every call site must be compiled as if a stack-switch might happen. Koka's evidence-passing transform, Effekt's capability-passing style, and OCaml 5's fibre-based runtime all reduce this cost, but the price of the full-power effect machinery is paid even by operations that never actually resume.

The empirical observation that drove Verum's design: in real code, the overwhelming majority of "effectful" operations are plain dependency injection. "Give me a Logger." "Give me a Database." "Give me a Clock." Those calls do not want to capture their continuation. They want a vtable dispatch and a way to be mocked in tests.

The tradeoff Verum makes

Verum's context system meets that common case with a mechanism every systems programmer already understands:

Dimension	Algebraic effects (Koka, Effekt, OCaml 5)	Verum contexts (using [...])
Power	Handlers may resume, abort, multi-shot	Plain virtual dispatch; no resumption
Compilation	Evidence-passing / CPS / fibre stack-switch	Vtable dispatch against task-local storage
Cost per call	Tens of nanoseconds even for trivial ops	~5–30 ns dynamic, zero when monomorphised
Cost model	Every effectful op may suspend	Function-call cost, independent of op count
Testing	Swap the handler	Swap the provider (provide X = mock)
Async interaction	Effects subsume async	Async orthogonal to contexts, compose cleanly
Mental model	Learn handler algebra / free monads	"It's DI with a language-level syntax"

For the 5 % of cases where reinterpretation is the point — non-deterministic search, probabilistic programming, backtracking parsers, proof search — Verum offers metaprogramming, tactic combinators, and explicit continuations (async/await, coroutine-style generators). None of those impose a runtime cost on every function in the program.

What this means in practice

• A Logger.info call is a vtable dispatch, not a suspension point.
• Context providers compose by lexical scoping, not by stacked handlers.
• Adding a context to a function's signature does not change its ABI beyond adding a capability requirement; the generated code path is the same shape.
• Compile-time and runtime DI share one surface — using [...] for both. Effect systems do not unify compile-time meta with runtime DI in this way.

If you are coming from Koka or OCaml 5, the mental adjustment is: Verum's contexts do less by design. You lose resume. You gain a cost model that stays flat as your program grows, the ability to hand a context stack to a spawn and have it just work, and the full algebra of dependency injection without any of the framework ceremony that languages without a language-level DI mechanism have to layer on top.

Grammar

From the grammar reference:

context_clause   = 'using' , context_spec ;
context_spec     = single_context_spec | extended_context_list ;
single_context_spec
                 = [ '!' ] , context_path , [ context_alias ] , [ context_condition ] ;
extended_context_list
                 = '[' , extended_context_item , { ',' , extended_context_item } , ']' ;

extended_context_item = negative_context
                      | conditional_context
                      | transformed_context
                      | named_context
                      | simple_context ;

context_group_def = 'using' , identifier , '=' , context_list_def , ';' ;
provide_stmt    = 'provide' , ( provide_layer | provide_single | provide_multi ) ;

Worked example — wiring a web service

A typical top-level entry point layers every context once. This one is a SHAPE, not a programme you can paste: ConsoleLogger, PrometheusMetrics, HttpServer, Request/Response and ok_response are yours to supply — core provides PgConfig, PgAdapter, SystemClock and LogLevel, and nothing else here.

fn main() {
    let pg_config = PgConfig.new("localhost", 5432, "app", "", "app");
    provide Logger   = ConsoleLogger.new(LogLevel.Info),
            Clock    = SystemClock.new(),
            Database = PgAdapter.connect(&pg_config),
            Metrics  = PrometheusMetrics.new()
    {
        let mut server = HttpServer.bind(&":8080").await?;
        server.serve(|req| handle(req)).await?;
    }
}

async fn handle(req: Request) -> Response
    using [Database, Logger, Clock, Metrics]
{
    let now = Clock.now();
    Logger.info(&f"req {req.path} at {now}");
    Metrics.increment("requests.total");
    ok_response(&Database.find_user(req.auth)?)
}

The multi-provide form takes comma-separated bindings and a MANDATORY block — the bindings are in scope for the block and nothing else. A single binding may use provide X = v; to run to the end of the enclosing scope, or provide X = v { ... }.

The handle function declares every capability it needs in its signature, and Clock.now() inside a function that did NOT declare [Clock] is refused — error<E801>: context 'Clock' used but not declared in function signature.

The obligation travels. Calling handle(req) from a function that declares no contexts is refused:

fn caller() { handle(req); }
// error<E801>: context `Database` used but not declared in
//              function signature

Declaring a different context does not satisfy it either — the check compares names, not the presence of a using clause. So a requirement cannot be lost by wrapping the call in a function, which is what "no hidden state" has to mean for it to be worth anything.

Tests swap in a mock:

@test
async fn test_handler() {
    // Several contexts at once: comma-separated bindings, ONE block.
    // `in` scopes a SINGLE binding and does not chain.
    provide Database = MockDatabase.new(),
            Logger   = NullLogger.new(),
            Clock    = FakeClock.at(epoch()),
            Metrics  = NullMetrics.new() {
        let req = Request.get("/users/42");
        let resp = handle(req).await;
        assert_eq(resp.status.code(), 200);
    }
}

Which of those four ships, and which you write

core/ ships the CONTEXTS — Logger, Clock, Database, Metrics and 29 others are declared in core/context/standard.vr — and exactly one of the doubles above: NullLogger (core/base/log.vr:535). The other three are yours, and that is the design rather than a gap: a double is written against your schema, not the library's.

// The three the example swaps in are declared by the test, not by core.
type MockDatabase is {};
type FakeClock is { at: Instant };
type NullMetrics is {};

No mocking framework. No DI container. Contexts are just types; provide is just assignment; the compiler does the rest.

Full build in HTTP service tutorial.

See also

• Stdlib → context — the Provider, Scope, and ContextError types.
• Async and concurrency — how contexts flow across tasks.
• Architecture → execution environment (θ+) — how context interacts with memory / recovery / concurrency.
• Architecture → runtime tiers — how the runtime implements task-local storage.
• HTTP service tutorial — end-to-end use of Layer.new().with_...(...).
• Cookbook → shared state — when a Mutex-wrapped context is the right shape.