Effects

A handler is a message tag plus a list of effects:

structure RHandler where
  tag  : String
  effs : List Eff

Effects are applied left to right by applyEff, each taking the current Doc and the message Payload and returning a new Doc. Nothing here performs I/O — an Eff is a description of a state change, which is what makes a handler decidable and therefore provable.

def reflStep (hs : List RHandler) (tag : String) (payload : Payload) (d : Doc) : Doc :=
  match hs.find? (fun h => h.tag == tag) with
  | some h => h.effs.foldl (fun d e => applyEff payload d e) d
  | none   => d          -- an unknown tag is a no-op, not a crash

Payloads

inductive Payload where
  | atom : Atom → Payload   -- most messages: a scalar
  | row  : Row → Payload    -- selecting a list row: the whole row

Payload.asAtom projects the scalar (.null for a row); Payload.field k reads a field from a row payload (.null for an atom). Row payloads are what let a handler lift a selected row's fields into scalars — selecting a conversation, a contact, an app.

The domain-free core

These carry no assumptions about what your app is about. A non-messaging app should be able to express itself with these alone.

Effect	Meaning
`setConst field value`	`field := value`
`setInput field`	`field := payload` (the scalar payload)
`setFromRow field from`	`field := payloadRow[from]`
`setFromScalar field from`	`field := scalars[from]`
`appendFromScalars table consts scalarFields`	append a row built from constant fields plus `(rowField := getScalar src)` pairs
`appendFromScalarsIfAbsent table consts scalarFields keyField`	the same, unless an existing row's `keyField` already equals the built row's — a dedup that keeps the original row position on a re-add
`appendFromRow table consts rowFields`	append a row of constants plus `(destField := payloadRow[srcField])`
`removeWhereField table field`	drop rows whose `field` equals the payload row's `field`
`lookupRoute target table field foundPath notFoundPath`	if scalar `target` is non-empty and matches some row's `field`, set `chat_with := target` and route to `foundPath`; else route to `notFoundPath`

appendFromScalars is the general row-builder. Example — an issue tracker creating a ticket from three input scalars:

⟨"create_issue",
  [ .appendFromScalars "issues"
      [("state", .str "open"), ("votes", .int 0)]        -- constants
      [("title", "title_draft"), ("body", "body_draft")]  -- field := scalar
  , .setConst "title_draft" .null
  , .setConst "body_draft"  .null ]⟩

The messaging-shaped effects

These exist because the framework's first apps were chat apps, and they bake that domain into the framework rather than into app data. They are convenient if you are building messaging and a dead end if you are not.

Effect	What it hard-codes
`pushDraft table`	appends `postRow` — a row of `from`, `body` (from the `draft` scalar), `media`, `trailing`, `outgoing`
`pushInput`	the same row, into the table named by the payload
`pushInputWith tags`	`pushInput` plus `(rowField := scalar)` tags
`setConvId`	`conv_id := group ? chat_with : canonical(identity, chat_with)`
`pushConvMessage`	appends to a table literally named `"messages"`, with fields `from`, `body`, `conv`, `trailing`
`routeIfHex64 target validPath invalidPath`	routes on whether a scalar is a well-formed 64-hex pubkey

postRow is defined in Encapp/AppGen.lean:

def postRow (d : Doc) : Row :=
  let id := short16 (asStr (d.getScalar "identity"))
  [ ("from", .str id), ("body", d.getScalar "draft"), ("media", .str id),
    ("trailing", .str "now"), ("outgoing", .bool true) ]

Domain-specific conveniences

Effect	Meaning
`likeRow table matchField`	toggles a `likes` count between 0 and 1 on the row whose `matchField` matches the payload row's

Emission

Every Eff has a JSON form (effJson) that the emitted runtime interprets. The JS side is the operational mirror of applyEff — same names, same order, same semantics. That correspondence is checked empirically rather than proven; see What is proven.

{"k":"appendFromScalars","table":"issues",
 "consts":[{"f":"state","v":"open"}],
 "scalars":[{"f":"title","src":"title_draft"}]}

Writing handlers well

Order matters. Effects fold left to right, so .setConst "draft" .null must come after the effect that consumes the draft.
Prefer declarative over clever. An effect list is data a reader can audit; a chain of interdependent effects is not.
Every handler needs a workflow. handler-coverage.mjs fails the gate on any tag no workflow fires — an unfired handler is untested surface. See Testing.

Recap

Effects are data describing state changes; handlers apply them left to right via foldl.
Payloads carry scalar atoms or whole rows; row payloads lift fields into scalars.
Domain-free effects (setConst, appendFromScalars, etc.) work in any app; avoid messaging-shaped effects unless you're building chat.
Each effect has a JSON form (effJson) that the JS runtime interprets as the operational mirror of applyEff.
Order matters: effects fold left to right, so side effects must be declared before consumption.
Every handler must be exercised by a workflow; uncovered tags fail the gate.

Next steps

App model — authoring the typed face whose update becomes the handler table
Views — buttons that fire handlers with scalar or row payloads
Workflows — testing effects with step-by-step state assertions