Taking Elm's Best Ideas Off the Browser: The Architecture Behind Sky

Most languages in the ML family have a web habit. Elm compiles to JavaScript. PureScript compiles to JavaScript. ReScript compiles to JavaScript. Gleam compiles to Erlang and JavaScript. Even Roc, which targets native code and bills itself as general-purpose, has its primary showcase in browser-adjacent tooling. The shared assumption is that functional type discipline belongs on the client side.

Sky makes a different set of assumptions. It takes Elm’s design influence, adds Hindley-Milner type inference, targets server-driven UI as the application model, and compiles to Go for single-binary deployment. None of those choices is accidental, and taken together they occupy a genuinely distinct point in the language design space.

What Hindley-Milner Type Inference Actually Does

The term gets used loosely, so it is worth being precise. The Hindley-Milner type system, formalized by Luis Damas and Robin Milner in their 1982 paper on principal type-schemes, provides a type inference algorithm that derives the most general type for any expression without requiring explicit annotations. The algorithm works by generating type constraints as it traverses the AST, then solving those constraints through unification.

The key property is principality: for any well-typed expression, there is a unique most general type, and the algorithm finds it. This gives you parametric polymorphism without explicit type parameters at call sites.

-- No annotations required
map f list =
  case list of
    [] -> []
    (x :: rest) -> f x :: map f rest
-- Inferred: map : (a -> b) -> List a -> List b

add x y = x + y
-- Inferred: add : number -> number -> number

The practical consequence is that you get Haskell-grade type safety with roughly the annotation burden of Python. The compiler catches contract violations at compile time, including exhaustiveness of pattern matches on sum types, without requiring you to annotate every function signature.

The well-known downside is error message quality. When unification fails, the algorithm reports the failure at the unification site, which may be far from the actual source of the inconsistency. Elm spent years improving this, investing in a custom constraint solver and error formatter that tries to surface the semantic intent of the failure rather than the raw unification conflict. Whether Sky inherits that investment or starts from scratch is one of the meaningful open questions about the project.

Go as a Compilation Target

Compiling to Go is an unusual choice. Go is not designed as a compilation target the way LLVM or WebAssembly are. It has no stable ABI in the sense that LLVM IR does. Its type system is simpler than most ML-family languages, which means the compiler needs to erase or encode higher-kinded types and sum types into Go’s type system.

But Go has properties that make it coherent as a target for exactly this use case.

Single binary output is Go’s default. Running go build produces a statically linked binary with the runtime embedded. There is no equivalent of Node.js version management or JVM flags to configure. Cross-compilation is also built-in: setting GOOS and GOARCH environment variables produces a binary for any supported platform without a separate toolchain. For a server-side application framework, this matters immediately.

Go’s standard library covers the primitives a server-driven UI runtime needs: HTTP servers, JSON encoding, context propagation, and TLS, all without external dependencies. A Sky application compiled to Go can serve UI descriptions over HTTP with a binary that links nothing beyond the Go runtime itself.

Go’s goroutines also map naturally to the event-driven model that server-driven UI requires. Each connected client can be managed by a goroutine with its own state, responding to incoming events and emitting updated UI descriptions. The Go scheduler handles the concurrency; Sky’s type system handles the state transitions.

The prior art for using Go as a high-level compilation target is thin. CUE generates Go code, but it is a configuration language, not a general-purpose one. Starlark has a Go interpreter, but it does not compile to Go. Sky appears to be making a relatively unexplored bet on Go’s deployment story as the primary motivation for the compilation target.

Server-Driven UI and Why Functional Types Fit

Server-driven UI (SDUI) inverts the conventional web architecture. Instead of the server sending data and the client deciding how to render it, the server sends a description of the UI: layout trees, component specifications, event bindings, state. The client is a thin renderer that interprets these descriptions and sends user interactions back as events.

At scale, this model has clear operational advantages. Airbnb published early work on server-driven UI for their mobile apps, noting that they could change application behavior without shipping a new app store build. Meta uses a similar model for parts of their feed infrastructure. The pattern trades client-side flexibility for server-side control.

For a functional language, SDUI maps onto existing idioms without friction. The Elm Architecture, which Sky draws from, is already a pure function from model to view: view : Model -> Html Msg. If you lift that entire loop to the server, the view output becomes a serializable data structure describing the UI, and user interactions become typed messages sent back to the server.

type Model = { count : Int, loading : Bool }

type Msg = Increment | Decrement | Reset

update : Msg -> Model -> Model
update msg model =
  case msg of
    Increment -> { model | count = model.count + 1 }
    Decrement -> { model | count = model.count - 1 }
    Reset     -> { count = 0, loading = False }

view : Model -> UI
view model =
  column
    [ button [ onClick Increment ] [ text "+" ]
    , text (String.fromInt model.count)
    , button [ onClick Decrement ] [ text "-" ]
    ]

In Elm, this loop runs in the browser. In Sky’s model, update and view run on the server. The view output is serialized into a UI description and sent to a thin client. Click events are transmitted back as Msg values.

The type system earns its keep in this architecture. Msg is an exhaustive sum type. If you add a Reset case and forget to handle it in update, the build fails. The compiler enforces the contract between the event producer (the UI description) and the event consumer (the update function). This eliminates an entire class of runtime bugs that would be invisible in a dynamically typed or loosely typed system, and it does so at the boundary that matters most: the interface between client and server.

Comparing the Neighbors

Sky occupies a position that none of its closest neighbors quite fills.

Phoenix LiveView does server-side state management with real-time DOM updates over WebSockets. It is production-proven at scale and has a large ecosystem. But it does not give you HM type inference or a purely functional update model. Elixir has a type system in active development, but it is not yet the primary tool for catching UI contract errors.

HTMX keeps the browser as a thin client by returning HTML fragments from the server. It requires no JavaScript framework and works well with any server language. But it does not give you typed UI descriptions or a structured event model. The client and server are coupled through HTML conventions, not through a type-checked interface.

Elm itself, as noted, stays in the browser. The MVU architecture is designed to run where the user is, not where the server is.

Sky’s synthesis, a functional language with HM types targeting Go for SDUI, does not have a direct equivalent. Whether that is because the combination is under-explored or because the trade-offs do not work in practice is something only deployed applications will answer.

The Trade-offs Worth Taking Seriously

The latency concern with SDUI is real. Every user interaction requires a server round-trip before the UI can update. Elm’s original design kept the update loop in the browser precisely to avoid this. For applications with reliable, low-latency connectivity, the round-trip is imperceptible. For mobile apps on poor networks, it can make the application feel sluggish.

Sky could address this with optimistic local updates, where the client applies a predicted state change immediately and reconciles with the server response. But that requires the client to understand the update semantics, which partially undermines the server-driven model.

The other trade-off is the Go type system’s expressiveness as an encoding target. Go does not have sum types natively. Encoding Elm-style union types in Go requires either interface types with type switches, or code generation that produces concrete struct types per variant. The ergonomics of that encoding will affect the quality of the generated code and the usefulness of any FFI between Sky and existing Go libraries.

These are not fatal problems. They are the expected set of challenges for a language at this stage. The design decisions are coherent, and the application model is grounded in patterns that have worked at scale elsewhere.

The Broader Pattern

The ML family of languages has a long history of good ideas that took a decade to find their practical form. Haskell’s monads showed up in Rust’s Option and Result. Elm’s MVU architecture influenced React’s state management conventions. OCaml influenced F#, which influenced C#‘s type inference.

Sky is making a concrete, early bet: that the combination of functional type discipline, server-driven UI architecture, and Go’s deployment characteristics is a viable basis for production applications. The project is early, and the proof will be in the applications built with it. But the combination of design decisions is coherent enough that it is worth watching, and worth thinking through before the pattern becomes obvious in retrospect.