A small project surfaced on Lobsters recently without much ceremony around it, but its description is specific enough to be worth unpacking. Sky is an Elm-inspired language with Hindley-Milner type inference that compiles to Go and targets server-driven UI as its primary use case. Each piece of that description has a distinct history, and each one reinforces the others.
The Elm Architecture
Elm is a functional language for the browser created by Evan Czaplicki, first described in his 2012 Harvard thesis and refined into its current form around the 0.17 release in 2016. The Elm Architecture (TEA) is the structural pattern it settled on: a Model type representing all application state, an update function that takes a message and the current model and returns a new model along with any side-effect commands, and a view function that takes the model and returns a description of the UI.
TEA is Elm’s structure; the guarantees Elm enforces around it are what make the language distinct. There are no runtime exceptions in well-typed Elm programs. The type system uses Hindley-Milner inference, meaning types are fully checked without requiring the programmer to annotate every binding. The compiler catches mismatches between what a function produces and what a caller expects, missing cases in pattern matches over union types, and values that might be absent being treated as always present.
Dan Abramov acknowledged drawing directly from Elm when designing Redux, and the pattern has since appeared in SwiftUI, Jetpack Compose, and dozens of smaller libraries. TEA’s influence is broad enough that it no longer belongs to any specific runtime.
TEA Running on the Server
Most Elm-inspired work targets JavaScript. PureScript carries a more powerful type system to the browser. Fable compiles F# to JavaScript and TypeScript-compatible output. Gleam brings static types to the Erlang BEAM, with a secondary JavaScript compilation target. ReScript is OCaml-derived and ships to JavaScript. Each of these takes Elm’s core insight, that a functional language with principled types can coexist with an existing ecosystem’s runtime, and applies it to a JavaScript or BEAM target.
Sky’s bet is different: compile to Go, run on the server, and use TEA as the architecture for server-driven UI.
Server-driven UI is a pattern where the server sends not just data but a structured description of the interface itself. The client is a thin renderer. It maintains a vocabulary of known components and renders whatever the server describes, without containing any product logic of its own. Airbnb, Spotify, and Facebook have all built production SDUI systems because they allow instant rollouts and centralized control of user-facing behavior without going through app store review cycles.
TEA maps onto this cleanly. The Model lives on the server. The update function runs on the server when a user action arrives. The view function produces not Html Msg as in browser Elm but a serialized component tree that the client renders. The unidirectional data flow that makes Elm programs predictable in the browser makes the same guarantee in a server-driven context: state transitions are pure functions, there is one canonical source of truth, and the client never needs to reconcile local state with remote state because it has no state of its own. The architecture removes an entire category of synchronization bugs.
Why Go
The choice of Go is not the obvious one, and Go has hosted this kind of experiment before without much success.
Oden was an Elm and Haskell-inspired language that compiled to Go, developed by Oskar Wickström around 2015 to 2017. It had a custom type system, pattern matching, and a similar functional-first design philosophy. Wickström abandoned it, citing the fundamental impedance mismatch between a rich functional type system and Go’s structural types and explicit error propagation. Go’s pre-1.18 lack of generics made things worse: generating idiomatic Go from a parametrically polymorphic source language required significant awkwardness in the emitted output, and the generated code was hard to debug because stack traces referred to Go source that no one had written.
Go 1.18 shipped generics in March 2022, and that changes some of the calculus. A Go-targeting compiler can now emit generic Go functions and types where the source language’s type variables require it, rather than resorting to interface{} and runtime type assertions. This does not remove all the friction. Go’s approach to effects, its error-as-value convention, and its structural subtyping are still a considerable distance from a purely functional model. But it opens more of the surface area than was available to Oden.
The argument for Go despite these frictions is the deployment story. Go builds statically linked binaries with no runtime dependency, often under 10MB, that start in milliseconds. Cross-compilation is a single environment variable. Containerizing a Go server means a FROM scratch Dockerfile and a COPY of the binary. For a language whose pitch is running TEA on backend servers, the Go binary story is genuinely good. It is a better fit for this use case than targeting the JVM or a Python runtime would be, precisely because the operational simplicity is part of what Sky is selling.
What Hindley-Milner Brings
Go has a type system that is deliberately modest. It has structural interfaces, basic generics since 1.18, and type inference for short variable declarations. What it does not have is the full Hindley-Milner inference described in Robin Milner’s 1978 paper “A Theory of Type Polymorphism in Programming” and formalized with Luis Damas in their 1982 paper on principal type schemes. Algorithm W, the practical inference procedure derived from that work, guarantees completeness: if a program is typeable, the algorithm finds the most general type without requiring hints from the programmer. This underpins ML, OCaml, Haskell, F#, and Elm.
The difference in practice is that a language with HM inference propagates type constraints through the entire program without annotations. A function that transforms a model record gets its type inferred from how it is used. Pattern matches over union types are checked for exhaustiveness at compile time. A view function cannot be called with a model that has not been properly initialized, because the compiler rejects such a call before the program runs. Go’s inference is limited to the declaration site; HM extends through the program. For a codebase where correctness depends on the model always being in a valid state and the view always consuming a well-typed model, this is a meaningful safety upgrade over writing the same logic in Go directly.
There is also an ergonomic point. Go’s verbosity around error handling and type annotations is a common friction point. A language that infers types fully while still compiling to Go binaries preserves Go’s operational advantages without carrying all of its syntactic weight.
The Lineage This Fits Into
The clearest analogies for what Sky is attempting are ClojureScript and Fable. ClojureScript gets the entire npm ecosystem and deploys wherever JavaScript runs. Fable gets npm, TypeScript interop, and a substantial F# library ecosystem. Gleam gets the BEAM’s fault-tolerance, OTP concurrency, and a secondary JavaScript target.
What these projects demonstrate is that a functional language targeting an existing runtime succeeds when it delivers a coherent interop story. ClojureScript can call any JavaScript library without friction. Fable compiles to TypeScript-compatible output so that existing JS tooling still works. The friction of using the host ecosystem’s packages is low enough that the type-safety gains outweigh it.
Sky’s interop story with Go packages will determine a lot. If calling a Go HTTP handler or database library from Sky code requires substantial boilerplate or type-system bridging, the practical appeal narrows significantly. The interop problem is the hardest engineering challenge in this category, and it is what Oden ran into directly. Go’s type system makes the problem structurally harder than JavaScript’s untyped surface, because there is no escape hatch through any: a Go function that returns ([]byte, error) does not map naturally onto a pure functional value without some explicit boundary layer.
Where This Lands
Sky is an early project, experimental, without production use cases or a stable release. But the core architectural idea is coherent, and the combination it targets is not arbitrary. TEA’s functional purity fits SDUI’s requirement that the server is the single source of truth. Hindley-Milner inference makes the type safety practical without annotation overhead. Go’s compilation model delivers the operational simplicity that a backend language needs.
The practical question is whether the Go interop story can be made smooth enough to be useful. Oden’s experience is instructive: the conceptual fit was good, but the engineering cost of the impedance mismatch was too high to sustain. Go generics have removed some of that friction since Oden’s time. Whether Sky can navigate the rest without Oden’s fate is the open question worth watching.