Sky.Spa v1 — client routing + the explicit typed server boundary (P4)

Status: P4 design of record. This is the DX-defining surface: client-side routing (History API) and the explicit, author-declared server boundary (client Http → a stateless Sky backend, sharing a Std.Codec). User code writes this as Std.App (App.app + sky build --target web:app); Std.Spa is the low-level client runtime Std.App builds on, documented here as the mechanism. Every claim below is grounded in real Sky surfaces (file:line), verified against the code.

Phase-0 architecture consult (findings, file:line)

Sky.Live routing — the shape P4 mirrors

Std.Codec — the shared wire contract

The client transport (P3, already landed)

The server side of the boundary

Proposed API (implemented in P4)

Routing — opt-in builders (config stays the 4 TEA fields)

Author-facing these are App.withRoutes / App.route / App.withNotFound / App.withOnNavigate on an App.app value; the client build for --target web:app synthesises the Std.Spa app from your App.app and runs the existing auto-split. Underneath, Std.Spa exposes the same shape on its AppConfig (the mechanism this doc verifies):

type Route  -- opaque, produced by `route`

route : String -> page -> Route

withRoutes     : List Route -> AppConfig model msg -> AppConfig model msg
withNotFound   : page -> AppConfig model msg -> AppConfig model msg
withOnNavigate : (page -> msg) -> AppConfig model msg -> AppConfig model msg

appDef =
    App.app
        { init = init, update = update, view = view
        , subscriptions = subscriptions
        }
        |> App.withRoutes
            [ App.route "/"      Home
            , App.route "/about" About
            ]
        |> App.withNotFound NotFound
        |> App.withOnNavigate (\_ -> NavHappened)


main =
    App.run appDef        -- sky build --target web:app  (client wasm + backend)

Why builders, not routes in config (deviation from the literal brief — rationale). Sky.Live puts routes in config because a server must route every URL; a Sky.Spa client can legitimately be a single-view app (the shipped spa-counter/spa-input/spa-perform/spa-sub/spa-http apps have no routes and MUST keep compiling). A required routes/notFound field would (a) break every one of those and (b) force a meaningless notFound page on a counter. Sky.Live itself attaches every optional through withX builders (withHead/withOnNavigate/…), so a routed Std.App app "reads the same" — same App.route / App.withOnNavigate names, same mental model — while routing stays the opt-in capability it actually is. The app value remains the four TEA fields; a routed app adds |> App.withRoutes […] |> App.withNotFound Page.

Convention (mirrors Sky.Live exactly): a routed app's Model has a page field. On navigation the runtime resolves the URL → page value and sets model.page via RecordUpdate(…, {"Page": …}), re-renders, and — if withOnNavigate is set — dispatches onNavigate page through update.

Client router (wasm, //go:build js):

The explicit typed server boundary — pure Sky over existing kernels

getJson  : Codec a -> String -> (Result Error a -> msg) -> Cmd msg
postJson : Codec body -> Codec a -> String -> body -> (Result Error a -> msg) -> Cmd msg

getJson issues Http.get url, checks the status is 2xx, decodes the body with the shared Codec a, and hands update a Result Error a directly — removing the double-nested case (HTTP result, then decode result) an app writes by hand. postJson additionally encodes the request body with a Codec body.

No new runtime kernel — both are pure Sky over Cmd.perform + Http.* + Codec.fromJson/toJson + Task.andThenResult, so they add zero runtime surface and inherit P3's wasm transport unchanged. An app that needs headers / auth cookies / a non-JSON shape drops to Http.request + Codec directly; the helper is the ergonomic 90% path, not a wall.

The shared type is proved end-to-end by putting the type + its Codec in ONE module imported by both the wasm client and the stateless Sky.Http.Server backend: change the type, and both sides fail to compile — one type, one codec, one wire contract, no OpenAPI/TS drift.

Security — the untrusted client is first-class (not a footnote)

The Sky.Spa client runs on the user's machine, so it is untrusted. The boundary's shape must not encourage trusting it, and the docs say so plainly:

Five-pillar check