--- layout: home title: Forma for Elm-style apps description: The Elm Architecture, checked from the database to the DOM. A prelude-defined Forma prototype generates Foldkit and Effect TypeScript, with exhaustive update, checked command recovery, and pure views. sidebar: false aside: false pageClass: forma-index forma-elm ---

Forma for Foldkit · pre-alpha prototype

The Elm Architecture, checked from the database to the DOM.

A message arrives. Update chooses the next model and commands. View describes the screen. Forma gives that loop a small Lisp vocabulary and checks its contracts, then generates Foldkit on Effect 4. Exhaustive update, typed command recovery, and pure view work in the TypeScript prototype today. A single API contract from server to client is the next step.

Edit a command live Read the limits first

              message
                 │
                 ▼
           pure update
            ╱         ╲
         model      commands
           │           │
           ▼           ▼
       pure view    Effect A E R
           │           │
           ▼       ok + errors
          DOM          │
                       └──→ message

Prelude-defined vocabulary · TypeScript engine only · prototype reference

This embed runs the existing Effect dialect, showing the operation and recovery that underlie a command. Introduce an error to remove recovery and expose an unhandled typed failure, then restore it. The full msg / command / update / view / app prelude runs through generateElmProgram in a build script; it is not wired into the browser worker or language server.

00 The problem

The loop is simple. Its TypeScript encoding isn't.

Foldkit brings the Elm Architecture to Effect: schema-backed models, messages, commands, and pure update. TypeScript expresses those through schemas, unions, factories, and function signatures. Exhaustiveness depends on how you write the matcher. Forma makes the decisions visible as application vocabulary, so mistakes can point to the source you authored.

counter/
message.tsschemas + tagged union← eventsmsg
command.tsCommand.define + Effect.catchTag← recoverycommand
update.tsevery variant → model + commands← transitionwith
view.tsHtmlBuilder + message events← renderingview
app.tsModel + init + update + view← wiringapp

Messages and update

(with model command…)

Prototype · TypeScript engine

Adding a message creates an obligation.

msg declares a closed tagged union. Each update case returns (with next-model), optionally followed by command keywords. Adding a variant without an update case produces a located diagnostic. Wildcard update cases are rejected, so every message stays visible in review.

Message payloads are checked wherever they are built: command success, error recovery, and view events. A string cannot become GotCount.count. Update is pure; naming a command schedules work without running it.

with keeps the model and its work together. A keyword such as :load-count identifies a declared command; unknown command names are rejected. Ordinary if and let can choose transitions.

counter.lispcomplete checked source

<<< @/snippets/elm/counter.lisp

one update arm removedreal diagnostic

<<< @/snippets/elm/missing-update.txt

wrong success payloadreal diagnostic

<<< @/snippets/elm/invalid-payload.txt

Commands

Every declared failure becomes a message.

Prototype · TypeScript engine

The Elm guarantee, checked.

Elm's Cmd has no typed failure channel. Here a command wraps an ordinary Forma Effect value with declared success, errors, and service requirements. :ok maps the value to a message. :error names each error and maps its payload to a message. The resulting command has E = never.

The checker requires a mapping for every error in the operation's declared set, even when a particular implementation never raises it. Catch-all handlers cannot erase that obligation. Services stay in R; TypeScript host code provides the resource layer to Foldkit.

This covers typed failures. Defects, interruption, and exceptions in hand-written service implementations are still Effect runtime concerns. The prototype does not prove totality or eliminate runtime crashes.

error mapping removedreal diagnostic

<<< @/snippets/elm/unmapped-error.txt

View

Describe the screen. Produce messages.

Prototype · TypeScript engine

No services in render.

The Hiccup tree generates Foldkit HtmlBuilder calls. Text and class expressions are pure functions returning String. Click expressions are pure functions returning Msg. Calling a service or placing an Effect in either position fails the checker; view has no Effect environment.

The deliberately small surface supports :div, :span, :button, :class, and :on-click. A click contains a message value, evaluated from the current model when rendering. Arbitrary JavaScript handlers, raw HTML, and I/O are outside this vocabulary.

service called in a text nodereal diagnostics

<<< @/snippets/elm/impure-view.txt

End to end

One API contract, both sides.

Proposed

The database-to-DOM headline is the direction.

The HttpApi spike already checks server handler contracts against endpoint declarations. This prototype checks frontend operations and messages separately. It does not derive client commands from those endpoints or share their declarations across generators.

The proposed connection would derive client success and error messages from an api. Adding an endpoint error could then add a message variant and make frontend update non-exhaustive. Today you add the message and recovery explicitly; changing an API declaration alone does not change the app.

05 The output

Plain Foldkit. Plain Effect.

This is the complete generated module from the counter source above, checked against foldkit@0.168.0 and effect@4.0.3. No Forma runtime is imported.

Schema-backed data

Model and Msg become Effect schemas and TypeScript types. Message tags and payload fields survive generation.

Named commands

Prelude emit hooks produce Command.define. An adapter turns checked command keywords into deferred Foldkit commands.

A mountable app

The exported Counter configuration has Model, init, update, and view. Host code passes it, a container, and service layers to Runtime.makeElement.

An isolated generator

Call generateElmProgram from @formalang/ts/elm. Prelude descriptors define the domain IR; existing mechanics checks the lowered expressions.

counter.tsactual generator output

<<< @/snippets/elm/counter.ts

06 Evidence

A running prototype, with rejection cases.

The counter conformance case compares generated TypeScript to a golden, checks it under strict settings without type escapes, validates its declaration artifacts, and runs a headless harness.

Transitions. Init creates the expected model. Increment and decrement preserve immutable earlier models. Load returns a command and sets the loading state.
Real execution. The same command runs against success and failure service layers. Its messages feed update, producing the expected count, status, and error reason.
Located rejection. Exact fixtures pin missing update cases, unmapped errors, catch-all recovery, invalid success and event payloads, unknown commands, and impure update and view.

These fixtures establish the prototype's current behavior. There is no browser DOM harness for the full DSL or generated HttpApi client.

07 The cost

What you give up.

This is a small application-language experiment. The costs and boundaries are part of its contract.

Trade-offs

Two languages. App logic is Lisp; service adapters, mounting, and tests are TypeScript. Debugging follows generated code because source maps are absent.
A restricted view. Three elements and two attributes are enough to test the loop, not to build an accessible production component library. Routing, forms, inputs, lists, and UI components need more design.
Explicit transitions. Every update result uses with. Every command error gets a named recovery mapping. The ceremony makes obligations reviewable.

Missing today

Command arguments and lifecycle. Commands wrap zero-argument Effect values. Model-derived arguments, cancellation, subscriptions, and managed resources are not implemented.
Integration. One app and one message union per source. No module linking, CLI integration, editor routing, or browser worker support for these forms.
Production guarantees. No SSR, hydration, source maps, totality proof, or compatibility promise. Host service code remains trusted.

08 Open questions

The surface should follow the app.

The syntax is designed around authoring a Lisp application, rather than exposing every Foldkit factory.

Why with?

A transition is a model plus work. with makes that one expression and keeps update pure. Named keywords avoid exposing Command construction in user code. Argument-bearing commands need a next design.

Why Hiccup?

A vector tree is compact and familiar in a Lisp. Existing ui.lisp and ViewSpec describe ontology-bound interfaces; this view renders an application model. They remain separate prototypes, with no shared component or event bridge yet.

Subscriptions

Model-driven subscriptions should describe lifetime and teardown, rather than act like commands fired by update. Their syntax and typed message relationship are proposed, not implemented.

One contract across the network

Which endpoint errors become distinct messages? Which remain a shared failure payload? Until the HttpApi bridge answers that, the server and frontend contracts are checked independently.

09 Fit

When to try it.

Worth trying

Experiments in a typed Lisp for the Elm Architecture.
Small new Foldkit widgets with a few service-backed commands.
Teams studying how to make error recovery and message coverage visible in review.

Not yet

Replacing an existing production Elm or TypeScript frontend.
Apps that need routing, subscriptions, complex inputs, or a component ecosystem.
Teams that need stable editor tooling or shared server/client API generation today.

Read the loop, then run its commands.

The reference documents the complete prototype surface. The fixture shows the generated module and the service layers that exercise it.

Prototype reference Counter conformance Forma for Effect