Sky Takes Elm's Type Safety Off the Browser and Ships It as a Go Binary

The combination Sky describes — Elm-inspired syntax, Hindley-Milner type inference, server-driven UI, Go compilation target — reads like it was assembled from a wishlist of independent ideas. But the combination makes sense once you understand what each part is compensating for.

Elm’s defining property isn’t its syntax or even its architecture. It’s the guarantee that comes from a Hindley-Milner type system fully applied: if your program compiles, a substantial class of runtime errors becomes impossible. No null pointer exceptions, no unexpected undefined behavior from type confusion, no runtime type errors. The compiler enforces these properties through unification-based type inference, the same algorithm underlying ML, OCaml, and Haskell. You write code that looks untyped; the compiler proves it type-correct without asking you to annotate everything.

Elm deploys to the browser and targets JavaScript as its output. That made sense in 2012 when Elm appeared, and the Elm Architecture — a unidirectional data flow model with init, update, and view — was genuinely influential. Redux, Vuex, and The Composable Architecture for SwiftUI all borrowed from it. But Elm’s target is specific: interactive frontend UIs running in browsers. The HM type system and the no-runtime-errors guarantee are scoped to that one output.

Sky’s premise is that these properties are at least as valuable on the server side as on the client, and that compiling to Go rather than JavaScript changes the deployment story in useful ways.

The Server-Driven UI Model

Server-driven UI is a specific approach where the server doesn’t just send data — it sends the UI structure itself. The client is a thin renderer. The server describes what components should exist, in what configuration, with what content, and the client executes those instructions without knowing anything about the application logic.

Airbnb described their mobile SDUI system in engineering posts from around 2021-2022. They send a JSON tree of component nodes; the iOS and Android clients have a registry of known components and render whatever the server describes. Lyft built something similar. The benefits they cited were concrete: you can change the UI without app store releases, run A/B tests at the server level, and maintain consistency across platforms without duplicating logic in each client.

Phoenix LiveView in Elixir takes a related but distinct approach. The server holds all state, renders HTML, and sends diffs over WebSocket. The client patches the DOM; React Server Components do something similar within the React model, streaming serialized component trees from server to browser. The direction across all of these is consistent: pull logic and state back to the server, make the client thin.

Sky sits in this tradition. The practical consequence is that the type safety guarantee applies where it matters most. A type error in a client-side SPA crashes one user’s session. A type error in the server that drives all your UI is a production incident. The HM guarantee being on the server is arguably more valuable.

What Hindley-Milner Actually Gives You

Hindley-Milner type inference works through constraint generation and unification. The compiler assigns fresh type variables to unknowns, collects constraints as it walks the syntax tree — if f x appears, then f must have type a -> b where a matches x’s type — and then runs Robinson’s unification algorithm to solve the constraint system. If unification fails, you get a type error with a specific reason. If it succeeds, every expression has a principal type: the most general type consistent with all uses.

The practical consequence is let-polymorphism. In a language with HM, let id = \x -> x gives id the type ∀a. a -> a. You can call it with an integer, a string, a list; the same function works at all those types, and the compiler verified this without a single annotation. Lambda-bound arguments don’t get this generalization — they’re monomorphic, which is why ML-family languages have let as a syntactic form and not just sugar for function application.

OCaml, Standard ML, Haskell, Elm, PureScript, and F# all use HM or direct extensions of it. Haskell extends it with typeclasses for ad-hoc polymorphism; Elm deliberately omitted typeclasses to reduce complexity. Sky follows the Elm school here: the type system is powerful enough to eliminate runtime type errors without requiring deep expertise to navigate.

Go as a Compilation Target

Very few languages use Go as an output. Most functional language compilers target JavaScript, native code via LLVM, JVM bytecode, or .NET IL. Go is statically compiled, has its own runtime, and its type system was designed with different goals than ML-family languages.

The impedance mismatch is real. Go before 1.18 had no parametric polymorphism — you expressed generic behavior through interface{} and runtime type assertions, which abandon type safety entirely. Go 1.18 introduced type parameters with constraint-based generics, closer to Java or C# generics than to HM. Go also has no algebraic data types; the conventional substitute is a struct plus an interface, which requires explicit type assertions and gives you no exhaustiveness checking on pattern matches.

A compiler targeting Go has to encode HM’s richer type universe into Go’s flatter one. Algebraic data types — the type Msg = Increment | Decrement | Reset that Elm uses everywhere — need to be generated as an interface plus a set of implementing structs, with a type switch to recover the variant at use sites. The compiler can generate this correctly; the question is whether the generated Go is readable and whether the boundary between generated and hand-written Go stays manageable.

The prior art here is Oden, a functional language with HM types that compiled to Go, active around 2016-2017. Oden was abandoned, in part because the impedance mismatch between what functional code wants to express and what Go can represent efficiently was difficult to bridge in a way that felt natural. The generated Go tended to accumulate interface boxing and type assertions, undermining the performance argument for targeting Go in the first place.

Whether Sky finds a better path through that same problem is an open question. The project is experimental and early-stage.

The Single Binary Argument

The reason to tolerate the impedance mismatch is what you get on the other side. go build produces a statically linked binary with no external runtime dependencies. You can cross-compile for Linux from a Mac with GOOS=linux GOARCH=amd64 go build. You can build a Docker image FROM scratch with just the binary and get a container in the 10-30MB range. You deploy by copying a file.

For a server-driven UI backend, this matters. You’re running something continuously, probably in a container, probably on infrastructure where the operational overhead of runtime management — JVM heap tuning, Node.js version management, Python environment isolation — is real cost. The Go binary sidesteps all of it. Go binaries also start in milliseconds rather than seconds, which matters in environments where cold starts are visible to users or where you deploy frequently.

Sky’s bet is that combining Elm’s type safety guarantee with Go’s deployment story is worth the work of bridging two incompatible type systems. Functional language designers have usually chosen between type safety and deployment simplicity — OCaml compiles to native binaries but carries its own runtime; Elm compiles to JavaScript and inherits Node’s operational complexity if you run it server-side; Haskell’s GHC binaries are large and require the GHC runtime. Sky is asking whether you have to accept that tradeoff.

Where This Fits

The broader context is a convergence toward server-side state management. LiveView, Turbo, React Server Components, and now Sky all express some version of the same idea: the server should know more about what the client is doing, and the client should do less. The question is which level you want your type system operating at.

Elm demonstrated convincingly that HM types in a frontend context eliminate a real category of bugs and make refactoring substantially safer. Sky is a thesis that the same guarantee applied to the server driving your UI is at least as valuable, and that shipping it as a Go binary is the right deployment answer for current infrastructure.

The project is at an early experimental stage, and whether the Go code it generates is clean enough to be maintainable alongside hand-written Go remains unclear from the outside. But the combination it’s attempting, one that nobody else seems to be pursuing with this specific set of constraints, is worth watching.