Sky.Spa — client-side TEA (overview)

When to use Sky.Spa vs Sky.Live

Sky.Live keeps the loop on the server: per-user Model, a live SSE per session, a full server-side re-render each interaction. It scales, but the ceiling is the stateful fleet (sticky sessions, session store, SSE fan-out). Sky.Spa moves the loop to the client, which changes the trade:

Reach for Sky.Spa when pure UI transitions should be instant and local (rich client-side interaction), the backend can be a stateless API, and the delivery target is a desktop/mobile-embed webview where a one-time wasm download is fine. Stay on Sky.Live for a browser web app today — its first paint is server HTML, not a multi-megabyte wasm blob.

The programming model — same as Sky.Live

An app is written exactly like a Sky.Live / web App.app; only the build --target (a client wasm backend) and a Model-shape convention change. The four TEA fields go in App.app; routing and the server boundary are attached with App.withX builders (exactly like the web target's optionals):

appDef =
    App.app
        { init = Model.init
        , update = Update.update      -- pure branches run on the CLIENT
        , view = View.view            -- Std.Ui Element, painted client-side to the DOM
        , subscriptions = Subs.subs   -- Sub.every timers, reconciled after each update
        }
        |> App.withRoutes
            [ App.route "/" All
            , App.route "/active" Active
            , App.route "/completed" Completed
            ]
        |> App.withNotFound NotFound


main =
    App.run appDef       -- built --target web:app  (runner-direct: App.runSpa appDef)

view is Std.Ui (the default — see the pinned defaults in AGENTS.md), not Std.Html: the Sky.Spa client renderer paints any Element tree to the DOM, so the same view could target Sky.Live (web), Sky.Tui (terminal), or Sky.Webview (desktop).

Model = { ui, data } — source of truth, not "where it lives"

In Sky.Spa the entire Model is client-owned (the loop runs on the client), so the useful declaration is source of truth, expressed structurally:

type alias Model =
    { page : Page       -- the routed page (the router sets it)
    , ui   : Ui         -- client-owned, ephemeral, NEVER serialized (no codec)
    , data : DataCache  -- a cached projection of server truth (has a Std.Codec)
    }

The wire boundary falls out of the types: things in data have a Std.Codec (they cross the network and hit the DB); things in ui are plain Sky types with no codec (they never leave the client). "Has a codec ⇒ server-backed" is the boundary. Sky removed RemoteData pre-v1, so model the fetch lifecycle with an explicit ADT (Loading | Loaded a | Failed Error | Stale a) rather than a magic wrapper.

v1 does not auto-enforce the { ui, data } split — that is the v2 auto-split (auto-split.md). v1 apps follow the discipline by hand, which keeps them forward-compatible with the v2 mechanism.

The server boundary — generated, with an explicit low-level form

Under a client --target the auto-split derives the boundary for you: an ordinary effectful update branch becomes a generated POST /_rpc/<Msg> (pure → client, any effect → server; see auto-split.md) over a Std.Codec shared with the backend — one type, one codec, one wire contract, no OpenAPI/TS drift. The low-level, explicit form — talk to a stateless Sky backend by hand with Std.Spa.getJson / postJson, decoding with that same codec — is what the generated code uses under the hood:

Refresh ->
    ( { model | ui = setStatus Loading model.ui }
    , Spa.getJson todosCodec "/api/todos" GotTodos )

GotTodos (Ok todos) -> ( { model | data = { todos = todos } }, Cmd.none )
GotTodos (Err e)    -> ( { model | ui = setStatus (Failed e) model.ui }, Cmd.none )

The idiom that makes the wire contract literally one file: put the shared types + codecs in a single Shared.sky and symlink it into both the client and server projects. Add a field there and both the client and server stop compiling — that is the whole point.

getJson / postJson are ordinary Sky over Cmd.perform + Http + Codec (no new runtime kernel). They hand update a Result Error a directly (a 2xx + decoded body, or an Err — a non-2xx status, a decode failure, and a network failure are all Err), so the app writes one case, not two.

How the client paints and handles events

The client renders with the same diff as Sky.Live (input-authority protocol §Patch operations): children are matched by key (Std.Ui.Keyed, a named field) or by shape, and a matched child keeps its DOM node, so a focused input keeps its focus, caret and typing when something is inserted above it. Event payloads follow Sky.Live's convention: onKeyDown / onKeyUp / onKeyPress get event.key, onCheck gets the checkbox's Bool, input / change get the value. A control's value is written only when the rendered value changes (Elm semantics): when update refuses an edit, the field keeps what the user typed. While an IME composition is open the field's input events are not dispatched; the committed text is, once. A server-painted first page is adopted (hydrated) only when it shows exactly what the client's first view says; otherwise the client builds the page itself. Adjacent texts (text "Hello, " next to text name) arrive as one browser text node, and hydration splits that node at the client's boundaries; the server's nodes stay in the page.

A widget island (Ui.island, Std.Ui overview) works the same as on Sky.Live. The boot loader carries the island runtime, so a widget file loaded with <script defer> can register before the wasm boots. The client keeps the widget's element when it rebuilds the island's parent, hands a widget event's detail to the Sky decoder, and delivers Cmd.toIsland after the update (a microtask). A Cmd.toIsland returned by a server branch cannot reach the browser: the backend logs SpaIslandCommandOnServer. Any other CustomEvent with a detail reaches its handler decoded the way the Sky.Live server decodes a wire argument.

App.withHead applies on every page. On an SSR page the backend renders it. On the static dist/index.html shell (an app whose backend has no per-request work, or a static host) the client applies it once at boot, from the first model, as Sky.Live does on its first load. Before v0.27.0 the head was dropped on the static shell.

Msg order and server calls — the ordering contract

The client keeps Sky.Live's TEA contract: every Msg's update runs exactly once, in arrival order, and the Cmds it returns run. A server branch (an auto-split POST /_rpc/<Msg>) keeps that contract; it never makes another Msg run twice or out of order, and it never drops a Cmd. There are two kinds, and the split picks the kind from the arm (runtime-go/rt/spa_rpcqueue.go):

• Async (Spa.rpc) — the arm's own model write is empty or reads no server data. The client runs that write itself when the Msg runs, exactly as Sky.Live does, and sends the request at once. The response comes back later as a Msg of its own (Applied<Msg>, then the result Msg of a Cmd.perform serverTask ResultMsg) and runs in arrival order, like any Cmd.perform result. Msgs that arrive meanwhile run at once, once each, against the current model, with their Cmds. Several async RPCs can be in flight together, and their results run in the order they arrive.

  Poll ->                                    -- async: the client sets `polling`
      ( { model | polling = True }
      , Cmd.perform (Relay.read model.room) Got )
  
  Got (Ok data) ->                           -- a client arm: runs when the read
      ( { model | polling = False, inbox = data :: model.inbox }, Cmd.none )
  

• Hold (Spa.rpcHold) — the arm's own model write needs server data (an inline Task.run, a server-tainted value), or its continuation arms settle on the server (a server-internal chain). Sky.Live runs such an update as one synchronous step: nothing else runs on the session until it returns. The client does the same: Msgs that arrive while a hold RPC is in flight wait, in order, and run once each, with their Cmds, after its response. The response's follow-up Msgs (the results of the branch's own server Cmds) run first. So two quick Inc clicks count to 2, and a draft typed during a Save is applied after it.

What this rules out, and why it matters: before v0.27.0 the client applied Msgs during an RPC and then re-ran them on top of the response. A client arm that spends a single-use value (a Noise.encrypt on the model's transport) failed the second time ("this state value was already used"), and a Msg that decided on a field the response changed (a timer tick that starts a call when busy is False) decided again, differently, and its new Cmd never ran.

Per-arm guarantees, in one list:

• a client arm runs once, when its Msg arrives, with its Cmds;
• an async server arm's own write runs in the client when its Msg arrives; its result runs when the response arrives;
• a hold server arm holds every later Msg until its response has run;
• a server arm's continuation whose own arm is client (reaches no server effect) runs in the client when the task's result arrives, on the model the client holds then, never on the server from a send-time copy;
• a chain that passes through a server hop (a continuation that itself reads server data) settles whole on the server, in one hold RPC: one round trip, and no Msg runs between its hops;
• a request is built from the model the Msg ran on, and a retry re-sends the same request (the backend's dedupe cache answers it without running the effect twice).

Write a long wait as an async arm. A long poll or a slow relay read belongs in a Cmd.perform from an arm whose model write reads no server data; the client then keeps running while it waits, and other server calls go out beside it. An arm that writes a server value into the model holds the client for its whole round trip.

A failed task is a result, not a console error. A client-local Cmd.perform whose task fails (Task.fail, a Std.Native call in a browser with no native shell, a client Http call) delivers its Err to the Msg you gave it, like an Ok; the client logs nothing. A server call that fails (a 5xx, a response the codec cannot decode) goes to App.withRpcError when the app declares it. Without that handler the client keeps the model and writes [sky.spa] RPC failed; kept last good model (no app-level handler …) once (the generated Applied<Msg> (Err e) arm returns Spa.reportRpcFailure e). A network error is re-sent by the runtime (see Network resilience below) and shows the Retry bar only once its retry budget is spent.

Network resilience — offline, sleep and overload are the runtime's job

A phone that switches apps, a laptop that sleeps, a radio that wakes up late, a proxy that answers 503 for a second during a deploy: each fails one request at the network level. The client handles this by itself; the app writes no retry code and no network banner (v0.27.3, runtime-go/rt/spa_retry.go).

• Transient or final. No answer, a timeout (a request that does not settle in 30 s is aborted) and the statuses 408, 425, 429, 502, 503 and 504 are TRANSIENT. Every other answer is FINAL and reaches the app as before.
• Re-sent by the runtime. Every server call is safe to re-send: it carries a request id, and the backend answers a repeated id from its dedupe cache without running the effect again. A client Http.get is re-sent too; a client Http.post is not.
• Schedule. Full jitter: the wait before retry n is random in [0, min(30 s, 1 s × 2^(n-1))]. A Retry-After header (seconds or a date) wins. One request is re-sent at a time, in the order they failed, so a click made while offline runs once, in order, when the connection returns. A request gives up after 8 attempts or 60 s.
• Running time, not wall time. The 60 s budget and the 30 s timeout count only time the page could run. While the page is hidden no request is given up. A request that was on the wire when the page froze (a phone app switch, a laptop lid, a tab restored from the back/forward cache) is re-sent at once on resume with a fresh budget: it does not reach App.withRpcError because the time the page was away made it look old (v0.27.6).
• Recovery signals. online, the page becoming visible again, pageshow and focus re-send the head of the queue at once, with a fresh budget.
• Protecting a recovering server. A retry token bucket per origin (10 tokens; a failure costs 1, a success refunds 0.1; below 5 no automatic retry starts) and, after a 429 or 503, client-side adaptive throttling of new requests (the Google SRE formula over a 2-minute window).
• What the user sees. Nothing while an outage is shorter than 3 s. After that, a small non-blocking "Reconnecting…" indicator (taps still work). The red "Can't reach the server [Retry]" bar shows only once a request's budget is spent, and the indicator goes when the connection is back.
• App.withRpcError receives FINAL errors only. A blip or a short outage never reaches it, so remove any app-level "network error, try again" banner.
• Your own indicator (optional). Sub.connection ConnectionChanged delivers Online | Reconnecting | Offline { pending : Int } on every change (import Std.Sub as Sub exposing (ConnectionState(..))). On Sky.Live and terminal targets it never fires.

Sub.every is a wake-up, not a clock: read the time the tick carries. A browser or a webview throttles timers in a background tab, so a counter of ticks drifts. Use Sub.everyWithTime 100 Tick (Tick : Int -> Msg receives the epoch milliseconds) and derive elapsed time from it. A tick whose update calls the server is treated as a poll: it is skipped while its previous call is unsettled, and while the page is hidden only its first call goes out; when the page is visible again one fresh tick runs at once. A tick that only changes the client model (a clock, a stopwatch) is never held back.

WebSocket from the client

A Sky.Spa client can hold its own WebSocket: Sky.Core.WebSocket (connect, send, sendBinary, receive, receiveWithin, forEachMessage, close, and the onOpen / onMessage / onClose / onError Subs) runs in the wasm client over the browser WebSocket API. The split classifies it as a client effect, so an arm that connects or sends runs in the client, not behind an RPC.

Connect ->
    ( model, Cmd.perform (WebSocket.connect "/ws") Connected )

subscriptions model =
    case model.sock of
        Just s -> WebSocket.onMessage s Got
        Nothing -> Sub.none

A path URL ("/ws") connects to the page's own origin (ws: or wss: after the page's scheme), so it passes a strict connect-src 'self'. Serve it from the backend with the server API, mounted with App.api:

wsHandler req =
    Ws.upgrade req (Ws.defaultCfg |> Ws.withOnFrame echo)

App.withRoutes [ App.route "/" Home, App.api "GET /ws" wsHandler ]

The upgrade's origin check admits the page's own origin; in production set Ws.withOriginPatterns. What a browser socket cannot do returns an Err instead of being ignored: request headers (withHeaders; the browser sends the session cookie itself, or use a query parameter) and a close code other than Normal or Custom 3000-4999. The browser answers pings itself, so withPingInterval has no effect. One reader per socket, as on the server: a Sub or a Task, not both. Proven in Chromium and WebKit by scripts/spa-websocket-e2e.sh.

Routing — App.withRoutes (History API)

Routing is opt-in via the App.withX builders (a single-view app needs none). The names read exactly like the web target:

• App.route path page — register a static route (App.route "/about" About). Put literal routes before :param patterns.
• App.routeParam path toPage — a route whose path carries a :param segment (App.routeParam "/thing/:id" ThingPage, ThingPage : String -> Page), captured as a String and passed to the page constructor. The captured value is percent-DECODED (/u/J%C3%B6rg gives "Jörg"), identically on the client, in the server-side first paint and on Sky.Live. Parse it (e.g. String.toInt) inside the constructor or view when you need a typed id; route an id your app rejects to App.withNotFound.
• App.withRoutes routes — resolves location.pathname on mount, on an intercepted internal-link click, and on Back/Forward, setting model.page.
• App.withNotFound page — the page shown when nothing matches.
• App.withOnNavigate (page -> msg) — fired after the route is applied, so the app can run an effect per navigation.

Internal <a href> clicks are intercepted (History pushState, no reload); Back/Forward (popstate) is honoured; an external host, target="_blank", a download, a sky-external mark, or a modified click is left to the browser.

A same-origin link to a path the server owns is a full browser navigation, not a client route: a path no client route matches, a path under /_sky/ or /_rpc/, and a path registered with Spa.serverRoute "GET /admin/logout" (for a path that is both a client route and a server route). A sign-out link, the Sky Console and a static file then reach the server. Nav.pushUrl and Nav.replaceUrl follow the same rule. One click runs only the handlers of the view it was delivered to; a nested outer onClick carries the Msg of that view.

The full surface (typed signatures + summaries) is sky doc Std.App.

Client persistence and identity

A web:app client writes its whole model to localStorage after each update and restores it on a full page load, so a reload keeps client scratch state (a form draft, a counter, a dismissed banner). localStorage is shared by every tab of the origin, and it holds ONE model: the last one any tab wrote.

A stored model restores only for the identity it was stored under. The identity is the value of the session field(s): the model fields of type Session / Maybe Session that a server branch writes, which the backend signs into the sky_spa cookie and the SSR seed carries. On a full load the client compares the identity of the stored model with the identity of the seed:

So two tabs with two identities (a practitioner in one, a patient link in the other) never show each other's data. Each tab's full load after the other tab wrote boots from its own seed: the tab loses its unsaved scratch state, never its server data. When an update signs out (clears the session field), the client removes the stored copy and does not write the signed-out model for the rest of that page's life, because that model still holds the signed-in user's other fields. A page served without an SSR seed (a static deploy, a native shell) has no server identity to compare, and restores the stored model as it is. An app with no session field has one identity, and restores as before.

Shared computers. The stored model stays in the browser until the next change of identity, sign-out in the page, or a full load under another identity. A user who closes the tab without signing out leaves their last model in localStorage, where the next user of that browser profile can read it with the developer tools (the app never shows it to them). Keep sensitive data in server state, not in client scratch fields, if the app runs on shared machines.

Before v0.25.18 the model was stored under sky:spa:model with no identity check. The client deletes that key on the first load and restores it only for an app with no session field. The current key is sky:spa:model:v2.

Sky.Live has no such store. A Sky.Live model lives on the server, keyed by the sky_sid session; the browser holds only the cookie. Two Sky.Live tabs with the same cookie share one session by design, and nothing of the model is written to the browser.

Security — the untrusted client is a first-class rule

In Sky.Live update runs on the server → trusted. In Sky.Spa update runs on the user's machine → untrusted. Therefore, unavoidably:

• The backend re-validates and re-authorizes every request and re-reads authoritative data (price, role, ownership, ids) from its own store. It may never trust a client-sent field for anything security-relevant.
• getJson / postJson are transport, not trust — they carry no ambient authority. Auth is an explicit header/cookie the author adds and the backend verifies with Std.Auth on every call; there is no session a client can spoof, because the backend is stateless.
• A hand-written Sky.Spa client that calls a stateless JSON API with a Bearer token and no cookie session needs no CSRF token: use Server.api routes (CSRF-exempt for the method they name). Security rests on re-validation.
• An endpoint that authenticates with a session COOKIE (the auto-split's signed sky_spa) is a Server.rpc route. The browser attaches the cookie by itself, so the route refuses any request that is not a same-origin application/json POST before the handler runs (403). The auto-split registers every /_rpc/<Msg> and /_rpc/__spaSignOut this way. See the auto-split security notes.
• Sign-out ends the signed session on the server, not only in the browser. The sky_spa token carries a session id; sign-out (and any change of the signed identity) records that id as ended in the session store, so a copy of the cookie taken before sign-out is refused afterwards. Give the replicas a shared store ([live] store / SKY_LIVE_STORE = postgres or redis). See Sign-out ends the signed session.
• GET /_sky/sub?topic=… streams a topic only when the app's own subscriptions, run on the visitor's verified session model, names it. Every other topic gets 403.
• Sky's typed secrets (Auth.signToken takes String, never any) and the production gate carry over unchanged.

Content-Security-Policy

A Sky.Spa page runs under script-src 'self' 'wasm-unsafe-eval' with no hashes and no 'unsafe-inline'. The build writes the wasm loader as a file, dist/spa-boot.<hash>.js, next to wasm_exec.js and main.<hash>.wasm, and precompresses it (.gz, and .br when brotli is installed) with them. Both dist/index.html and the SSR first-paint page load it the same way:

<script src="/wasm_exec.js"></script>
<script src="/spa-boot.<hash>.js" data-wasm="/main.<hash>.wasm"></script>

The loader reads the wasm URL from its own data-wasm attribute, so the file is the same for every build and its name changes only when the loader changes. The #sky-model seed stays a <script type="application/json"> block, which a browser never executes. The backend serves /spa-boot.<hash>.js itself, from memory, so the SSR page boots whether or not the backend can reach dist/. A static host (nginx, Caddy, a CDN) that serves the dist/index.html shell can serve the dist copy: the bytes are the same. 'wasm-unsafe-eval' is required because it allows WebAssembly.instantiateStreaming. It does not allow JS eval. Set SKY_CSP=strict to make the backend send the policy itself. See the Sky.Live architecture notes.

Deploying behind a proxy

A common layout runs the backend binary from its own directory and puts a proxy (Caddy, nginx) in front of it. The proxy serves the wasm from the frontend dist/ and forwards every other path to the backend. This is the contract for each asset the SSR page and dist/index.html name:

A Sky.Spa app must be served at the root of its origin. The SSR page and dist/index.html use root-absolute URLs, so a sub-path mount is not supported. (A Sky.Live app can run under a sub-path with SKY_LIVE_BASE_PATH behind a proxy that strips the prefix.)

The SSR page inlines its base CSS. The backend emits no other script, style sheet or font. The wasm pair stays a dist file because an app can host the wasm on a CDN, and wasm_exec.js must match the Go toolchain that built that wasm.

A Caddy example for a backend on port 8951 whose dist is at /srv/app/frontend/dist:

example.com {
    @wasm path *.wasm /wasm_exec.js
    handle @wasm {
        root * /srv/app/frontend/dist
        file_server {
            precompressed br gzip
        }
    }
    handle {
        reverse_proxy 127.0.0.1:8951
    }
}

A request for a Sky-owned asset name that the backend cannot serve (a stale /spa-boot.<hash>.js, a /_sky/*.js from an older build, or the wasm pair when dist/ is not reachable) is a 404. It is never the HTML of an app page, so a stale page fails loudly in the browser console instead of running HTML as script. A root route parameter (App.route "/:slug") no longer captures the wasm pair either: those names go to the dist file server first.

v0.25.19 did not serve the loader from the backend. Behind the layout above the backend answered /spa-boot.<hash>.js with HTML, the browser refused to run it, and the page never became interactive. On v0.25.19, add /spa-boot.*.js to the paths the proxy serves from dist/, or upgrade.

Native device capabilities

Std.Native capabilities are client effects: the auto-split keeps them in the wasm client, and on a native shell they reach the device through the shell's bridge. The secure store (Native.secureSet / secureGet / secureRemove) and the biometric prompt (Native.authenticate) have no web API, so in a plain browser they are Err Unavailable, never a localStorage fallback. The camera code scanner (Native.scanCode) is the same: the native shells have one, a browser does not (scan there with a widget island). Secret.fromString and Secret.reveal are pure and run in the client, so a client branch can use a secret it read from the device; Secret.fromEnv reads the server's environment and stays on the server. A Secret has no codec and never crosses the wire. Purpose strings, entitlements and sky package --release: docs/skyapp/native.md.

Honest limits

These are real, current scope boundaries — not roadmap optimism:

• Bundle weight → desktop/mobile-embed only. A real Sky.Spa app compiles to a standard Go→wasm bundle of ~9.5 MB raw / ~2.5 MB gzip (examples/60-spa-todos, measured). That is fine for a one-time desktop/mobile-embed download; it is too heavy for production web (Elm's equivalent ≈30 KB). The size is inherent to real Sky dispatch being reflection-native (sky_call / reflect.MakeFunc), which keeps most of the runtime reachable.
• Web / TinyGo / Sky→JS = v2. The named lever to shrink the bundle (TinyGo) cannot compile reflect.MakeFunc, so production web needs either a reflection-free core rewrite or a Sky→JS backend. Both are v2 bets, not done. See design.md §0/§9.
• Browser coverage. The TEA loop, the client renderer and the round trip run headlessly (Node and a DOM shim, examples/60's run_roundtrip.sh) and in Chromium and WebKit in the release gate's browser e2e scripts (scripts/spa-*-e2e.sh). Other browsers are not tested.
• The auto-split is built. sky build on a Spa.app entry or a web:app target derives the client/server partition (auto-split.md). What it cannot carry is a build error, and sky check reports the same error.
• Client effect surface is bounded. Client effects run through a single-threaded wasm interpreter: Cmd.perform (sync kernels like Time.now / Random inline; async Http via fetch), Sub.every timers, Sub.subscribeTopic (an EventSource on the backend's push endpoint), Sub.onFragment (the client reads location.hash at load and on every hashchange), Std.Nav (pushUrl / replaceUrl / clearFragment: the History API, then the route like a link click; a server branch's navigation runs in the client when it sends the request) and Sky.Core.WebSocket (the browser WebSocket API, above). Cmd.publish is a documented client no-op (no peer/session bus in a single tab); Http.Stream subscriptions are not wired on the client.

See also

• design.md — thesis, the two grill findings (bundle wall + thesis computability), the staged plan, and the measured evidence.
• auto-split.md — the v2 compiler-derived split (Task-body tracing + the effects-via-Cmd dialect).
• examples/60-spa-todos — the worked full-stack example.
• sky doc Std.App — the live front-door API (the low-level transport is sky doc Std.Spa).