Views

A view is a finite tree drawn from a closed vocabulary. Closed is the point: because the set of constructors is fixed, exactly one generic interpreter per platform can render any app, and there is never per-screen render code to write, test or let drift.

Two types, same shape:

View Msg — the authored, typed face. A button carries a real Msg value.
RView — the reflected face. A button carries a (tag, payload) pair.

reflectView mechanically converts one to the other, defunctionalizing messages. You author in View Msg when you want type safety, or directly in RView (with ViewDsl) when a screen is mostly layout.

The minimal vocabulary

Constructor	Renders
`text s`	static text
`scalar k`	the live value of scalar `k`
`rowField k`	field `k` of the current row (inside a `list`)
`input k`	a text input two-way bound to scalar `k`
`button label tag payload`	a button that fires `step(tag, payload)`
`list table item`	`item`, once per row of `table`
`col children`	a container

The styled vocabulary

The styled group is what lets an entire product — chrome, shell, every screen — be authored as view data carrying its own inline style, so nothing downstream is hand-written.

Constructor	Renders
`raw s`	a bare text node, no wrapper
`el tag style children`	an arbitrary element with inline style
`elAttr tag attrs children`	an element with arbitrary attributes, including SVG namespacing — this is how line-art icons are expressed as data
`img src style`	an image
`styled style child`	wraps a node in an inline style
`btn label style tag payload`	a styled button
`click style tag payload children`	a clickable styled container
`rowSelect style tag children`	a list item that fires `tag` with the whole row as payload
`inp field placeholder style`	a styled input bound to `field`
`rowFieldOr key fallback`	a row field, or a literal when absent

Lists and derived views

Constructor	Renders
`list table item`	every row
`listWhere table field scalarKey item`	rows where `row[field]` equals `scalars[scalarKey]` — a filtered view without a filtered table
`listDistinct table field item`	one item per distinct value of `field`, using the latest row — conversation lists, grouped feeds
`listOrEmpty table item empty`	every row, or the `empty` view when the table has none

listOrEmpty exists because empty states are a real screen users see, and a framework without one pushes authors into hand-written conditionals.

Conditionals

Constructor	Renders
`cond scalarKey then else`	branch on whether a scalar is truthy
`condEq scalarKey value then else`	branch on `scalars[key] == value`
`condField field then else`	branch on whether the current row's `field` is truthy
`condFieldEqScalar field scalarKey then else`	branch on `row[field] == scalars[key]` — this is how "is this message mine?" is expressed: `from == identity`

Conditionals are view constructs, not logic. Keep decisions that change state in handlers; keep decisions that change appearance here.

Routing is not a constructor

There is no route atom. A view function dispatches on a scalar:

def helloView (d : Doc) : View HMsg :=
  match asStr (d.getScalar "path") with
  | "/feed"     => …
  | "/my_posts" => …
  | _           => .text ""

and the reflected app stores one RView per path in pages. This keeps the vocabulary small and puts the routing decision in one readable place. See Routing and gates.

Rendering

The renderer is the documented atom→node boundary, and there is one per platform:

appDomJs maps each constructor to a DOM node and wires events to step;
appRnJs maps the same constructors to React Native elements.

Both consume the identical appCoreJs state machine, and test/native-core-identity.mjs asserts the two emitted cores are byte-identical. Style handling is the one genuinely different part — the web takes inline CSS strings directly, while the native emitter parses them into RN style objects, which is why emitNative accepts base-style parameters and why test/fuzz-parity.mjs fuzzes styling specifically.

Proving view facts

Because a view is data, you can prove things about it. This catches the copy-paste bug where a page lists the wrong table:

theorem helloView_feed_lists_messages :
    firstListTable (helloView (helloInit.setScalar "path" (.str "/feed")))
      = some "messages" := by native_decide

For assertions about the rendered page rather than the view value, use a workflow's ui checks (seesText, namedControl), which the replayers evaluate against the live DOM. Those are replay-only and deliberately not part of the native_decide proof — see Workflows.

Recap

Views are finite trees from a closed vocabulary: text, scalars, inputs, buttons, lists, and conditionals.
Two types with the same shape: View Msg (typed) and RView (reflected for codegen).
Conditionals branch on scalars or row fields; routing is scalar dispatch via match, not a constructor.
The vocabulary is small enough for one generic renderer per platform (DOM, React Native).
Views are data, so you can prove facts about them — catching copy-paste bugs at compile time.
Styling is inline on web; the native emitter parses it into RN style objects.

Next steps

Effects — how handlers transform state via the Eff algebra
Routing and gates — pages as data and guards that enforce entry sequences
Workflows — testing views with cross-platform UI assertions