Skip to main content

exch

One interaction between two components: the send and the matching receive as a single step of a global protocol.

component Radar;
component CommandPost;

message struct TrackReport {
    track_id: uint32;
}

global protocol Report {
    exch any TrackReport from Radar to CommandPost;
}

Payloads​

The sending half takes the same forms as send, and an optional into describes the receiving half with the forms of recv. Omit the into and the receiver is read off the sending half.

  • into is what says where the message lands and what the receiver assumes. Write it when the exchange binds the message for later statements, or when the receiver's assuming differs from the sender's where.
  • into let name: T introduces a binding visible to later statements. A bare into name names a binding that already exists.
  • Both endpoints have to be fixed, though not written: an omitted from or to comes from the on connection, so exch any TrackReport on TrackFeed; fixes both.
  • The message type is message data on both halves, and the sending half's type is assignable to the into target's type. Assignable, not identical — a receiver may name an ancestor of what is sent.
component Radar;
component CommandPost;

message struct TrackReport {
    track_id: uint32;
    bearing_deg: float32;
}

message struct EngageOrder {
    track_id: uint32;
}

connection TrackFeed from Radar to CommandPost;

global protocol Report {
    exch any TrackReport on TrackFeed;
    exch any TrackReport into let latest: TrackReport from Radar to CommandPost;
    exch any report: TrackReport where report.bearing_deg >= 0.0
        into any accepted: TrackReport assuming accepted.bearing_deg >= 0.0
        from Radar to CommandPost;
    exch EngageOrder { track_id = latest.track_id; } from CommandPost to Radar;
}

Compatibility​

The sender's where and the receiver's assuming are the two halves of one claim about the value on the wire. The exchange is compatible when everything the sender may produce is something the receiver accepts, given the statements before it.

  • An exchange with neither predicate makes no claim, and is compatible.
  • A where that is weaker than the assuming is not: the sender may produce a value the receiver treats as a safety error.
  • Which endpoints an exchange connects also decides which earlier in block bindings it can name. An endpoint derived from a connection involves its component exactly as a written one does.

Errors​

An exchange that fixes only one endpoint​

Neither a written endpoint nor an on connection supplies the receiver here.

component Radar;
component CommandPost;

message struct TrackReport {
    track_id: uint32;
}

global protocol Report {
    exch any TrackReport from Radar;   // error: exch-from-to-required
}

An into target that is not a binding​

component Radar;
component CommandPost;

message struct TrackReport {
    track_id: uint32;
}

global protocol Report {
    exch any TrackReport into TrackReport from Radar to CommandPost;   // error: exch-into-target-not-var
}

Two halves that disagree about the message​

component Radar;
component CommandPost;

message struct TrackReport {
    track_id: uint32;
}

message struct Ack {
    track_id: uint32;
}

global protocol Report {
    exch any TrackReport into let ack: Ack from Radar to CommandPost;   // error: exch-type-mismatch
}
  • send — the sending half on its own, in a local protocol.
  • recv — the receiving half on its own.
  • global protocol — the statement sequence an exch belongs to.
  • connection — the clause that fixes the endpoints.