Predicates

Foundation

Every tag form means the set of states its key may be in, and it means the same set on either side of a comparison:

A URN means the things that are in an allowed state at every key. So a URN is a description, and a description is a set: media:document;ext=pdf is every value whose ext is pdf, whatever its other tags.

Two descriptions can be asked two different questions, and a third arises when one side is not a description but a thing:

These are three relations on one meaning, not one relation with exceptions; Why there are three explains why they must stay separate.

The model is tagged-urn/formal (Lean), and every implementation runs code generated from it. tagMatch_iff_allows, tagMeets_iff_allows, refines_iff_holds and meets_iff_holds are the theorems that say the tables below are inclusion and overlap of the meanings above, for single keys and for whole URNs.

The guarantee: conforms_to, accepts, is_equivalent, is_comparable

conforms_to(a, b)   :⟺  a ⪯ b              a is at least as specific as b
accepts(a, b)       :⟺  b ⪯ a              the same, from the pattern's side
is_equivalent(a, b) :⟺  a ⪯ b  ∧  b ⪯ a    the same tag set
is_comparable(a, b) :⟺  a ⪯ b  ∨  b ⪯ a    on one specialization chain

Examples:

conforms_to(media:bytes;document;ext=pdf, media:bytes)   = true   # every pdf of bytes is bytes
conforms_to(media:bytes, media:bytes;document;ext=pdf)   = false  # bytes need not be a pdf
conforms_to(media:ext, media:document;ext=pdf)           = false  # "some ext" is not a promise of pdf
conforms_to(media:document;ext=pdf, media:ext)           = true   # a pdf is some ext
is_equivalent(media:ext, media:document;ext=pdf)         = false  # different tag sets
is_comparable(media:ext, media:document;ext=pdf)         = true   # one chain

The table

Instance (row) against pattern (column): ✓ when every state the instance allows, the pattern allows.

An instance that omits a key, or says ?x, promises nothing about it, so it satisfies only the patterns that ask for nothing. x promises presence and no particular value. Nothing is “decided later” here: a guarantee is settled by the two descriptions alone.

Properties

• conforms_to and accepts are reflexive and transitive (refines_refl, refines_trans): a preorder.
• is_equivalent is an equivalence relation, and equivalent URNs say the same thing at every key, up to missing and ?x, which mean the same (equivalent_iff_same_forms). Alias lookup and stream matching by equivalence are matching by tag set.
• Refining never scores lower (tagScore_monotone), so a source that conforms to an argument is never less specific than it.

The possibility: meets

meets(a, b)  :⟺  some thing is described by both a and b

Symmetric: neither side is the instance. This is what a search asks, and what “decided at run time” means:

meets(media:ext, media:document;ext=pdf)        = true   # some ext COULD be a pdf
conforms_to(media:ext, media:document;ext=pdf)  = false  # it is not guaranteed to be
meets(media:document;ext=pdf, media:ext=png)    = false  # excluded

The table

The same seven forms; ✓ when the two allow a common state. Symmetric, so only the cells that fail are worth listing. Two forms fail to meet exactly when:

Every other pair meets.

Properties

• Reflexive and symmetric (meets_refl, meets_symm).
• Not transitive, and not meant to be (tagMeets_not_transitive): a pdf meets “some ext”, which meets a png.
• Whatever conforms meets (refines_meets; no form is empty), and what meets b meets everything b refines (meets_of_refines).

meets is for exploring. Nothing is ever routed on it: a call is routed on a guarantee (Dispatch).

Complete things: satisfies, may_satisfy

A description that omits a key says nothing about it. A thing that exists omits a key because it does not have it. Two kinds of thing are complete:

• the media of an actual value (a stream that arrived, an output that was produced, or a file that was detected);
• a cap’s own list of cap-tags: a cap has the tags it has.

A media type on a cap’s in or out is not complete: a cap that takes media:document;ext=pdf takes compressed pdfs too.

satisfies(thing, pattern)     guaranteed, reading the thing's omissions as absences
may_satisfy(thing, pattern)   possible, on the same reading

The complete reading changes exactly one row: the thing’s missing row becomes the !x row (Constraint.closed).

conforms_to(media:document;ext=pdf, media:document;ext=pdf;!compressed)  = false  # as a TYPE it may be compressed
satisfies(media:document;ext=pdf, media:document;ext=pdf;!compressed)    = true   # as a VALUE it has no such tag

satisfies is not a relation between two descriptions and is not transitive through one (refinesClosed_not_transitive): x=v satisfies the description that says nothing of x, a complete thing silent on x satisfies !x, and x=v does not. What holds is the law a satisfaction relation has: what satisfies a description satisfies everything that description refines (refinesClosed_of_refines).

Which one

if declared_output.conforms_to(&next_input)? { /* the edge always works */ }
if declared_output.meets(&next_input)?       { /* it may; check when run */ }
if arrived_stream.satisfies(&arg_type)?      { /* this value is that arg */ }

For caps, none of these alone is the routing question; see Dispatch.

Common mistakes

Using a possibility where a guarantee is needed

if candidate_output.meets(&needed) { /* route here */ }   // WRONG

A cap that gives “some image” could give a jpeg. Routing a call that needs a jpeg to it is a failure waiting for the value to turn up.

Reading a value as a type

if stream_media.conforms_to(&pattern) { ... }   // reads the value's omissions as "anything"
if stream_media.satisfies(&pattern)   { ... }   // reads them as absences

The two agree until a pattern asks for an absence (!x) or forbids a value (x?=v).

Confusing direction

if pattern.conforms_to(&instance) { ... }  // BACKWARDS
if instance.conforms_to(&pattern) { ... }  // or: pattern.accepts(&instance)

Why there are three

A single table cannot answer all three questions. Reading an instance-side x or ?x as “whatever the pattern wants, decided later” puts a possibility inside a guarantee. Reading an omitted key as “anything” in a pattern and “absent” in an instance treats one side as a description and the other as a complete thing. A relation built that way is neither a guarantee nor a possibility: refinement stops being transitive, media:ext and media:document;ext=pdf become “equivalent”, and equivalence stops being an equivalence relation.

The separation follows established work. A description with unknown parts means the set of things it could be; a predicate can be asked to hold of all of that set or of some of it, and the two are different relations with different laws. The second is reflexive and symmetric and must not be transitive (Garcia, Clark & Tanter, Abstracting Gradual Typing, POPL 2016, Def. 1–3; Siek & Taha, Gradual Typing for Functional Languages, 2006). Subtyping as inclusion of meanings is semantic subtyping (Frisch, Castagna & Benzaken, JACM 2008). Matchmaking calls the same pair plug-in and intersection match (Li & Horrocks, 2003). And reading an omission as an absence is the closed-world assumption (Reiter, 1978), which belongs to facts, not to descriptions.

Summary