synit-manual/src/protocols/syndicate/dataspacePatterns.md

120 lines
4.6 KiB
Markdown
Raw Normal View History

# Patterns over assertions
- [`[syndicate-protocols]/schemas/dataspacePatterns.prs`](https://git.syndicate-lang.org/syndicate-lang/syndicate-protocols/src/branch/main/schemas/dataspacePatterns.prs)
Each [subscription record](./dataspace.md) asserted at a dataspace entity contains a pattern
over [Preserves values](../../guide/preserves.md#grammar-of-values).
The pattern language is carefully chosen to be reasonably expressive without closing the door
to efficient indexing of dataspace contents.[^efficient-indexing]
## 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](#binding) in the overall pattern.
## Example
Consider the pattern:
```preserves
<arr [<lit 1> <bind <arr [<bind <_>> <_>]>> <_>]>
```
The following values each yield different results:
- `[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 3 4] 5]` fails, because `[2 3 4]` has more than the expected two elements.
- `[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 *compound*.
```preserves-schema
Pattern = DDiscard / DBind / DLit / DCompound .
```
### Discard
A *discard pattern* matches any input value.
```preserves-schema
DDiscard = <_>.
```
### Binding
A *binding pattern* 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.
```preserves-schema
DBind = <bind @pattern Pattern>.
```
### Literal
A *literal pattern* matches any **atomic** Preserves value. In order to match a literal
**compound** value, a combination of compound and literal patterns must be used.
```preserves-schema
DLit = <lit @value AnyAtom>.
AnyAtom =
/ @bool bool
/ @float float
/ @double double
/ @int int
/ @string string
/ @bytes bytes
/ @symbol symbol
/ @embedded #!any
.
```
### Compound
Each *compound pattern* first checks the type of its input: a `rec` pattern fails unless it is
given a Record, an `arr` demands a Sequence and a `dict` only matches a Dictionary.
```preserves-schema
DCompound = <rec @label any @fields [Pattern ...]>
/ <arr @items [Pattern ...]>
/ <dict @entries { any: Pattern ...:... }> .
```
If the type check fails, the pattern match fails. Otherwise, matching continues:
- `rec` patterns compare the label of the input Record against the `label` field in the
pattern; unless they match literally and exactly, the overall match fails. Otherwise, if the
number of fields in the input does not equal the number expected in the pattern, the match
fails. Otherwise, matching proceeds structurally recursively.
- `arr` patterns fail if the number of subpatterns does not match the number of items in the
input Sequence. Otherwise, matching proceeds structurally recursively.
- `dict` patterns consider each of the key/subpattern pairs in `entries` in turn, according to
the Preserves order of the keys.[^dict-pattern-ordering] If any given key from the pattern
is not present in the input value, matching fails. Otherwise, matching proceeds recursively.
The pattern ignores keys in the input value that are not mentioned in the pattern.
---
[^efficient-indexing]: Most implementations of Syndicated Actor Model dataspaces use an
efficient index datastructure [described here](https://git.syndicate-lang.org/syndicate-lang/syndicate-rkt/src/commit/90c4c60699069b496491b81ee63b5a45ffd638cb/syndicate/HOWITWORKS.md).
[^dict-pattern-ordering]: 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`).