Dispatch

La domanda centrale

Dati:

• Un candidato p (una capacità registrata)
• Una richiesta r (ciò che vuole il chiamante)

La domanda del dispatch è:

Il candidato p può servire la richiesta r?

I due non sono dello stesso genere. Un candidato è una cap: una cosa nel fabric che prende questo, dà quello e ha questi tag. Una richiesta è una domanda sulle cap, e una domanda può lasciare un lato senza chiedere nulla:

• “Qualcosa che mi dia questo file. Non so ancora che cosa prenderà.”
• “In che cosa si può trasformare questo input?”
• “Quali sono le scelte per il passo intermedio?”

Perciò una richiesta viene letta come una query, e il dispatch è una query che ammette una cap. Il predicato è indipendente dal tipo: la classificazione CapKind è una descrizione del risultato e non compare in nessun punto della regola.

Il modello è capdag/formal (Lean); ogni implementazione esegue codice generato a partire da esso. I nomi in code qui sotto sono le sue definizioni e i suoi teoremi.

Query

Che cosa chiede una query a un lato

Una Query chiede qualcosa dell’input, qualcosa dell’output, un pattern di cap-tag e un effetto. Query.admits q c vale quando ciascuno è soddisfatto, con i cap-tag propri della cap letti come completi (Predicati: cose complete):

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

Sconosciuto non significa “qualsiasi cosa”

media: è un tipo, la cima dell’ordine dei media, “qualsiasi cosa”. Un candidato il cui input è media: prende qualsiasi cosa: un’affermazione su ogni input.

Un lato su cui non si chiede nulla non afferma nulla. È uno sconosciuto: soddisfatto da qualche valore, non richiesto a tutti. Una query il cui input è sconosciuto ammette esattamente le cap che una qualche query tipizzata (la stessa, con un input dichiarato) ammette (unknown_input_is_exists):

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

Questo è il sollevamento esistenziale di un giudizio tipizzato su ciò che uno sconosciuto potrebbe essere. È derivato dalla regola tipizzata, non aggiunto a essa.

Le letture di un cap URN

Un cap URN viene letto nel ruolo che svolge:

“Aperto” significa che il lato non vincola nulla: omesso, media: o qualunque cosa equivalente a esso (unconstrainedMedia). Un output aperto in una richiesta già non chiede nulla, perché ogni output è entro media:, quindi andava detto soltanto per l’input.

Le domande che nessun cap URN sa esprimere sono query costruite direttamente:

Il predicato di dispatch

Definizione

serves(p, r) è Query.ofRequest(r) che ammette p. Per esteso (serves_iff), con p = (i_p, o_p, y_p, e_p) e 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

Le quattro congiunzioni

Input (controvariante)

Richiesta: in="media:bytes;document;ext=pdf"    (specifica)
Candidato: in="media:bytes"            (più generale)

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

Un candidato che prende media:bytes serve una richiesta che invia media:bytes;document;ext=pdf.

Output (covariante)

Richiesta: out="media:record"              (ciò che serve)
Candidato: out="media:fmt=json;record"     (una garanzia più forte)

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

Un candidato che promette soltanto “qualche ext” non serve una richiesta che ha bisogno di ext=pdf: media:ext ⪯ media:document;ext=pdf è falso. Potrebbe servirla (Potrebbe servire, e gradi).

Cap-tag

I tag della richiesta sono un pattern; quelli del candidato sono i tag che ha.

Il dispatch non è simmetrico

Dispatch(p, r) non implica Dispatch(r, p). Una richiesta che invia media:model-spec è servita da un candidato che prende media:bytes (un model-spec è fatto di byte); una richiesta che invia media:bytes non è servita da un candidato che prende soltanto media:model-spec.

Potrebbe servire, e gradi

serves è una garanzia. L’altra domanda è se il candidato potrebbe essere ciò che viene chiesto, e sostituisce ogni limite con la sovrapposizione (Predicati: la possibilità):

mayAdmit(q, c)  ⟺  ogni lato richiesto di c si incontra (MEETS) con ciò che è richiesto,
                    l'effetto corrisponde e c.y può soddisfare q.tags

Una cap risponde a una query con un grado (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

Tutto ciò che è garantito è possibile (Query.admits_mayAdmit). L’esplorazione del fabric mostra possible; una chiamata non viene mai instradata su di esso.

Esempi

Una richiesta che lascia aperti i suoi lati

Richiesta: cap:download-model
Candidato: cap:in="media:model-spec";download-model;out="media:download-result"

Input:  l'input della richiesta è aperto → non stabilito → PASS ✓
Output: o_p ⪯ media:  → PASS ✓
Tag:    il candidato ha download-model → PASS ✓

Risultato: SERVE ✓

Un candidato che non promette alcun output particolare

Richiesta: cap:in="media:document;ext=pdf";extract;out="media:record"
Candidato: cap:in="media:bytes";extract

Input:  pdf ⪯ bytes → PASS ✓
Output: media: ⪯ media:record?  No: il top non è più specifico → FAIL ✗

Risultato: NON SERVE

Tipi incompatibili

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

Input:  pdf ⪯ image?  No → FAIL ✗

Risultato: NON SERVE

Una richiesta per l’assenza di un tag

Richiesta: cap:!constrained;generate-json
Candidato A: cap:generate-json;in=…;out=…               → SERVE ✓      (non ha quel tag)
Candidato B: cap:constrained;generate-json;in=…;out=…   → NON SERVE ✗  (ce l'ha)

Proprietà

Che cosa si compone

Leggere una richiesta come una query non fa di serves una relazione fra due cap con una legge di composizione, e infatti non lo è: un candidato solo-pdf serve una richiesta il cui input è aperto; quella richiesta, letta come candidato, serve una richiesta di immagine; e il candidato solo-pdf non serve la richiesta di immagine.

Le leggi stanno dove sta la struttura:

• Una domanda più stretta ha meno risposte (Query.narrower_trans): tutto ciò che risponde a q₁ risponde a q₂, e tutto ciò che risponde a q₂ risponde a q₃, quindi tutto ciò che risponde a q₁ risponde a q₃.
• Stabilire uno sconosciuto restringe (ofCall_narrower_ofRequest): ogni chiamata tipizzata in cui una richiesta potrebbe trasformarsi chiede almeno ciò che chiede la richiesta.
• Fra chiamate tipizzate, “può fare le veci di” equivale a “non chiede di meno” (capRefines_narrower). capRefines a b è la relazione tipizzata fra due cap intese come descrizioni (sottotipizzazione delle frecce): i_b ⪯ i_a ∧ o_a ⪯ o_b ∧ … ∧ y_a ⪯ y_b. È riflessiva e transitiva (capRefines_refl, capRefines_trans), e una cap che può fare le veci di una richiesta la serve (capRefines_serves).

Monotonia

Migliorare un candidato nelle direzioni giuste (input più ampio, output più stretto) non gli impedisce mai di fare le veci (capRefines_monotone).

Selezione

Fra i candidati che servono, sceglie il ranking (Ranking); ciò che restituisce serve la richiesta, qualcosa viene restituito ogni volta che qualcosa serve, e nulla di ciò che serve si classifica strettamente meglio (select_sound, select_complete, select_optimal).

Implementazione

impl CapUrn {
    /// Questo candidato SERVE la richiesta?  — instradamento
    pub fn is_dispatchable(&self, request: &CapUrn) -> bool;
    /// POTREBBE servirla?  — esplorazione, mai instradamento
    pub fn may_dispatch(&self, request: &CapUrn) -> bool;
    /// `cap` corrisponde a questa cap letta come PATTERN?  — ricerca
    pub fn accepts(&self, cap: &CapUrn) -> bool;
    /// Le due sono la STESSA cap?  — risoluzione di un nome
    pub fn is_equivalent(&self, other: &CapUrn) -> bool;
    /// Ciò che questa cap dà, `next` lo prende?  — l'arco di un percorso
    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) è CapQuery::from_request(request).admits(candidate), e pattern.accepts(cap) è CapQuery::from_pattern(pattern).admits(cap). Ogni mirror (Rust, Go, Python, JavaScript, Objective-C/Swift) ha la stessa superficie ed è vincolato al modello dalla stessa tabella (formal/conformance.json).

Errori comuni

Usare accepts per il dispatch

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

accepts è la lettura come pattern: il suo input e il suo output vanno nel verso opposto e il suo lato aperto è l’output. La cap di una cartuccia con un tag che la richiesta non menzionava risulta “non accettata”, e un candidato con un input più ampio viene rifiutato.

Usare is_equivalent per il dispatch, o il dispatch per la risoluzione

Vedi Risoluzione e dispatch.

Instradare su una possibilità

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

Controllare un solo asse

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

Tutte e quattro le coordinate devono essere controllate.

Risoluzione e dispatch: quale predicato?

Il dispatch non è l’unica domanda di corrispondenza fra cap che il sistema pone. Ce ne sono tre, e usano di proposito tre predicati:

Perché la risoluzione degli alias usa is_equivalent e non il dispatch

Quando esegui capdag <alias> …, l’alias viene risolto nel registro del fabric in esattamente un cap URN concreto, un punto completamente specificato e non un pattern. Il passo successivo è trovare la cartuccia che implementa quella cap: una domanda di risoluzione (“quale cartuccia dichiara questa cap?”), non una domanda di dispatch (“quale cartuccia potrebbe servire questa richiesta?”).

La stessa CLI espone anche superfici di ispezione e visualizzazione attorno a questa risoluzione: capdag resolve <alias> [--no-cache] stampa la definizione risolta di una cap (con --no-cache che scavalca una cache del fabric indicizzata per versione, che una ripubblicazione in staging può lasciare obsoleta), capdag cache clear|refresh invalida o rinnova quella cache, e capdag dag-viz <alias> --mermaid|--dot disegna l’intero MachinePlan (i passi e i loro output, mappe, raccolte, input e output, e archi tipizzati).

La risoluzione degli alias effettua la corrispondenza con l’is_equivalent simmetrico (entrambe le cap lette come descrizioni, nulla di sconosciuto, equivalenti su ogni lato, equivalent_axiswise) perché:

• Determinismo / minima sorpresa. L’alias nomina una cap specifica. L’utente ottiene una cartuccia che fornisce quella cap, mai una più specifica o più generale che semplicemente potrebbe servire la richiesta.
• Nessun allargamento accidentale. La risoluzione non deve “ripiegare” su un candidato più lasco; se nulla implementa esattamente la cap risolta, quella è una vera risposta “nessun candidato” che il chiamante deve vedere (e correggere pubblicando la cartuccia giusta), non qualcosa da mascherare facendo il dispatch verso una corrispondenza approssimativa. Una cap che non promette alcun output particolare non è la stessa cap di una che promette pagine, anche se come pattern le corrisponde.

L’equivalenza viene decisa sulle coordinate in/out/effetto analizzate, mai per uguaglianza di stringhe, poiché due cap URN semanticamente identici possono essere serializzati in modo diverso (ordine dei tag, il marcatore arbitrario op); perciò la corrispondenza percorre il predicato analizzato, e la risoluzione non prefiltra mai tramite un indice basato su stringhe (che scarterebbe candidati equivalenti ma serializzati diversamente prima che l’equivalenza venga verificata).

Dove si usa ciascuno

• Risoluzione (is_equivalent): CartridgeRepo::get_suggestions_for_cap e la ricerca delle cartucce di sviluppo in CartridgeManager::find_cartridge_binary. Queste due sono la stessa domanda del percorso di esecuzione e DEVONO usare lo stesso predicato.
• Trova-qualsiasi-cosa / dispatch (is_dispatchable): get_cartridges_by_cap (enumera ogni cartuccia capace), Cap::accepts_request e i punti di dispatch del planner/router, in ogni mirror.
• Ricerca (accepts / CapQuery): completamento dei cap URN.

Regola pratica: risolvere un nome → is_equivalent; chiedere “chi può servire questo?” → is_dispatchable; chiedere “che cosa c’è di simile a questo?” → una query. Non mescolarli mai all’interno di una stessa domanda.

Cap astratte: risolvi l’ombrello, poi fai il dispatch verso una cap concreta

Una cap astratta è un ombrello di dispatch su cap che differiscono solo per il formato, per esempio cap:disbind;in=media:document;out="media:enc=utf-8;ext=txt;page;plain-text" o cap:convert-image;in=media:image;out=media:image. È una destinazione di alias valida ma non è mai supportata da una cartuccia ed è esclusa dal grafo delle cap eseguibili (LiveMachinePlanGraph::add_cap la salta), quindi non può mai comparire come un arco che il wizard o il planner offrirebbero e poi non riuscirebbero a eseguire.

Una cap astratta dice che cosa hanno in comune le sue specializzazioni. Ogni convertitore sotto convert-image prende un’immagine e ne produce una, quindi l’ombrello è immagine → immagine, non media: → media:: una cap il cui input è media: ha fatto un’affermazione su ogni tipo. I supertipi vengono dalla dimensione medium — media:image, media:audio, media:video, media:document — e ogni tipo di un formato è conforme al suo medium (media:ext=png;image è un media:image). Dove le specializzazioni non condividono alcun medium su un lato (il rendering delle pagine prende un documento o un file di testo), quel lato resta largo quanto loro. Il registro lo impone alla pubblicazione: un ombrello dichiarato più largo del medium che tutte le sue specializzazioni condividono non viene pubblicato.

Letta come richiesta, una cap astratta è servita da ogni specializzazione concreta, ed è questo che ne fa un ombrello.

Eseguire capdag <abstract-alias> <file> usa entrambi i predicati, in ordine:

1. Risolvi l’alias nel cap URN astratto con is_equivalent (quale cap indica questo nome?).
2. Fai il dispatch verso una cap concreta con is_dispatchable. La CLI rileva il tipo di media del file di input, costruisce la richiesta = la cap astratta con il suo input stabilito come quel media (e il suo output come --to <target> quando indicato), e chiede a FabricRegistry::narrow_abstract_cap: quale cap URN concreto (non astratto) serve quella richiesta? Esattamente uno → lo esegue; zero → “no handler for this input”; più di uno → ambiguo (il chiamante disambigua con --to, oppure nominando l’alias concreto).

Il restringimento non aggiunge alcuna regola propria. Un file di testo dato a convert-image viene rifiutato perché nessun convertitore di immagini può fare il dispatch di un input di testo — lo stesso is_dispatchable che sceglie il convertitore per un JPEG — e il rifiuto stampa l’URN dell’ombrello, che porta il tipo che dichiara: no concrete cap specializes 'cap:convert-image;in=media:image;out=media:image' for input 'media:enc=utf-8;ext=txt'.

Ogni cap astratta deve avere ≥1 specializzazione concreta nella stessa istantanea (imposto alla pubblicazione), così il restringimento può sempre raggiungere una cartuccia reale. Le cap astratte che il fabric definisce sono convert-image, convert-audio, disbind, extract-frames e extract-audio-track.

Percorsi

I tipi sono gli oggetti; uno raffina un altro quando tutto ciò che è il primo, lo è anche il secondo. Le cap sono le frecce fra di essi. Un percorso da A a B è una catena di cap lungo cui una cosa di tipo A può essere portata per diventare una cosa di tipo 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

Un percorso vuoto è un raffinamento (non c’è nulla da eseguire), quindi i percorsi hanno identità (Route.id), si compongono (Route.append) e funzionano ancora da qualunque cosa più stretta a qualunque cosa più ampia (Route.retype). Questa è la categoria in cui si naviga il fabric; il cammino di un planner è un percorso, e la sua correttezza sta in questi tre fatti.

Perché una richiesta non è una cap

Il dispatch non è una relazione fra due cap. Una relazione fra due cap che legge come non vincolata una dimensione della richiesta impostata a media: non può essere anche transitiva. Mantenere la transitività significa eliminare la clausola: una richiesta che lascia aperto il suo input sarebbe allora servita soltanto da un candidato che prende tutto, e chiedere al fabric “che cosa mi dà questo?” non troverebbe nulla. Ciò che viene messo in corrispondenza non sono due cap:

• Una query viene confrontata con una libreria tramite una relazione per ciascuna parte della specifica, ognuna delle quali può essere eliminata (Zaremski & Wing, Specification Matching of Software Components, TOSEM 1997, Def. 2). Il loro plug-in match è la chiamata tipizzata; il loro plug-in post match, con la precondizione eliminata, è una richiesta il cui input è sconosciuto.
• Una descrizione con una parte sconosciuta indica l’insieme delle cose che potrebbe essere, e soddisfa un predicato quando qualche membro lo soddisfa (Garcia, Clark & Tanter, Abstracting Gradual Typing, POPL 2016, Def. 3). Lo sconosciuto non è il tipo in cima: trattarlo come tale è la confusione fra un esistenziale e un universale che rende tali relazioni non transitive.
• La legge transitiva appartiene al rendere una descrizione più precisa, un preordine accanto alla sottotipizzazione (Castagna, Lanvin, Petrucciani & Siek, Gradual Typing: A New Perspective, POPL 2019, §2.1 “materialization”).
• “Qualche” e “tutti” sono i due aggiunti della stessa operazione (Lawvere, Adjointness in Foundations, 1969).

Riepilogo

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

Questo è il predicato principale per l’instradamento. Il ranking (documento successivo) si applica soltanto dopo che si sa che un candidato serve.