Dispatch

The central question

Given:

• A candidate p (a registered capability)
• A request r (what the caller wants)

The dispatch question is:

Can candidate p serve request r?

The two are not the same kind of thing. A candidate is a cap: a thing in the fabric that takes this, gives that, and has these tags. A request is a question about caps, and a question may leave a side unasked:

• “Something that gives me this file. I do not know yet what it will take.”
• “What can this input be turned into?”
• “What are the choices for the step in between?”

So a request is read as a query, and dispatch is a query admitting a cap. The predicate is kind-agnostic: the CapKind classification is a description of the result and appears nowhere in the rule.

The model is capdag/formal (Lean); every implementation runs code generated from it. Names in code below are its definitions and theorems.

Queries

What a query asks of one side

A Query asks something of the input, something of the output, a cap-tag pattern, and an effect. Query.admits q c holds when each is met, the cap’s own cap-tags being read complete (Predicates: complete things):

admits(q, c)  ⟺  q.input admits c.in  ∧  q.output admits c.out
               ∧  (q.effect = ? ∨ c.effect = q.effect)
               ∧  c.y satisfies q.tags

Unknown is not “anything”

media: is a type, the top of the media order, “anything”. A candidate whose input is media: takes anything: a claim about every input.

An unasked side claims nothing. It is an unknown: satisfied by some value, not required of all. A query whose input is unknown admits exactly the caps that some typed query (the same, with an input stated) admits (unknown_input_is_exists):

admits(⟨unknown, o, y, e⟩, c)  ⟺  ∃ i. admits(⟨covers i, o, y, e⟩, c)

That is the existential lifting of a typed judgment over what an unknown could be. It is derived from the typed rule, not added to it.

The readings of a cap URN

A cap URN is read in the role it plays:

“Open” means the side constrains nothing: omitted, media:, or anything equivalent to it (unconstrainedMedia). An open output in a request already asks nothing, because every output is within media:, so only the input needed saying.

Questions no cap URN can spell are queries built directly:

The dispatch predicate

Definition

serves(p, r) is Query.ofRequest(r) admitting p. Spelled out (serves_iff), with p = (i_p, o_p, y_p, e_p) and r = (i_r, o_r, y_r, e_r):

Dispatch(p, r)  ⟺  (i_r open ∨ i_r ⪯ i_p)  ∧  o_p ⪯ o_r  ∧  (e_r = ? ∨ e_p = e_r)  ∧  y_p satisfies y_r

The four conjuncts

Input (contravariant)

Request:  in="media:bytes;document;ext=pdf"     (specific)
Candidate: in="media:bytes"            (more general)

i_r ⪯ i_p?  pdf;bytes refines bytes  →  PASS ✓

A candidate that takes media:bytes serves a request that sends media:bytes;document;ext=pdf.

Output (covariant)

Request:  out="media:record"               (what is needed)
Candidate: out="media:fmt=json;record"     (a stronger guarantee)

o_p ⪯ o_r?  fmt=json;record refines record  →  PASS ✓

A candidate that promises only “some ext” does not serve a request that needs ext=pdf: media:ext ⪯ media:document;ext=pdf is false. It could serve it (Could serve, and grades).

Cap-tags

The request’s tags are a pattern; the candidate’s are the tags it has.

Dispatch is not symmetric

Dispatch(p, r) does not imply Dispatch(r, p). A request that sends media:model-spec is served by a candidate that takes media:bytes (a model-spec is bytes); a request that sends media:bytes is not served by a candidate that takes only media:model-spec.

Could serve, and grades

serves is a guarantee. The other question is whether the candidate could be what is asked, and it replaces every bound with overlap (Predicates: the possibility):

mayAdmit(q, c)  ⟺  each asked side of c MEETS what is asked,
                    the effect matches, and c.y may satisfy q.tags

A cap answers a query with a grade (Query.grade):

producing(media:ext=jpeg;image)  against  out="media:ext=jpeg;image"  →  exact
producing(media:image)           against  out="media:ext=jpeg;image"  →  guaranteed
producing(media:ext=jpeg;image)  against  out="media:image"           →  possible
producing(media:ext=jpeg;image)  against  out="media:enc=utf-8"       →  none

Whatever is guaranteed is possible (Query.admits_mayAdmit). Exploring the fabric shows possible; a call is never routed on it.

Examples

A request that leaves its sides open

Request:  cap:download-model
Candidate: cap:in="media:model-spec";download-model;out="media:download-result"

Input:  the request's input is open → not established → PASS ✓
Output: o_p ⪯ media:  → PASS ✓
Tags:   the candidate has download-model → PASS ✓

Result: SERVES ✓

A candidate that promises no particular output

Request:  cap:in="media:document;ext=pdf";extract;out="media:record"
Candidate: cap:in="media:bytes";extract

Input:  pdf ⪯ bytes → PASS ✓
Output: media: ⪯ media:record?  No: top is not more specific → FAIL ✗

Result: DOES NOT SERVE

Incompatible types

Request:  cap:in="media:document;ext=pdf";convert;out="media:ext=html"
Candidate: cap:in="media:image";convert;out="media:enc=utf-8"

Input:  pdf ⪯ image?  No → FAIL ✗

Result: DOES NOT SERVE

A request for the absence of a tag

Request:  cap:!constrained;generate-json
Candidate A: cap:generate-json;in=…;out=…               → SERVES ✓  (it has no such tag)
Candidate B: cap:constrained;generate-json;in=…;out=…   → DOES NOT ✗ (it has it)

Properties

What composes

Reading a request as a query does not make serves a relation between two caps with a composition law, and it is not one: a pdf-only candidate serves a request whose input is open; that request, read as a candidate, serves an image request; and the pdf-only candidate does not serve the image request.

The laws are where the structure is:

• A narrower question has fewer answers (Query.narrower_trans): whatever answers q₁ answers q₂, and whatever answers q₂ answers q₃, so whatever answers q₁ answers q₃.
• Establishing an unknown narrows (ofCall_narrower_ofRequest): every typed call a request could become asks for at least what the request asks for.
• Between typed calls, “can stand in for” is “asks for no less” (capRefines_narrower). capRefines a b is the typed relation between two caps as descriptions (arrow subtyping): i_b ⪯ i_a ∧ o_a ⪯ o_b ∧ … ∧ y_a ⪯ y_b. It is reflexive and transitive (capRefines_refl, capRefines_trans), and a cap that can stand in for a request serves it (capRefines_serves).

Monotonicity

Making a candidate better in the right directions (broader input, narrower output) never stops it standing in (capRefines_monotone).

Selection

Among the candidates that serve, ranking chooses (Ranking); what it returns serves the request, something is returned whenever anything serves, and nothing that serves ranks strictly better (select_sound, select_complete, select_optimal).

Implementation

impl CapUrn {
    /// Does this candidate SERVE the request?  — routing
    pub fn is_dispatchable(&self, request: &CapUrn) -> bool;
    /// COULD it?  — exploring, never routing
    pub fn may_dispatch(&self, request: &CapUrn) -> bool;
    /// Does `cap` fit this cap read as a PATTERN?  — searching
    pub fn accepts(&self, cap: &CapUrn) -> bool;
    /// Are the two the SAME cap?  — resolving a name
    pub fn is_equivalent(&self, other: &CapUrn) -> bool;
    /// Does what this cap gives, `next` take?  — a route's edge
    pub fn flows_into(&self, next: &CapUrn) -> bool;
    pub fn may_flow_into(&self, next: &CapUrn) -> bool;
}

impl CapQuery {
    pub fn from_request(request: &CapUrn) -> Self;
    pub fn from_pattern(pattern: &CapUrn) -> Self;
    pub fn producing(output: &MediaUrn, tags: &BTreeMap<String, String>) -> Self;
    pub fn consuming(input: &MediaUrn, tags: &BTreeMap<String, String>) -> Self;
    pub fn between(input: &MediaUrn, output: &MediaUrn, tags: &BTreeMap<String, String>) -> Self;
    pub fn admits(&self, cap: &CapUrn) -> bool;
    pub fn may_admit(&self, cap: &CapUrn) -> bool;
    pub fn grade(&self, cap: &CapUrn) -> MatchGrade;   // Exact | Guaranteed | Possible | None
}

candidate.is_dispatchable(request) is CapQuery::from_request(request).admits(candidate), and pattern.accepts(cap) is CapQuery::from_pattern(pattern).admits(cap). Every mirror (Rust, Go, Python, JavaScript, Objective-C/Swift) has the same surface and is held to the model by the same table (formal/conformance.json).

Common mistakes

Using accepts for dispatch

if candidate.accepts(&request) { /* dispatch */ }   // WRONG

accepts is the pattern reading: its input and output run the other way and its open side is the output. A cartridge’s cap with a tag the request did not mention is “not accepted”, and a candidate with a broader input is refused.

Using is_equivalent for dispatch, or dispatch for resolution

See Resolution vs. dispatch.

Routing on a possibility

if candidate.may_dispatch(&request) { /* dispatch */ }   // WRONG

Checking only one axis

if candidate.op == request.op { /* dispatch */ }   // WRONG

All four coordinates must be checked.

Resolution vs. dispatch: which predicate?

Dispatch is not the only cap-matching question the system asks. There are three, and they use three predicates on purpose:

Why alias resolution uses is_equivalent, not dispatch

When you run capdag <alias> …, the alias is resolved in the fabric registry to exactly one concrete cap URN, a fully-specified point and not a pattern. The next step is to find the cartridge that implements that cap: a resolution question (“which cartridge declares this cap?”), not a dispatch question (“which cartridge could serve this?”).

The same CLI also exposes inspection and visualization surfaces around this resolution: capdag resolve <alias> [--no-cache] prints a cap’s resolved definition (with --no-cache bypassing a version-keyed fabric cache that a staging re-publish can leave stale), capdag cache clear|refresh invalidates or renews that cache, and capdag dag-viz <alias> --mermaid|--dot renders the full MachinePlan (steps and their outputs, maps, gathers, inputs and outputs, and typed edges).

Alias resolution matches with the symmetric is_equivalent (both caps read as descriptions, nothing unknown, equivalent on every side, equivalent_axiswise) because:

• Determinism / least surprise. The alias names one specific cap. The user gets a cartridge that provides that cap, never a more specific or more general one that merely could serve the request.
• No accidental widening. Resolution must not “fall back” to a looser candidate; if nothing implements the exact resolved cap, that is a real “no candidate” answer the caller needs to see (and fix by publishing the right cartridge), not something to paper over by dispatching to a near-match. A cap that promises no particular output is not the same cap as one that promises pages, although as a pattern it fits it.

Equivalence is decided on the parsed in/out/effect coordinates, never by string equality, since two semantically identical cap URNs can serialize differently (tag order, the arbitrary op marker), so matching walks the parsed predicate, and resolution never prefilters through a string-keyed index (which would drop equivalent-but-differently-serialized candidates before equivalence is tested).

Where each is used

• Resolution (is_equivalent): CartridgeRepo::get_suggestions_for_cap and the dev-cartridge lookup in CartridgeManager::find_cartridge_binary. These two are the same run-path question and MUST use the same predicate.
• Find-anything / dispatch (is_dispatchable): get_cartridges_by_cap (enumerate every capable cartridge), Cap::accepts_request, and the planner/router dispatch sites, in every mirror.
• Search (accepts / CapQuery): cap URN completion.

Rule of thumb: resolving a name → is_equivalent; asking “who can serve this?” → is_dispatchable; asking “what is there like this?” → a query. Never mix them within one question.

Abstract caps: resolve the umbrella, then dispatch to a concrete cap

An abstract cap is a dispatch umbrella over caps that differ only by format, for example cap:disbind;in=media:document;out="media:enc=utf-8;ext=txt;page;plain-text" or cap:convert-image;in=media:image;out=media:image. It is a valid alias target but is never backed by a cartridge and is excluded from the runnable cap graph (LiveMachinePlanGraph::add_cap skips it), so it can never appear as an edge the wizard or planner would offer and then fail to execute.

An abstract cap says what its specializations have in common. Every converter under convert-image takes an image and makes one, so the umbrella is image → image, not media: → media:: a cap whose input is media: has made a claim about every type. The supertypes come from the medium dim — media:image, media:audio, media:video, media:document — and every per-format type conforms to its medium (media:ext=png;image is a media:image). Where the specializations share no medium on a side (page rendering takes a document or a text file), that side stays as wide as they are. The registry enforces this at publish: an umbrella declared wider than the medium all of its specializations share is not published.

Read as a request, an abstract cap is served by every concrete specialization, which is what makes it an umbrella.

Running capdag <abstract-alias> <file> uses both predicates, in order:

1. Resolve the alias to the abstract cap URN with is_equivalent (which cap does this name mean?).
2. Dispatch to a concrete cap with is_dispatchable. The CLI detects the input file’s media type, builds the request = the abstract cap with its input established as that media (and its output as --to <target> when given), and asks FabricRegistry::narrow_abstract_cap: which concrete (non-abstract) cap URN serves that request? Exactly one → run it; zero → “no handler for this input”; more than one → ambiguous (the caller disambiguates with --to, or by naming the concrete alias).

Narrowing adds no rule of its own. A text file given to convert-image is refused because no image converter is dispatchable for a text input — the same is_dispatchable that picks the converter for a JPEG — and the refusal prints the umbrella’s URN, which carries the type it declares: no concrete cap specializes 'cap:convert-image;in=media:image;out=media:image' for input 'media:enc=utf-8;ext=txt'.

Every abstract cap must have ≥1 concrete specialization in the same snapshot (enforced at publish), so the narrowing can always reach a real cartridge. The abstract caps the fabric defines are convert-image, convert-audio, disbind, extract-frames and extract-audio-track.

Routes

Types are the objects; one refines another when everything it is, the other is. Caps are the arrows between them. A route from A to B is a chain of caps a thing of type A can be carried along to become a thing of type B (Route):

flows(c₁, c₂)    ⟺  c₁.out ⪯ c₂.in       what c₁ gives, c₂ takes — guaranteed
mayFlow(c₁, c₂)  ⟺  c₁.out meets c₂.in   it could — to explore, and to check when run

An empty route is a refinement (nothing to run), so routes have identities (Route.id), compose (Route.append), and still work from anything narrower to anything wider (Route.retype). That is the category the fabric is navigated in; a planner’s path is a route, and its soundness is those three facts.

Why a request is not a cap

Dispatch is not a relation between two caps. A relation between two caps that reads a request dimension set to media: as unconstrained cannot also be transitive. Keeping transitivity means dropping the clause: a request that leaves its input open would then be served only by a candidate that takes everything, and asking the fabric “what gives me this?” would find nothing. What is matched is not two caps:

• A query is matched against a library by one relation per part of the specification, any of which may be dropped (Zaremski & Wing, Specification Matching of Software Components, TOSEM 1997, Def. 2). Their plug-in match is the typed call; their plug-in post match, the precondition dropped, is a request whose input is unknown.
• A description with an unknown part means the set of things it could be, and holds of a predicate when some member does (Garcia, Clark & Tanter, Abstracting Gradual Typing, POPL 2016, Def. 3). The unknown is not the top type: treating it as one is the conflation of an existential with a universal that makes such relations non-transitive.
• The transitive law belongs to making a description more precise, a preorder beside subtyping (Castagna, Lanvin, Petrucciani & Siek, Gradual Typing: A New Perspective, POPL 2019, §2.1 “materialization”).
• “Some” and “all” are the two adjoints of the same operation (Lawvere, Adjointness in Foundations, 1969).

Summary

Dispatch(p, r)  ⟺  (i_r open ∨ i_r ⪯ i_p)  ∧  o_p ⪯ o_r  ∧  (e_r = ? ∨ e_p = e_r)  ∧  y_p satisfies y_r

This is the primary predicate for routing. Ranking (next document) applies only after a candidate is known to serve.