Patterns over assertions

[syndicate-protocols]/schemas/dataspacePatterns.prs

Each subscription record asserted at a dataspace entity contains a pattern over Preserves values.

The pattern language is carefully chosen to be reasonably expressive without closing the door to efficient indexing of dataspace contents.¹

Interpretation of patterns

A pattern is matched against a candidate input value. Matching can either fail or succeed; if matching succeeds, a sequence of (numbered) bindings is produced. Each binding in the sequence corresponds to a (possibly-nested) binding pattern in the overall pattern.

Example

Consider the pattern:

<group <arr> {
  0: <lit 1>
  1: <bind <group <arr> {
    0: <bind <_>>
    1: <_>
  }>>
  2: <_>
}>

Each of the following values yields different results when matched against it:

[1 2 3] fails, because 2 is not an array.
[1 [2 3] 4] succeeds, yielding a binding sequence [[2 3] 2], because the outer bind captures the whole [2 3] array, and the inner (nested) bind captures the 2.
[1 [2] 5] fails, because [2] lacks an element at index 1.
However, [1 [2 3 4] 5] succeeds, yielding a binding sequence [[2 3 4] 2], because [2 3 4] has at least the expected two elements at indexes 0 and 1.
[1 [<x> <y>] []] succeeds, yielding a binding sequence [[<x> <y>] <x>]. Each discard pattern (<_>) ignores the specific input it is given.

Abstract syntax of patterns

A pattern may be either a discard, a (nested) binding, a literal, or a group (compound).

Pattern =
    / @discard <_>
    / <bind @pattern Pattern>
    / <lit @value AnyAtom>
    / <group @type GroupType @entries { any: Pattern ...:... }>
.

Discard

A discard pattern, <_>, matches any input value.

Binding

A binding pattern, <bind ...>, speculatively pushes the portion of the input under consideration onto the end of the binding sequence being built, and then recursively evaluates its subpattern. If the subpattern succeeds, so does the overall binding pattern (keeping the binding); otherwise, the speculative addition to the binding sequence is undone, and the overall binding pattern fails.

Literal

A literal pattern, <lit ...>, matches any atomic Preserves value:

AnyAtom =
    / @bool bool
    / @double double
    / @int int
    / @string string
    / @bytes bytes
    / @symbol symbol
    / @embedded #:any
.

In order to match a literal compound value, a combination of group and literal patterns must be used.

Group

Each group pattern first checks the type of its input: a rec pattern fails unless it is given a Record having the specified label, an arr demands a Sequence and a dict only matches a Dictionary.

GroupType =
    / <rec @label any>
    / <arr>
    / <dict>
.

If the type check fails, the pattern match fails. Otherwise, matching continues. Subpatterns in the entries field in the group pattern are considered in increasing Preserves order of key.² For Records, each key must be a field index; for Sequences, each key is an element index; and for Dictionaries, keys are just keys in the dictionary to be matched. Each subpattern is matched against the corresponding portion of the input, failing if no such item exists.

Group patterns ignore keys in values being matched that are not mentioned in the pattern. Matching succeeds if such values have more than the structure and information required of them by a given pattern, but not if they have less. This allows for protocol extension: for example, records with "extra" fields will continue to match.

Most implementations of Syndicated Actor Model dataspaces use an efficient index datastructure described here.

The ordering of visiting of keys in a dict pattern is important because bindings are numbered in this pattern language, not named. Recall that <dict {a: <bind <_>>, b: <bind <_>>}> is an identical Preserves value to <dict {b: <<bind <_>>, a: <bind <_>>}>, so to guarantee consistent binding results, we must choose some deterministic order for visiting the subpatterns of the dict. (In this example, a will be visited before b, because a < b).

The Synit Manual