Predicati

Fondamento

Ogni forma di tag significa l’insieme degli stati in cui può trovarsi la sua chiave, e significa lo stesso insieme su entrambi i lati di un confronto:

Un URN significa le cose che si trovano in uno stato ammesso per ogni chiave. Quindi un URN è una descrizione, e una descrizione è un insieme: media:document;ext=pdf è ogni valore il cui ext è pdf, quali che siano i suoi altri tag.

A due descrizioni si possono porre due domande diverse, e ne sorge una terza quando uno dei lati non è una descrizione ma una cosa:

Sono tre relazioni su un unico significato, non una relazione con eccezioni; Perché sono tre spiega perché devono restare separate.

Il modello è tagged-urn/formal (Lean), e ogni implementazione esegue codice generato da esso. tagMatch_iff_allows, tagMeets_iff_allows, refines_iff_holds e meets_iff_holds sono i teoremi che affermano che le tabelle qui sotto sono l’inclusione e la sovrapposizione dei significati qui sopra, per singole chiavi e per URN interi.

La garanzia: conforms_to, accepts, is_equivalent, is_comparable

conforms_to(a, b)   :⟺  a ⪯ b              a è almeno tanto specifico quanto b
accepts(a, b)       :⟺  b ⪯ a              lo stesso, dal lato del pattern
is_equivalent(a, b) :⟺  a ⪯ b  ∧  b ⪯ a    lo stesso insieme di tag
is_comparable(a, b) :⟺  a ⪯ b  ∨  b ⪯ a    sulla stessa catena di specializzazione

Esempi:

conforms_to(media:bytes;document;ext=pdf, media:bytes)   = true   # ogni pdf di bytes è bytes
conforms_to(media:bytes, media:bytes;document;ext=pdf)   = false  # i bytes non devono per forza essere un pdf
conforms_to(media:ext, media:document;ext=pdf)           = false  # "un qualche ext" non è una promessa di pdf
conforms_to(media:document;ext=pdf, media:ext)           = true   # un pdf è un qualche ext
is_equivalent(media:ext, media:document;ext=pdf)         = false  # insiemi di tag diversi
is_comparable(media:ext, media:document;ext=pdf)         = true   # una sola catena

La tabella

Istanza (riga) contro pattern (colonna): ✓ quando ogni stato che l’istanza ammette è ammesso anche dal pattern.

Un’istanza che omette una chiave, o dice ?x, non promette nulla su di essa, quindi soddisfa solo i pattern che non chiedono nulla. x promette la presenza e nessun valore in particolare. Qui nulla viene “deciso in seguito”: una garanzia si stabilisce con le sole due descrizioni.

Proprietà

• conforms_to e accepts sono riflessivi e transitivi (refines_refl, refines_trans): un preordine.
• is_equivalent è una relazione di equivalenza, e URN equivalenti dicono la stessa cosa per ogni chiave, a meno di missing e ?x, che significano la stessa cosa (equivalent_iff_same_forms). La ricerca degli alias e la corrispondenza degli stream per equivalenza sono corrispondenze per insieme di tag.
• Raffinare non dà mai un punteggio più basso (tagScore_monotone), quindi una sorgente conforme a un argomento non è mai meno specifica di esso.

La possibilità: meets

meets(a, b)  :⟺  qualcosa è descritto sia da a sia da b

Simmetrica: nessuno dei due lati è l’istanza. È ciò che chiede una ricerca, ed è ciò che significa “deciso al momento dell’esecuzione”:

meets(media:ext, media:document;ext=pdf)        = true   # un qualche ext POTREBBE essere un pdf
conforms_to(media:ext, media:document;ext=pdf)  = false  # non è garantito che lo sia
meets(media:document;ext=pdf, media:ext=png)    = false  # escluso

La tabella

Le stesse sette forme; ✓ quando le due ammettono uno stato in comune. È simmetrica, quindi vale la pena elencare solo le celle che falliscono. Due forme non si incontrano esattamente quando:

Ogni altra coppia si incontra.

Proprietà

• Riflessiva e simmetrica (meets_refl, meets_symm).
• Non transitiva, e non è pensata per esserlo (tagMeets_not_transitive): un pdf incontra “un qualche ext”, che incontra un png.
• Ciò che è conforme si incontra (refines_meets; nessuna forma è vuota), e ciò che incontra b incontra tutto ciò che b raffina (meets_of_refines).

meets serve per esplorare. Nulla viene mai instradato in base a esso: una chiamata viene instradata in base a una garanzia (Dispatch).

Cose complete: satisfies, may_satisfy

Una descrizione che omette una chiave non dice nulla su di essa. Una cosa che esiste omette una chiave perché non ce l’ha. Due tipi di cose sono complete:

• il media di un valore effettivo (uno stream che è arrivato, un output che è stato prodotto o un file che è stato rilevato);
• l’elenco dei tag propri di una cap: una cap ha i tag che ha.

Un tipo di media sull’in o sull’out di una cap non è completo: una cap che accetta media:document;ext=pdf accetta anche pdf compressi.

satisfies(thing, pattern)     garantito, leggendo ciò che manca alla cosa come assente
may_satisfy(thing, pattern)   possibile, con la stessa lettura

La lettura completa cambia esattamente una riga: la riga mancante della cosa diventa la riga !x (Constraint.closed).

conforms_to(media:document;ext=pdf, media:document;ext=pdf;!compressed)  = false  # come TIPO può essere compresso
satisfies(media:document;ext=pdf, media:document;ext=pdf;!compressed)    = true   # come VALORE non ha quel tag

satisfies non è una relazione fra due descrizioni e non è transitiva attraverso una descrizione (refinesClosed_not_transitive): x=v soddisfa la descrizione che non dice nulla di x, una cosa completa che tace su x soddisfa !x, e x=v no. Ciò che vale è la legge propria di una relazione di soddisfacimento: ciò che soddisfa una descrizione soddisfa tutto ciò che quella descrizione raffina (refinesClosed_of_refines).

Quale usare

if declared_output.conforms_to(&next_input)? { /* l'arco funziona sempre */ }
if declared_output.meets(&next_input)?       { /* potrebbe; verifica all'esecuzione */ }
if arrived_stream.satisfies(&arg_type)?      { /* questo valore è quell'argomento */ }

Per le cap, nessuno di questi da solo è la domanda di instradamento; vedi Dispatch.

Errori comuni

Usare una possibilità dove serve una garanzia

if candidate_output.meets(&needed) { /* instrada qui */ }   // SBAGLIATO

Una cap che fornisce “una qualche immagine” potrebbe fornire un jpeg. Instradarle una chiamata che ha bisogno di un jpeg è un fallimento che aspetta solo che arrivi il valore.

Leggere un valore come un tipo

if stream_media.conforms_to(&pattern) { ... }   // legge le omissioni del valore come "qualsiasi cosa"
if stream_media.satisfies(&pattern)   { ... }   // le legge come assenze

I due coincidono finché un pattern non chiede un’assenza (!x) o vieta un valore (x?=v).

Confondere la direzione

if pattern.conforms_to(&instance) { ... }  // AL CONTRARIO
if instance.conforms_to(&pattern) { ... }  // oppure: pattern.accepts(&instance)

Perché sono tre

Un’unica tabella non può rispondere a tutte e tre le domande. Leggere un x o un ?x dal lato dell’istanza come “qualunque cosa voglia il pattern, deciso in seguito” mette una possibilità dentro una garanzia. Leggere una chiave omessa come “qualsiasi cosa” in un pattern e come “assente” in un’istanza tratta un lato come una descrizione e l’altro come una cosa completa. Una relazione costruita così non è né una garanzia né una possibilità: il raffinamento smette di essere transitivo, media:ext e media:document;ext=pdf diventano “equivalenti”, e l’equivalenza smette di essere una relazione di equivalenza.

La separazione segue lavori consolidati. Una descrizione con parti incognite significa l’insieme delle cose che potrebbe essere; si può chiedere che un predicato valga per tutto quell’insieme o per una parte di esso, e sono due relazioni diverse con leggi diverse. La seconda è riflessiva e simmetrica e non deve essere transitiva (Garcia, Clark & Tanter, Abstracting Gradual Typing, POPL 2016, Def. 1–3; Siek & Taha, Gradual Typing for Functional Languages, 2006). La sottotipizzazione come inclusione dei significati è la sottotipizzazione semantica (Frisch, Castagna & Benzaken, JACM 2008). Il matchmaking chiama la stessa coppia corrispondenza plug-in e intersection (Li & Horrocks, 2003). E leggere un’omissione come un’assenza è l’ipotesi del mondo chiuso (Reiter, 1978), che appartiene ai fatti, non alle descrizioni.

Riepilogo