§4 Syntactic grammar

This chapter defines Bynk’s phrase structure: how tokens (§3) combine into declarations, types, expressions, patterns, and statements. Each production is generated from the grammar (§2.1) and embedded by name.

A production states what parses. Every constraint beyond parsing — name resolution, typing, exhaustiveness, refinement admission, the effect discipline, and all other well-formedness — is a static-semantics rule, specified normatively in §5 and not repeated here. Where a construct carries such constraints, this chapter forward-references §5 rather than restating them.

The chapters mirror the construct groupings of the friendly grammar reference; the productions are shared, the register here is the normative definition.

§4.1 Top-level & modules

A source file is a commons, a context, an adapter, or test declarations.

§4.1.1 source_file

source_file ::= (commons_decl | context_decl | adapter_decl | suite_decl)+ | item_fragment+ | expr_fragment

A whole file: one or more top-level declarations, or a single fragment used by editor tooling.

§4.1.2 item_fragment

item_fragment ::= context_body_item | handler | store_field | key_decl

A tooling entry point: a single body item parsed in isolation. Not written by hand.

§4.1.3 expr_fragment

expr_fragment ::= statement+ expression? | expression

A tooling entry point: statements and/or an expression parsed in isolation. Not written by hand.

§4.1.4 commons_decl

commons_decl ::= "commons" qualified_name ("{" commons_body_item* "}" | commons_body_item*)

A commons module. The body braces are optional at file scope; with no braces the body items run to the end of the file.

§4.1.5 context_decl

context_decl ::= "context" qualified_name ("{" context_body_item* "}" | context_body_item*)

A context. As with commons, the body braces are optional at file scope. Well-formedness: §5.

§4.1.6 adapter_decl

adapter_decl ::= "adapter" qualified_name ("{" adapter_body_item* "}" | adapter_body_item*)

An adapter — the host boundary: a capability contract co-located with a named TypeScript binding. As with commons, the body braces are optional at file scope. An adapter’s providers are external (bodiless, §4.3.8) and it may not declare services or agents; those placement rules, the binding requirement, and the reserved bynk namespace are well-formedness: §5.

§4.1.7 suite_decl

suite_decl ::= "suite" qualified_name ("as" ("unit" | "integration" | "system"))? ("{" test_body_item* "}" | test_body_item*)

A suite block naming the commons or context it targets. A suite header may carry an optional as <tier> clause (§4.9) that sets the default tier its cases inherit. Well-formedness: §5.

§4.1.8 commons_body_item

commons_body_item ::= uses_decl | type_decl | fn_decl | messages_decl | capability_decl | provider_decl | service_decl | agent_decl | actor_decl | event_decl

The declaration forms admitted in a commons body.

§4.1.9 context_body_item

context_body_item ::= uses_decl | consumes_decl | exports_decl | type_decl | fn_decl | capability_decl | provider_decl | service_decl | agent_decl | actor_decl | messages_decl | event_decl

The declaration forms admitted in a context body, including consumes and exports.

§4.1.10 adapter_body_item

adapter_body_item ::= binding_decl | uses_decl | consumes_decl | exports_decl | type_decl | fn_decl | capability_decl | provider_decl | service_decl | agent_decl | actor_decl | messages_decl | event_decl

The declaration forms admitted in an adapter body: the binding clause, capability and type declarations, pure helpers and uses, consumes, exports, and providers. The grammar is deliberately permissive — service and agent parse here so the placement error can be precise; their rejection is well-formedness: §5.

§4.1.11 test_body_item

test_body_item ::= uses_decl | consumes_decl | stub_clause | case | property_decl

The declaration forms admitted in a suite body: uses, stub clauses, and case / property declarations.

§4.1.12 event_decl (v0.238)

event_decl ::= "event" identifier store_annotation* "=" record_type

event, a name, zero or more @name(args) annotations, =, and a record body: a typed fact a context emits with the Events capability and other contexts receive with a from Events(E) subscription (§4.4.7b). The body is a record type only; its fields may carry a default (field: T = expr). The grammar admits an event in any body, and the annotation list in any number. Placement (contexts only), the closed annotation set (@schema(N), at most once), field defaults, and emission are well-formedness: §5.7b.

§4.1.13 messages_decl (v0.228)

messages_decl ::= "messages" string_literal store_annotation* "{" message_entry* "}"

A message bundle’s block for one locale: messages, the locale tag as a string literal, zero or more annotations (@reference marks the reference locale), and a brace-delimited list of entries. The grammar admits it in any body; placement (commons only), the tag’s LocaleTag check, and the one-@reference rule are well-formedness: §5.11.

§4.1.14 message_entry

message_entry ::= string_literal "=>" string_literal ","?

One "code" => "template" entry in a messages block. Both sides are plain string literals: an interpolated string ("…\(x)…") is a parse error here. A template’s {name} placeholders are ICU MessageFormat, not Bynk syntax; they are checked by §5.11, not parsed by the grammar.

§4.1.15 qualified_name

qualified_name ::= identifier ("." identifier)*

A dotted sequence of identifiers, e.g. shop.orders. A dotted name is a single flat identifier, not a hierarchy: bynk and bynk.time are independent names that merely share a leading segment.

§4.1.16 uses_decl

uses_decl ::= "uses" qualified_name

uses followed by a qualified name. Well-formedness: §5.

§4.1.17 consumes_decl

consumes_decl ::= "consumes" qualified_name ("as" identifier | "{" (identifier ("," identifier)*)? ","? "}")?

consumes a unit, in one of three forms: the whole unit (consumes b), the whole unit under an alias (consumes b as Alias), or a capability selection (consumes b { Cap, … }), which flattens the named capabilities into the consumer’s local capability namespace under their bare names. The target may be a context or an adapter; which forms each consumer kind admits, and the flattening and clash rules, are well-formedness: §5.

§4.1.18 exports_decl

exports_decl ::= "exports" ("opaque" | "transparent" | "capability") "{" (identifier ("," identifier)*)? ","? "}"

exports, one of opaque / transparent / capability, and a brace-delimited identifier list. Well-formedness: §5.

§4.1.19 binding_decl

binding_decl ::= "binding" string_literal ("requires" "{" (binding_requirement ("," binding_requirement)*)? ","? "}")?

An adapter’s binding clause: the TypeScript module supplying its external provider classes, as a string-literal path resolved relative to the adapter’s source file, with an optional requires { … } map of npm dependencies. Well-formedness: §5.

§4.1.20 binding_requirement

binding_requirement ::= string_literal ":" string_literal

One "package": "range" entry in a binding’s requires map. Ranges MUST be pinned; well-formedness: §5.

Type declarations and the type references that appear in signatures.

§4.2.1 type_decl

type_decl ::= "type" identifier ("[" identifier ("," identifier)* "]")? "=" type_body

type, a name, an optional [A, B] type-parameter list (v0.157 — only a record body may be generic; a parameter is an unconstrained, bound-free name scoped to the declaration), =, and a type body. Well-formedness: §5; the type system: §6.

§4.2.2 type_body

type_body ::= opaque_type | refined_type | record_type | sum_type | enum_type

The right-hand side of a type: one of the five type forms.

§4.2.3 opaque_type

opaque_type ::= "opaque" base_type ("where" refinement)?

opaque, a base type, and an optional where refinement.

§4.2.4 refined_type

refined_type ::= base_type ("where" refinement)?

A base type with an optional where refinement. Well-formedness: §5; admission: §6.

§4.2.5 record_type

record_type ::= "{" (record_field ("," record_field)*)? ","? "}"

A brace-delimited, comma-separated list of record fields, with an optional trailing comma.

§4.2.6 record_field

record_field ::= identifier ":" type_ref ("where" refinement)? ("=" expression)?

A field name, :, a type, an optional inline where refinement, and an optional = default expression. Well-formedness: §5.

§4.2.7 sum_type

sum_type ::= sum_variant+ ("embeds" type_ref "as" constant_name ("," type_ref "as" constant_name)*)?

One or more |-prefixed variants, followed by an optional trailing embeds <type> as <Variant>, … clause (v0.154) declaring error embeddings — mappings a value of <type> auto-wraps into the named single-payload variant, which the ? operator uses for automatic error conversion (§5.2). embeds and as are contextual keywords here. Well-formedness: §5.

§4.2.8 sum_variant

sum_variant ::= "|" constant_name ("(" (variant_payload_field ("," variant_payload_field)*)? ","? ")")?

A |, a constant name, and an optional parenthesised payload.

§4.2.9 variant_payload_field

variant_payload_field ::= identifier ":" type_ref

A named field in a sum-variant payload: an identifier, :, and a type.

§4.2.10 enum_type

enum_type ::= "enum" "{" (constant_name ("," constant_name)*)? ","? "}"

enum and a brace-delimited list of constant names — a sum type whose variants all carry no payload.

refinement ::= refinement_pred ("&&" refinement_pred)*

One or more predicates joined by &&. Well-formedness: §5.

§4.2.12 refinement_pred

refinement_pred ::= pred_call | predicate_name

A single predicate: a predicate call or a bare predicate name.

§4.2.13 pred_call

pred_call ::= predicate_name "(" (pred_arg ("," pred_arg)*)? ")"

A predicate name applied to parenthesised arguments, e.g. InRange(1, 100).

§4.2.14 predicate_name

predicate_name ::= "Matches" | "InRange" | "MinLength" | "MaxLength" | "Length" | "NonNegative" | "Positive" | "NonEmpty"

The set of built-in refinement predicates. Well-formedness: §5.

§4.2.15 pred_arg

pred_arg ::= "-"? number_literal | "-"? float_literal | string_literal

An argument to a predicate: a number or string literal.

§4.2.16 base_type

base_type ::= "Int" | "String" | "Bool" | "Float" | "Duration" | "Instant" | "Bytes"

The primitive types Int, String, and Bool. Well-formedness: §5.

§4.2.17 type_ref

type_ref ::= function_type_ref | base_type | unit_type | validation_error_type | generic_type_ref | applied_type_ref | identifier

A type as it appears in a signature: a function type, a base type, the unit type, the validation-error type, a generic application, or a named type.

§4.2.17a function_type_ref

function_type_ref ::= (base_type | unit_type | validation_error_type | generic_type_ref | applied_type_ref | identifier | "(" type_ref ("," type_ref)* ","? ")") "->" type_ref

A function type (v0.20a): Int -> Int, (Int, String) -> Bool, () -> Int. The arrow is right-associative — A -> B -> C is A -> (B -> C) — and a parenthesised list before -> is a parameter list (a single parenthesised type without an arrow is a grouping; the empty () without an arrow stays the unit type). A function type is effectful exactly when its return type is Effect[_] — the structural rule of §6. Function types are confined to non-boundary positions; well-formedness: §5.

§4.2.18 unit_type

unit_type ::= "(" ")"

The unit type ().

§4.2.19 validation_error_type

validation_error_type ::= "ValidationError"

ValidationError, the error type produced when refined-type validation fails.

§4.2.20 generic_type_ref

generic_type_ref ::= ("Option" | "Effect" | "HttpResult" | "List" | "Stream" | "Query" | "Connection" | "History") "[" type_ref "]" | ("Result" | "Map") "[" type_ref "," type_ref "]"

A generic constructor — Result, Option, Effect, HttpResult, or (v0.20b) List, Map — applied to bracketed type arguments. Well-formedness: §5 (Map keys are value-keyable, §5.10); the type system: §6.

§4.2.20a applied_type_ref

applied_type_ref ::= identifier "[" type_ref ("," type_ref)* "]"

An application of a user-declared generic type (v0.157) to bracketed type arguments — Paginated[User], Keyed[String, Int]. The head is a user type name declared type Name[T, …] = { … } (a record). A generic type must be applied to exactly its declared number of arguments, and a generic record is a non-boundary value. Well-formedness: §5; the type system: §6.

§4.3 Functions, capabilities & providers

Pure functions and methods, capability interfaces, and the providers that implement them.

§4.3.1 fn_decl

fn_decl ::= "fn" (method_name | identifier) ("[" identifier ("," identifier)* "]")? "(" params? ")" "->" type_ref requires_clause* ensures_clause* block

fn, a function name or a Type.method name, an optional [A, B] type-parameter list (v0.20a — free functions only; a type parameter is an unconstrained, bound-free name scoped to the signature and body), a parameter list, ->, a return type, any number of contract clauses (v0.115), and a block body. Well-formedness: §5.

§4.3.1a requires_clause / ensures_clause (v0.115)

requires_clause ::= "requires" identifier ":" expression

ensures_clause ::= "ensures" identifier ":" expression

A function contract (testing track slice 3): named requires (preconditions) and ensures (postconditions) between the return type and the body, each a pure Bool predicate expression — the one predicate surface (§4.6, ADR 0144). A requires predicate is over the parameters; an ensures predicate is over the parameters and result, the contextual binding for the return value (an ordinary identifier elsewhere). Well-formedness — purity, Bool type, result scope, distinct names: §5 (ADR 0150).

§4.3.2 method_name

method_name ::= identifier "." identifier

A Type.method name, defining a method on a named type.

§4.3.3 params

params ::= (self_param | param) ("," param)* ","?

A parameter list: an optional self receiver followed by named parameters, with an optional trailing comma.

§4.3.4 self_param

self_param ::= "self"

The self receiver of a method or handler.

§4.3.5 param

param ::= identifier ":" type_ref

One parameter: an identifier, :, and a type. Well-formedness: §5.

§4.3.6 capability_decl

capability_decl ::= "capability" identifier "{" capability_op* "}"

capability, a name, and a brace-delimited list of operation signatures. Well-formedness: §5.

§4.3.7 capability_op

capability_op ::= "fn" identifier ("[" identifier ("," identifier)* "]")? "(" (param ("," param)*)? ","? ")" "->" type_ref

One operation in a capability: fn, a name, an optional [T, …] type-parameter list (v0.235, ADR 0281), parameters, ->, and a return type — no body. A type parameter is resolved only from an explicit type argument at the call site (Cap.op[SomeType](…)), never inferred. Well-formedness: §5.

§4.3.8 provider_decl

provider_decl ::= "provides" identifier "=" identifier given_clause? ("{" provider_op* "}")?

provides, the capability name, =, an implementation name, an optional given clause, and an optional brace-delimited list of operation implementations. The presence of the brace block distinguishes the two provider kinds: with a block the provider is implemented in Bynk (context-only); with no block it is external — its implementation is the named class exported by the enclosing adapter’s binding module (§4.1.19). The absence of the block, not an empty one, is the signal. Placement and wiring rules: well-formedness, §5.

§4.3.9 provider_op

provider_op ::= "fn" identifier "(" (param ("," param)*)? ","? ")" "->" type_ref block

One operation implementation: a capability operation signature with a block body. Well-formedness: §5.

§4.3.10 given_clause

given_clause ::= "given" qualified_name ("," qualified_name)*

given and a comma-separated list of the capabilities a handler or provider may use. Well-formedness: §5.

§4.4 Services & handlers

A service groups the handlers that respond to calls and external triggers.

§4.4.1 service_decl

service_decl ::= "service" identifier service_protocol? by_clause? given_clause? "{" cors_policy? security_policy? limits_policy? (store_annotation* handler)* "}"

service, a name, an optional from <protocol> header clause, and a brace-delimited list of handlers. One protocol per service. Well-formedness: §5.

§4.4.1a HTTP service policies (v0.131, v0.141, v0.142)

A from http service may open with up to three policy sections, in header position before its handlers and in this order: cors { }, then security { }, then limits { }, each optional (the order is service_decl’s). A policy out of that order, or after a handler, is a parse error (bynk.parse.policy_order). Each is a brace-delimited list of name: value fields. cors, security and limits are contextual keywords, ordinary identifiers elsewhere. The grammar admits any field name and any value expression; the closed field sets, their value types, and the from http-only placement are well-formedness: §5.7.1, §5.7.3 and §5.7.4.

cors_policy

cors_policy ::= "cors" "{" (cors_field ","?)* "}"

The cross-origin policy (v0.131).

cors_field

cors_field ::= identifier ":" expression

One name: value field of a cors policy.

security_policy

security_policy ::= "security" "{" (security_field ","?)* "}"

The security-headers policy (v0.141).

security_field

security_field ::= identifier ":" expression

One name: value field of a security policy.

limits_policy

limits_policy ::= "limits" "{" (limits_field ","?)* "}"

The request-limits policy (v0.142).

limits_field

limits_field ::= identifier ":" expression

One name: value field of a limits policy.

§4.4.2 service_protocol

service_protocol ::= "from" ("http" | "cron" | "queue" "(" string_literal ")" | "websocket" "(" "in" ":" type_ref "," "out" ":" type_ref ","? ")" | "Events" "(" type_ref event_pattern? ")" schema_dispatch_clause?)

The from <protocol> clause: from http, from cron, from queue("name") (v0.44), from websocket(in: I, out: O) (v0.103), or from Events(E) (v0.238), whose event may carry a delivery pattern and a via schema(N) clause (§4.4.7b). Absent ⇒ the contract-mediated default, which admits only on call. Well-formedness: §5.

§4.4.2a handler

handler ::= call_handler | http_handler | cron_handler | queue_handler | ws_open_handler | ws_close_handler | event_handler

A handler: a call, HTTP, cron, queue, WebSocket, or event entry point, matching the service’s protocol. Well-formedness: §5.

§4.4.3 call_handler

call_handler ::= "on" "call" identifier? "(" (param ("," param)*)? ","? ")" "->" type_ref by_clause? given_clause? block

on call, an optional name, parameters, ->, a return type, an optional given clause, and a block body.

§4.4.4 http_handler

http_handler ::= "on" http_method "(" string_literal ")" "(" (param ("," param)*)? ","? ")" "->" type_ref by_clause? given_clause? block

on <Method>("route") — an HTTP method-builder (the verb collapses verb+route into one config expression in the handler-config slot), then parameters, ->, a return type, an optional given clause, and a block body. Valid only in a from http service. Well-formedness: §5.

§4.4.5 http_method

http_method ::= "GET" | "POST" | "PUT" | "PATCH" | "DELETE"

The HTTP verbs a route may handle. Well-formedness: §5.

§4.4.6 cron_handler

cron_handler ::= "on" "schedule" "(" string_literal ")" "(" (param ("," param)*)? ","? ")" "->" type_ref by_clause? given_clause? block

on schedule("expr"), parameters, ->, a return type, an optional given clause, and a block body. Valid only in a from cron service. Well-formedness: §5.

§4.4.7 queue_handler

queue_handler ::= "on" "message" "(" (param ("," param)*)? ","? ")" "->" type_ref by_clause? given_clause? block

on message(message) — the bound queue lives on the service’s from queue("name") header. Parameters, -> Effect[QueueResult], an optional given clause, and a block body. Well-formedness: §5.

§4.4.7a WebSocket handlers (v0.103)

A from websocket(in: I, out: O) service declares the connection-lifecycle handlers on open, on message, and on close. Each is a handler head — on, the lifecycle keyword, parameters, -> Effect[()], a required by_clause naming the actor, an optional given clause, and a block body — and is valid only in a from websocket service:

on open — the upgrade handshake; the body sees an owned connection binding of type Connection[O].
on message — parameters end with the decoded inbound frame of type I.
on close — the connection ended.

on message reuses the queue_handler production. The grammar admits the by clause on every head as optional; that on open names its actor is well-formedness. Well-formedness — exactly one on open, edge authentication, held-resource disposal: §5.

ws_open_handler

ws_open_handler ::= "on" "open" "(" (param ("," param)*)? ","? ")" "->" type_ref by_clause? given_clause? block

on open, parameters, ->, a return type, optional by and given clauses, and a block body.

ws_close_handler

ws_close_handler ::= "on" "close" "(" (param ("," param)*)? ","? ")" "->" type_ref by_clause? given_clause? block

on close, with the same shape as on open (v0.106).

§4.4.7b Events subscriptions (v0.238)

A from Events(E) service subscribes to the event E (§4.1.12) and has one handler, on event. Its header may narrow delivery with a payload pattern, from Events(E { field: value, .. }) (v0.239), and with a version clause after the closing ), via schema(N) (v0.244); a header carries either, both, or neither. via is part of the Events protocol’s production, so via on any other protocol is a syntax error. Well-formedness: §5.7b.

event_handler

event_handler ::= "on" "event" "(" (param ("," param)*)? ","? ")" "->" type_ref by_clause? given_clause? block

on event, parameters (the payload, then optionally an EventEnvelope), ->, a return type, optional by and given clauses, and a block body.

event_pattern

event_pattern ::= "{" (event_pattern_field ",")* ".." "}"

A brace-delimited list of name: value fields closed by a required ... The pattern lists a subset of the event’s fields; { } with no fields is a parse error (bynk.parse.event_pattern_empty), and the unfiltered form is the bare from Events(E).

event_pattern_field

event_pattern_field ::= identifier ":" event_pattern_value

One name: value entry in an event_pattern.

event_pattern_value

event_pattern_value ::= "-"? number_literal | string_literal | boolean_literal | (identifier ".")? identifier

The value a field is matched against: an Int, String or Bool literal, or a variant reference, bare (Domestic) or qualified (Region.Domestic).

schema_dispatch_clause

schema_dispatch_clause ::= "via" "schema" "(" "-"? number_literal ")"

via schema(N). The grammar admits a signed number literal; that N is a positive Int is well-formedness (§5.7b). A range (via schema(2..)) is not part of the grammar.

§4.4.8 by_clause (v0.45)

by_clause ::= "by" (identifier ":")? identifier ("|" identifier)*

by (<binder>:)? <Actor> ("|" <Actor>)* — the actor(s) a handler consumes, positioned after the return type, alongside given (v0.155 relocated it from before the parameter list, where by <Actor> (…) read as a call) (on schedule("…") () -> … by s: Scheduler). The binder is optional (v0.50): by <name>: <Actor> captures the verified identity (read as <name>.identity); by <Actor> declares-and-verifies the contract without capturing it (anonymous or verify-and-discard). Omitting by entirely inherits the protocol’s default actor; on a from http handler by is required (the binder still optional).

A |-separated list of actors (v0.52) is an ordered sum of peer actors (by who: User | Visitor): the boundary tries each peer’s scheme in declared order and binds the first that verifies; the body matches on the resolved actor (the binder is required for a sum). Well-formedness: §5.

An actor is a nominal boundary contract — a closed, compiler-known authentication scheme plus an optional sealed identity — consumed by a handler’s by clause (§4.4.8). Actors are context-only.

§4.4.9 actor_decl (v0.45)

actor_decl ::= "actor" identifier ("{" "auth" "=" scheme scheme_config? ("," "identity" "=" type_ref)? "}" | "=" identifier "where" expression)

actor <Name> { auth = <Scheme> }, optionally , identity = <Type>. The refinement form actor <Name> = <Base> where <predicate> (v0.53) declares an authorisation invariant over a Bearer base; the predicate is a closed set of claim predicates (hasClaim, claimEquals). Well-formedness: §5.

§4.4.10 scheme

scheme ::= "None" | "Internal" | "Bearer" | "Signature" | "Oidc"

The closed authentication-scheme set. None, Internal, Bearer, Signature (v0.51), and Oidc (v0.151) are supported. The authenticated schemes carry a keyed-args config — Bearer(secret = "<ENV>"), Signature(secret = "<ENV>", header = "<Header>", (timestamp = "<Header>", tolerance = <seconds>)?), and Oidc(issuer = "<url>", audience = "<aud>", jwks = "<url>") — parsed by the scheme_config production (string- or integer-valued args; the checker validates which keys each scheme admits). Unlike Bearer/Signature, an Oidc config names no secret: its trust root is the provider’s public JWKS. Well-formedness: §5.

§4.4.10a scheme_config

scheme_config ::= "(" scheme_arg ("," scheme_arg)* ")"

The parenthesised, comma-separated key = value arguments an authenticated scheme carries.

§4.4.10b scheme_arg

scheme_arg ::= identifier "=" (string_literal | number_literal)

One key = value argument; the value is a string or integer literal. Which keys each scheme admits is well-formedness: §5.

§4.5 Agents

An agent is a keyed, stateful entity whose state lives in store fields that handlers read by name and write with :=.

§4.5.1 agent_decl

agent_decl ::= "agent" identifier "{" key_decl store_field* (invariant_decl | transition_decl)* (store_annotation* call_handler)* "}"

agent, a name, and a body holding a key declaration, store fields, zero or more invariants and transitions, and handlers — in that fixed order. Well-formedness: §5.

§4.5.2 key_decl

key_decl ::= "key" identifier ":" type_ref

key, an identifier, :, and a type — the agent’s identity.

§4.5.2a store_field

store_field ::= "store" identifier ":" store_kind store_annotation* ("=" expression)?

store, a name, :, a store_kind over its type parameters, zero or more store_annotations, and an optional = initialiser — a persistent field of the agent. Well-formedness — required initial value, kind validity: §5 (ADR 0108).

§4.5.2b store_kind

store_kind ::= identifier ("[" type_ref ("," type_ref)* "]")?

The closed catalogue of storage kinds: Cell, Map, Set, Cache, Log. The catalogue is closed — there is no Queue storage kind (ADR 0122).

§4.5.2c store_annotation

store_annotation ::= "@" identifier ("(" (annotation_arg ("," annotation_arg)*)? ","? ")")?

A @name(args) annotation between the kind and the initialiser — @ttl (on Cache), @retain (on Log), @indexed (on Map), @bounded. Arguments are compile-time literals. Well-formedness — kind match, known name: §5 (ADR 0111).

§4.5.2d annotation_arg

annotation_arg ::= (identifier ":")? expression

One annotation argument: an optional label: and a value expression, as in @indexed(by: id) (labelled) or @ttl(5.minutes) (positional). The grammar admits any expression; the checker restricts arguments to literals and the @indexed field-name labels (ADR 0111 D4).

§4.5.3 invariant_decl (v0.80)

invariant_decl ::= "invariant" identifier ":" expression

invariant, a name, :, and a predicate expression — a universally-quantified property that must hold of every committed state. Invariants form a phase between the store fields and the handlers; one after a handler is a parse error (bynk.parse.invariant_after_handler). The predicate references the agent’s store fields by bare name. Well-formedness — purity, Bool type, agent-locality: §5 (ADR 0107).

§4.5.4 transition_decl (v0.116)

transition_decl ::= "transition" identifier ":" expression

transition, a name, :, and a predicate expression — a step invariant over the agent’s old/new state pair. Transitions sit in the same phase as invariants (between the store fields and the handlers); one after a handler is a parse error (bynk.parse.transition_after_handler). The predicate reads state fields through the contextual old and new bindings (old.status, new.balance), which are ordinary identifiers outside a transition. Well-formedness — purity, Bool type, agent-locality, a genuine step reference: §5 (ADR 0151).

§4.6 Expressions

Bynk is expression-oriented: a block’s value is its final expression. Operator precedence is fixed by the binary_expr production (§4.6.7).

§4.6.1 expression

expression ::= if_expr | match_expr | is_expr | expect_expr | binary_expr | unary_expr | primary

Any expression: control flow, a refinement check, an operator expression, or a primary.

§4.6.2 primary

primary ::= lambda_expr | paren_expr | method_call | field_access | call | record_construction | record_spread | question_expr | ok_expr | err_expr | some_expr | none_expr | effect_pure_expr | val_expr | wire_expr | trace_expr | list_literal | block | number_literal | float_literal | string_literal | boolean_literal | unit_literal | self_expr | identifier

The atomic and postfix expressions: literals, names, calls, field and method access, constructors, and parenthesised expressions.

§4.6.3 if_expr

if_expr ::= "if" expression block ("else" (if_expr | block))?

if, a condition, a block, and an optional else arm (either a further if or a block). A missing else defaults to () (v0.146, ADR 0170) and is legal only when the then-branch is unit (() / Effect[()]); a value-producing if still requires its else. Well-formedness: §5.

§4.6.4 match_expr

match_expr ::= "match" expression "{" match_arm* "}"

match, a scrutinee, and a brace-delimited list of match arms. Well-formedness — including exhaustiveness: §5.

§4.6.5 is_expr

is_expr ::= expression "is" pattern

An expression, is, and a pattern. Well-formedness — including the narrowing it introduces: §5.

§4.6.6 binary_expr

binary_expr ::= expression "implies" expression | expression "||" expression | expression "&&" expression | expression ("==" | "!=") expression | expression ("<" | "<=" | ">" | ">=") expression | expression ("+" | "-") expression | expression ("*" | "/") expression

The binary operators, listed from lowest precedence (implies, then ||) to highest (*, /); the production order is the precedence order. implies (v0.80) is logical implication, right-associative, P implies Q ≡ !P || Q. Well-formedness: §5.

v0.130 (ADR 0158): a +/- that begins a new line does not continue the additive chain — it starts a new construct instead, so a comma-less match arm beginning with a negative literal pattern (10 ⏎ -2 => …) reads as two arms, not 10 - 2. This applies only at the +/- level; * and / continue across a line break as usual. Like the same-line [ rule for type application (§4.6.8, §4.6.10, §4.6.21a), this is a case where a line break is syntactically significant — see §3.4.

§4.6.7 unary_expr

unary_expr ::= ("!" | "-") expression

Logical negation ! and numeric negation -, prefixed to an expression.

§4.6.8 method_call

method_call ::= primary "." identifier ("[" type_ref ("," type_ref)* "]")? "(" (expression ("," expression)*)? ","? ")"

A receiver, ., a method name, and parenthesised arguments. Well-formedness: §5.

v0.22a: the numeric base-type keywords Int and Float are admitted in static-receiver position — Int.parse(s) / Float.parse(s) — but only when immediately followed by .; a bare Int in expression position remains a parse error. (List.empty() needs no such rule: List is lexically an ordinary identifier.)

v0.22b: a method call accepts explicit type arguments — Json.decode[Order](s) — under the same same-line-[ rule as call type application (0039): a [ opening a new line is a list literal. In v0.22b only the Json.decode static consumes them; type arguments on any other method are bynk.generics.type_arg_mismatch (generic user methods remain deferred). The bare name[T] value form stays reserved.

§4.6.9 field_access

field_access ::= primary "." identifier

A receiver, ., and a field name. Well-formedness: §5.

§4.6.9a lambda_expr

lambda_expr ::= "(" (lambda_param ("," lambda_param)*)? ")" "=>" (expression | block)

A lambda (v0.20a): (o) => o.paid, (acc, t) => acc + t, () => 0, or with a block body (o) => { … }. Always parenthesised; => is the value arrow, shared with match arms — -> stays the type arrow. Well-formedness (contextual parameter typing, the unannotated rule, bottom-up effectfulness): §5.

§4.6.9b lambda_param

lambda_param ::= identifier (":" type_ref)?

One lambda parameter with an optional type annotation — optional because an expected function type supplies it; required in unconstrained positions (§5).

§4.6.10 call

call ::= identifier ("[" type_ref ("," type_ref)* "]")? "(" (expression ("," expression)*)? ","? ")"

A name, optional bracketed type arguments (v0.20a, name[T](…) — the explicit-instantiation form; a bare name[T] without an argument list is a reserved parse error), and parenthesised arguments — a function call, a variant construction, an agent instantiation, or (v0.20a) the application of a function-typed value in scope. Well-formedness: §5.

§4.6.11 record_construction

record_construction ::= identifier "{" (field_init ("," field_init)*)? ","? "}"

A type name and a brace-delimited list of field initialisers. Well-formedness: §5.

§4.6.12 field_init

field_init ::= identifier ":" expression | identifier

One field of a record construction: name: value, or the shorthand name.

§4.6.13 record_spread

record_spread ::= identifier "{" "..." expression ("," field_init)* ","? "}" | "{" "..." expression ("," field_init)* ","? "}"

A ... spread of an existing record, optionally overriding fields, with or without a leading type name. Well-formedness: §5.

§4.6.14 question_expr

question_expr ::= expression "?"

An expression followed by ?. Well-formedness: §5.

§4.6.15 ok_expr

ok_expr ::= "Ok" "(" expression ")"

Ok(…) — the success constructor of Result or HttpResult. Well-formedness: §5.

§4.6.16 err_expr

err_expr ::= "Err" "(" expression ")"

Err(…) — the failure constructor of Result. Well-formedness: §5.

§4.6.17 some_expr

some_expr ::= "Some" "(" expression ")"

Some(…) — the present constructor of Option. Well-formedness: §5.

§4.6.18 none_expr

none_expr ::= "None"

None — the absent constructor of Option.

§4.6.19 effect_pure_expr

effect_pure_expr ::= "Effect" "." "pure" "(" expression ")"

Effect.pure(…) — lifts a pure value into an Effect.

§4.6.20 val_expr

val_expr ::= "Val" "[" type_ref "]" val_arg?

Val[T] with an optional pin argument (v0.114, retiring Mock[T]). Well-formedness — including that it is valid only in test bodies: §5.

§4.6.21 val_arg

val_arg ::= "(" expression ("," expression)* ","? ")" | "{" (field_init ("," field_init)*)? ","? "}"

The pin to a Val[T]: positional arguments or a brace-delimited record of field pins.

§4.6.21a list_literal

list_literal ::= "[" (expression ("," expression)* ","?)? "]"

(v0.20b) [a, b, c], with an optional trailing comma — a leading [ in expression position. It does not collide with explicit type application (name[T](…), §4.6.10): that [ is a postfix form on a callee identifier and MUST sit on the same line as it — a [ opening a new line starts a list literal. There is no Map literal ({ } is records and blocks) and no indexing form (get(i) returns Option[T]). Well-formedness — including empty-literal element-type inference: §5.10.

§4.6.22 paren_expr

paren_expr ::= "(" expression ")"

A parenthesised expression, for grouping.

§4.6.23 self_expr

self_expr ::= "self"

self — the receiver inside a method or agent handler. Well-formedness: §5.

§4.6.24 wire_expr

wire_expr ::= "Wire" "(" expression ")"

Wire(<expr>) — a raw, unvalidated argument to a service address in a system-tier case (§4.9): the String is the wire form the boundary receives, a JSON body or a path segment, so a case can drive the router with input the type system forbids. Its placement is well-formedness: §5.9.

§4.7 Patterns & matching

The patterns used in match arms and is checks.

§4.7.1 match_arm

match_arm ::= (pattern | refined_pattern) ("if" expression)? "=>" expression ","?

A pattern, an optional if guard (an arbitrary Bool expression over the pattern’s bindings), =>, a result expression, and an optional trailing comma — arm separators are optional. An arm’s pattern may also be a refined pattern (§4.7.10), which only a match arm admits: it is not one of the _pattern forms, so it cannot appear after is or as an alternative or sub-pattern. Well-formedness: §5.

§4.7.2 pattern

pattern ::= wildcard_pattern | literal_pattern | variant_pattern | or_pattern | paren_pattern

A pattern: a wildcard, a literal, a binding, a variant pattern, an or-pattern, or a parenthesised pattern. A lowercase-led identifier is a binding (it matches anything and binds the value); an uppercase-led one is a nullary variant — in the concrete grammar both parse as variant_pattern.

§4.7.3 variant_pattern

variant_pattern ::= (identifier ".")? identifier ("(" (pattern_binding ("," pattern_binding)*)? ","? ")")?

A name, optionally qualified, with an optional parenthesised list of bindings. The name is an identifier, not a constant name: a lowercase-led identifier binds the value, an uppercase-led one discriminates a variant. Well-formedness: §5.

§4.7.4 wildcard_pattern

wildcard_pattern ::= "_"

_ — matches anything and binds nothing.

§4.7.5 pattern_binding

pattern_binding ::= named_binding | pattern

A binding within a variant pattern: a named binding, or a full sub-pattern matched against the payload field (one recursion point). A lowercase-led identifier binds the field, an uppercase-led one discriminates a nested nullary variant (Err(PollClosed)), _ ignores it, and a nested variant recurses (Some(Ok(x))). Well-formedness: §5.

§4.7.6 named_binding

named_binding ::= identifier ":" pattern

Binds a payload field by name, matching it against a sub-pattern: field: name, or field: _ to ignore it.

§4.7.7 literal_pattern

literal_pattern ::= "-"? number_literal | string_literal | boolean_literal

An integer (optionally negated), a string, or a boolean, matching a primitive scrutinee by value. Exhaustiveness: §5.6.

§4.7.8 or_pattern

or_pattern ::= pattern "|" pattern

p₁ | p₂, left-associative: matches if either alternative matches. | here is a pattern operator, distinct from boolean ||. That every alternative binds the same names at the same types, against one value type, is well-formedness: §5.6.

§4.7.9 paren_pattern

paren_pattern ::= "(" pattern ")"

A pattern in parentheses: transparent grouping, most useful around an or-pattern. It never admits a refined pattern inside.

§4.7.10 refined_pattern

refined_pattern ::= wildcard_pattern "where" refinement

_ where predicate — a runtime guard on a match arm, reusing the refinement-predicate catalogue of §4.2.11. The inner form is the wildcard only: any other inner pattern, (p₁ | p₂) included, is bynk.parse.refined_pattern_inner. Its scrutinee types and exhaustiveness are well-formedness: §5.6.

§4.8 Statements

A block is a sequence of statements ending in an optional value expression.

§4.8.1 block

block ::= "{" statement* expression? "}"

A brace-delimited sequence of statements with an optional trailing expression, which is the block’s value. A block with no trailing expression has the implicit value () (unit) — the parser synthesises a () tail (v0.146, ADR 0170); an empty block {} is therefore the unit value.

§4.8.2 statement

statement ::= let_stmt | effect_let_stmt | effect_send_stmt | do_stmt | assign_stmt | expect_expr

A statement: a let, an effectful let, an asynchronous send (~>), a do effect statement, a := store write, or an assertion.

§4.8.3 let_stmt

let_stmt ::= "let" binding_name (":" type_ref)? "=" expression

let, a binding name, an optional type annotation, =, and an expression. Well-formedness: §5.

§4.8.4 effect_let_stmt

effect_let_stmt ::= "let" binding_name (":" type_ref)? "<-" expression call_site_actor?

let, a binding name, an optional type annotation, <-, and an effect expression. Well-formedness: §5.

§4.8.5 effect_send_stmt

effect_send_stmt ::= "~>" expression

~> and an effect expression — an asynchronous send. Unlike an effect_let_stmt it carries no binder: the reply is not awaited and nothing is bound. Well-formedness — including the requirement that the reply be Effect[()] (the error gate): §5.

§4.8.6 do_stmt (v0.146)

do_stmt ::= "do" expression

do and an effect expression — a unit effect statement (ADR 0170). Like an effect_send_stmt it carries no binder; unlike it, the effect is awaited and joins the enclosing computation. The binder-free spelling of let _ <- e when the awaited value is unit. Well-formedness — including the requirement that the operand be Effect[()] (a valued reply keeps the explicit let _ <- e): §5.

§4.8.7 assign_stmt (v0.81)

assign_stmt ::= identifier ":=" expression

An identifier, :=, and an expression — a Cell store write. Well-formedness — including that the target is a store Cell field and the right-hand side does not read it: §5 (ADR 0108).

§4.8.8 expect_expr

expect_expr ::= "expect" (observation_expr | faults_expr | expression)

expect and a Bool predicate, or — inside a case — an observation_expr or a faults_expr. Well-formedness: §5.

§4.8.9 observation_expr (v0.117)

observation_expr ::= identifier "." identifier ("called" ("once" | number_literal "times")? ("with" expression)? | "never" "called" | "before" identifier "." identifier)

An observation over a capability seam: a Cap.op subject (the capability and one of its operations, named, not called) followed by a matcher — called (optionally once / <n> times, optionally with <predicate>), never called, or before Cap.op. The matcher words called, never, once, times, with, before are contextual: outside an observation clause they are ordinary identifiers. A with predicate reads the operation’s parameters by their declared names. Well-formedness — seam resolution, with scope and purity: §5.

§4.8.9a faults_expr

faults_expr ::= expression "faults"

A fault claim (#1706): an effectful call followed by faults, claiming that awaiting the call throws rather than returns. faults is contextual: outside an expect subject it is an ordinary identifier. Well-formedness — the subject is a call of type Effect[_], and the claim is not made at the system tier: §5.

§4.8.9 trace_expr (v0.117)

trace_expr ::= "trace" "(" identifier "." identifier ")"

trace(Cap.op) — a test-only builtin yielding the recorded calls of a capability operation as a List of per-operation call records, in call order. trace is an ordinary identifier outside a case. Well-formedness: §5.

§4.8.10 binding_name

binding_name ::= identifier | "_"

The name bound by a let: an identifier, or _ to discard the value.

§4.9 Testing constructs

Cases, tiers, and provider overrides. See also the top-level suite_decl (§4.1.7).

§4.9.1 case

case ::= "case" string_literal ("as" ("unit" | "integration" | "system"))? "{" stub_clause* statement* expression? "}"

case, a description string, an optional as <tier> clause (unit | integration | system; unit is the default and elided), and a block body whose leading items may be case-scoped stub clauses. Well-formedness: §5.

§4.9.2 stub_clause

stub_clause ::= "stub" identifier "." identifier "(" (("_" | expression) ("," ("_" | expression))* ","?)? ")" ("returns" "each" "[" (("fails" | expression) ("," ("fails" | expression))* ","?)? "]" | "returns" expression | "fails")

A per-seam provider override: stub, a capability, ., a method, a parenthesised argument-pattern list (_ or a value per parameter), and a right-hand side — returns <value>, returns each [<outcome>, …], or fails. Legal at suite and case scope. Well-formedness: §5.

§4.9.3 property_decl (v0.114)

property_decl ::= "property" string_literal "{" for_all "}"

property, a description string, and a block holding one for all binder: the generative sibling of case, whose subjects the runner produces. Well-formedness: §5.9a.

§4.9.4 for_all

for_all ::= "for" "all" for_all_binding ("," for_all_binding)* ("where" expression)? block

for all, one or more comma-separated bindings, an optional where filter expression, and a block body of expects.

§4.9.5 for_all_binding

for_all_binding ::= identifier ":" type_ref

name: Type — binds name to a generated inhabitant of Type.

§4.9.6 call_site_actor (v0.182)

call_site_actor ::= "by" identifier ("(" expression ")")?

by <Actor> or by <Actor>(<identity>) in a case body: the actor the case acts as when it drives a service handler, with its identity value. Distinct from the handler’s by_clause, which binds an actor and carries no identity argument. Well-formedness: §5.9.