Sky

sky-lang.org · Docs & tour · Examples

Status: v0.23.x — public APIs are stable for the v1.0 line; minor versions ship features additively. Internals can still change between minor versions. The compiler is written in Rust (cargo workspace at rust/) — the typed-Go output and the "if it compiles, it works" guarantee carry over unchanged. The retired Haskell compiler stays under legacy-haskell-compiler/ as the differential oracle. New in v0.23: Std.App — one builder + one --target for every app shape, and secrets are now the typed, self-redacting Sky.Core.Secret.

Sky is a fullstack functional language that compiles to typed Go. You write Elm-style syntax — explicit types, exhaustive pattern matching, no runtime exceptions — and ship a single static binary with a batteries-included stdlib, observability built in, and any Go package just an import away. One init / update / view runs it server-side (Sky.Live) or client-side in wasm (Sky.Spa) — same source, different reach.

module Main exposing (main)

import Std.Log exposing (println)

main =
    println "Hello from Sky!"

sky init hello && cd hello && sky run src/Main.sky

Why Sky

• If it compiles, it works. Every side effect returns Task Error a; every fallible value returns Result Error a; sky check invokes go build on the emitted Go so any shape mismatch surfaces at type-check time. There is no runtime null, no uncaught exception, no silent numeric coercion.
• One language, every shape — including cross-platform. The same init / update / view / subscriptions source compiles to a server-rendered web app (Sky.Live), a terminal UI (Sky.Tui), a native desktop window (Sky.Webview), or a wasm client (Sky.Spa) shipped to web, desktop, iOS, and Android from one codebase. One Std.Ui Element view paints to the DOM, to ANSI cells, or to a native webview.
• Batteries included. Auth, database, HTTP client + server, WebSocket, JSON, JWT, CSV, email, encryption, observability — every primitive a real app needs is in the stdlib (Std.Db, Std.Auth, Std.Ui, Std.Cache, Std.Email, …) and documented with sky doc --serve.
• Go's whole ecosystem. sky add github.com/some/package — the compiler introspects the Go package and generates strict, typed Sky bindings. No hand-written FFI glue. Stripe SDK (~76k FFI symbols) compiles and tree-shakes to a 4k-line main.go.
• AI-friendly by design. Explicit annotations, exhaustive pattern matching, no implicit coercions, no exceptions. LLMs generate code that compiles the first time. The shipped CLAUDE.md and sky init's starter CLAUDE.md give any AI assistant the load-bearing context to scaffold production apps directly.
• One binary out the back. Every project compiles to a static Go binary. Deploy with scp, with Docker, or as a CLI you brew install.

Why the compiler is in Rust

The Haskell compiler carried Sky through v0.17. The push to v1 — "if it compiles, it works" end to end, on an architecture that stays maintainable — surfaced limits in it that were structural rather than incidental: a monolithic multi-thousand-line lowering pass, mutable IORef compiler state that fought the very purity Sky promises its users, and an HM solver that needed hard memory budgets to stay bounded. The rewrite moves the compiler to a Rust cargo workspace of small, single-responsibility crates — lexer/parser, name resolution, HM inference, type-directed lowering, Go codegen, FFI, formatter, LSP — so each architectural decision sits behind a real module boundary instead of inside one file, and a query-DAG core makes incremental rebuilds and cross-module analysis robust by construction. Rust earns its place specifically: it compiles the corpus faster and with a lower, more predictable memory profile, and its algebraic enums, enforced exhaustiveness, and absence of null mirror the discipline Sky itself enforces — the compiler is now written in the same style it compiles. The typed-Go output and the "if it compiles, it works" contract carry over unchanged; every one of v0.17's hard-won learnings is now a crate boundary, a gate, or a test, which is what makes the v1 goals reachable. The retired Haskell compiler stays under legacy-haskell-compiler/ as a byte-for-byte differential oracle until v1 is tagged.

Hello, Sky

A counter web app — type-checked, server-driven, no JavaScript.

module Main exposing (main)

import Sky.Core.Prelude exposing (..)
import Sky.Core.String as String
import Sky.Core.Error exposing (Error)
import Sky.Core.Task exposing (Task)
import Std.App as App
import Std.Cmd as Cmd
import Std.Sub as Sub
import Std.Ui as Ui exposing (Element)
import Std.Ui.Font as Font


type Msg
    = Increment
    | Decrement


type alias Model = { count : Int }


init : () -> ( Model, Cmd Msg )
init _ = ( { count = 0 }, Cmd.none )


update : Msg -> Model -> ( Model, Cmd Msg )
update msg model =
    case msg of
        Increment -> ( { model | count = model.count + 1 }, Cmd.none )
        Decrement -> ( { model | count = model.count - 1 }, Cmd.none )


view : Model -> Element Msg
view model =
    Ui.row [ Ui.spacing 16, Ui.padding 24 ]
        [ Ui.button [] { onPress = Just Decrement, label = Ui.text "−" }
        , Ui.el [ Font.size 24 ] (Ui.text (String.fromInt model.count))
        , Ui.button [] { onPress = Just Increment, label = Ui.text "+" }
        ]


subscriptions : Model -> Sub Msg
subscriptions _ =
    Sub.none


appDef =
    App.app
        { init = init, update = update, view = view, subscriptions = subscriptions }
        |> App.withNotFound ()


main : Task Error ()
main =
    App.run appDef

sky run src/Main.sky    # http://localhost:8000

One App.app source, one --target per shape: bare (or --target web) serves it over Sky.Live; --target terminal:tui paints the same view to a terminal canvas; --target desktop wraps it in a native desktop window.

Install

# macOS / Linux — single-binary install
curl -fsSL https://raw.githubusercontent.com/anzellai/sky/main/install.sh | sh

# or build from source (Rust toolchain required to build the compiler)
git clone https://github.com/anzellai/sky
cd sky/rust && cargo build --release -p sky
# or install straight to ~/.local/bin:
#   cargo install --path rust/crates/sky --root ~/.local --locked

The sky binary embeds the runtime, stdlib, and Sky Console. End users only need sky on PATH and Go 1.21+ available for codegen.

Pick your shape — when to use what

Every shape is the same TEA-style init / update / view / subscriptions; pick by where the loop should run and how you ship it.

You write ONE App.app { init, update, view, subscriptions } source and pick a backend with a build-time --target family[:variant] (default web). You never import Std.Live/Std.Spa/Std.Tui/Std.Cli/Std.Webview — Std.App composes them all.

You're building	--target	Reach for it when	Delivers
Interactive web app, server-driven	web (default)	you want zero client build + instant first paint, server-owned state, and real-time updates over one SSE per session; the target is the browser today	Sky.Live
Cross-platform app (web · desktop · iOS · Android)	web:app · desktop:mac · tablet:ipad · mobile:ios	pure UI transitions should be instant + local (client wasm, no round-trip), the backend is a stateless API, and you ship to a webview (desktop/mobile)	Sky.Spa (client wasm)
HTTP / JSON API (no UI)	—	you're serving JSON/REST with typed routes + middleware, no rendered UI	Sky.Http.Server (Server.listen 8000 [...])
Terminal UI (TUI)	terminal:tui	a rich terminal app — the same Std.Ui view, painted to ANSI cells	Sky.Tui
CLI tool / background job	terminal:cli	a one-shot command or line-oriented loop	Sky.Cli (or bare main = Task.run ...)
Native desktop window	desktop	a desktop .app/.exe wrapping your UI in a native window	Sky.Webview

Add App.withNotFound … (mandatory for web/desktop) and App.withRoutes […] to the same appDef; for a raw Std.Html view use App.web instead of App.app, and for a hand-authored terminal view : model -> String use App.cli / App.tui. main = App.run appDef is the entry for every target.

Sky.Live vs Sky.Spa — the two TEA runtimes. Sky.Live keeps the loop on the server (per-user model, live SSE, a full re-render each interaction) — great for a browser web app with zero client build and instant first paint. Sky.Spa moves the loop to the client (compiled to wasm), so pure UI transitions are instant and local, the backend shrinks to a stateless API, and the one codebase ships to web, desktop, iOS, and Android. Same Model / Msg / update / view, same Std.Ui Element — you pick the runtime, not a rewrite.

Every backend shares Std.Ui for layout, Std.Auth for sessions, Std.Db for persistence, Std.Log / Std.Trace for observability, and Sky.Core.* for pure primitives.

Cross-platform + native device APIs (Sky.Spa)

sky build --target web|desktop|ios|android takes one Sky.Spa app to every platform, and sky spa-split derives a wasm frontend + a stateless backend + a shared codec contract from a single project. Native device capabilities are plain typed effects (Task Error a) via Std.Native — clipboard, local storage, geolocation, share, notifications, camera/photo/file pickers, battery, and more.

Extending native platform APIs — experimental. Native.bridge lets an app (or a distributable Sky library, with native/ios/*.swift + native/android/*.java and entitlement/manifest fragments) register its own native capability — e.g. Apple Pay / Google Pay — with no compiler change. This extensibility layer is an early, evolving feature; the API may change.

What ships with Sky

A short tour. Full reference at sky doc --serve or docs/stdlib.md.

Module	What it gives you
Std.Ui	Typed no-CSS layout DSL (row/column/el/button/input + Background/Border/Font/Region subs). Renders to inline-styled HTML, ANSI cells, or native Webview from the same source.
Std.Live	Sky.Live runtime — TEA app + SSE patches + session stores (memory / sqlite / redis / postgres) + routing + cookies + auth gates.
Std.Spa	Sky.Spa runtime — the same TEA loop compiled to GOOS=js GOARCH=wasm and run on the client (web / desktop / iOS / Android). sky spa-split derives a wasm frontend + a stateless backend + a shared codec contract from one project.
Std.Native	Typed native device capabilities as Task Error a effects — clipboard, local storage, geolocation, share, notifications, camera / photo / file pickers, battery, online/language/theme. Native.bridge + native/<platform>/ lets an app or library add its own (experimental).
Std.Bundle	Cross-platform packaging identity in code (withName / withId / withIcon / withVersion / withPermission / withAsset); sky build --target fills the Info.plist / AndroidManifest / icons / entitlements.
Sky.Http.Server	HTTP server with typed routes, middleware (CORS / logging / rate-limit / basic-auth), streaming responses, WebSocket upgrade.
Std.Auth	bcrypt password hashing, HS256 / RS256 JWT, register / login / roles. Typed secrets — never fmt.Sprintf("%v", token).
Std.Db	SQLite + PostgreSQL via one interface. Connection pool, prepared statements, versioned migrations, Db.RowDecoder, withTransaction. Sky can also ship and supervise the PostgreSQL itself — see below.
Std.Db.Schema	Typed, dialect-safe schema DSL — define tables as values; createTable emits the correct CREATE TABLE for SQLite and Postgres from one definition (no INTEGER-overflow / AUTOINCREMENT-vs-BIGSERIAL drift).
Std.Money + Std.Decimal	Arbitrary-precision Decimal + currency-typed Money (50+ ISO 4217 codes + crypto) with allocate for fair splits and conversion rates.
Std.Cache	LRU + TTL in-memory cache, parametric on key + value, monotone stats.
Std.Analytics	Typed product analytics — typed event props (Money lossless, Pii redactable), consent-gated + anonymous by default, opt-in Sky.Live auto page-views, SQLite store, and a Sky Console Analytics tab (counts / recent / revenue-by-currency).
Std.Email	Resend / SES / SendGrid / SMTP under one typed EmailProvider. SKY_EMAIL_DRY_RUN=1 for tests.
Std.Compression / Std.Csv / Std.Config	gzip / zstd; RFC 4180 CSV; TOML / YAML / JSON decoders that mirror Sky.Core.Json.Decode.
Sky.Core.WebSocket	Client + server bidirectional sockets.
Sky.Core.Crypto	SHA-256 / 512, HMAC, RSA sign/verify, AES-GCM, ChaCha20, scrypt password derivation, AEAD constants.
Std.Webview	Native desktop window (macOS in v0.1; Linux / Windows in v0.2).

PostgreSQL, without the setup

Developing on SQLite and deploying on Postgres is how dialect differences reach users. So sky ships and supervises PostgreSQL itself, across four tiers:

sky db start | stop | ps                 # a per-project dev cluster, on a unix socket
sky db provision --embed                 # fetch + pin a PostgreSQL bundle
sky build --embed src/Main.sky           # bundle it INTO the binary → ./sky-out/app --embed
sky db provision --shared --app myapp    # one host cluster; a database + role per app

The app binary never knows which tier it is in. It consumes a DSN — only the provisioner changes, so the same binary runs against a dev cluster, its own embedded PostgreSQL, or a managed database, with no code change. Bundles are built from source in CI (PostgreSQL 18.6, pinned) with an SBOM and a GPL/LGPL/AGPL link gate, and published as postgres-bundle-v18.6.

Where the embedded bundle runs: it's a self-contained, glibc-linked PostgreSQL, so it works on any normal Linux VM (EC2/GCE), a macOS/Linux laptop, and debian-slim/distroless containers with a mounted volume — verified end-to-end. It does not run on Alpine (musl), bare FROM scratch, or Windows (use WSL2 or a system Postgres), and a stateful database is the wrong fit for stateless functions (Lambda / Cloud Functions → pair with managed PG). Full matrix: docs/skydb/embedded-postgres.md.

It fits in 1 GB. On the e2-small this was measured on, a Sky.Live app plus its own embedded PostgreSQL leaves the machine ~410 MB short of its total before a single session exists — MemTotal − MemAvailable, OS included, with the app idle at ~21–27 MB and PostgreSQL costing +28.4 MB of that (docs/perf/runs/gcp-embed-postgres-20260815/sweep.tsv, analysed at docs/perf/skylive-interaction-cost.md). Without the database it is ~382 MB. So a free-tier or entry-level cloud instance runs a real app with a real database, and the managed-database line disappears from the bill.

Sizing is measured on real GCE instances, not guessed (docs/perf/): a session's marginal cost is 625–650 kB on x86 with a PostgreSQL session store (451–531 kB on the memory store, stock GOGC), and CPU runs out well before memory does — an e2-small with embedded PostgreSQL sustains ~64 interactions/sec at 300 sessions, an e2-medium ~262 (commit 3ed83c08; docs/perf/runs/gcp-x86-capacity-20260816/). Count physical cores, not vCPUs — a GCE vCPU is an SMT thread, worth ~1.27×, not 2× (runs/gomaxprocs-scaling-20260816/). And on a burstable e2 instance plan with the sustained figure: a rested e2-small's first run measured 2.7× what it then sustained.

A single instance has no replica — --shared generates a backup timer, a lone --embed app does not, so schedule a pg_dump. Full sizing: docs/skydb/embedded-postgres.md.

A Sky app process opens four PostgreSQL-facing pools, and on a shared server their sum is the binding constraint — the arithmetic is worked through in docs/skydb/embedded-postgres.md, along with the full design and the tier-by-tier trade-offs.

No postgres-bundle-v* release has been cut yet, so sky db provision --embed has nothing to fetch. sky db start works today against SKY_POSTGRES_BIN, a local bundle, or a system PostgreSQL.

Observability — built in

Every Sky.Live and Sky.Http.Server app auto-mounts:

• /_sky/console — Std.Ui dashboard with overview, logs, metrics, traces, errors (production-gated via SKY_CONSOLE_AUTH).
• /_sky/metrics — Prometheus scrape endpoint (sky_live_requests_total{route,status}, latency histograms, drop counters).
• /_sky/healthz / /_sky/readyz — liveness + readiness probes.
• /_sky/buildinfo — commit, build timestamp, Sky version.

Run sky console serve to stand up a central hub that multiple Sky apps push telemetry to via the HubExporter (OTLP/HTTP). See docs/history/v0.16.x-console/HUB.md for the multi-service dashboard, tenant isolation, and the 3-layer auth defense-in-depth model.

OTEL_EXPORTER_OTLP_ENDPOINT is honoured for the standard OpenTelemetry collector — point at Honeycomb, Grafana Tempo, Datadog, etc.

Telemetry storage tunes from your config binding (or SKY_TELEMETRY_* env, which overrides it): counter/histogram coalescing windows shrink the telemetry tables on a busy app, and Sky.Config.withTelemetryDbCapacity drives an hourly database size report that warns before you run out of room. See docs/observability.md.

Going to production

# sky.toml
name = "myapp"
version = "1.0.0"
entry = "src/Main.sky"

[live]
port = 8000
store = "sqlite"          # memory / sqlite / redis / postgres
storePath = "sessions.db"
ttl = "30m"

[database]
driver = "sqlite"         # sqlite / postgres
url = "DATABASE_URL"

# Std.Auth has no [auth] section — it's a library. signToken takes the
# secret + TTL as arguments; SKY_AUTH_TOKEN_SECRET (≥32 bytes) comes from
# the environment, never a committed file.

[log]
format = "json"           # plain / json
level  = "info"

ENV=production \
SKY_AUTH_TOKEN_SECRET="$(openssl rand -base64 48)" \
SKY_CONSOLE_AUTH=app SKY_CONSOLE_TOKEN="$(openssl rand -base64 48)" \
sky build src/Main.sky && ./sky-out/app

The production gate is ENV (then SKY_ENV fallback). Unset or dev / development / local → dev mode. Anything else locks down the dev console, banner, and metrics endpoint.

Deploy with scp + your favourite supervisor, drop the binary into a Docker FROM scratch image, or run it directly on any platform with a Go 1.22+ runtime.

Documentation

📖 Documentation site — the guided Learn Sky tour (from your first app to a real web app, plus a chapter for developers coming from another language), topic guides, and a searchable API reference generated from the stdlib source on every build. The links below point at the same content in the repo.

• Getting started — install + your first app in 5 minutes.
• Stdlib reference — every module, every function, indexed by tier (Pure / Fallible-pure / Task / Diverging).
• Sky.Live — server-driven UI
  • SSE patches + sessions + routing.
• Std.Ui — typed no-CSS layout DSL.
• Sky.Tui — terminal backend for Std.Ui.
• Sky.Webview — native desktop window.
• Std.Auth — sessions + JWT + roles.
• Std.Db — SQLite + PostgreSQL.
• Embedded PostgreSQL — the four tiers, from a per-project dev cluster to a shared host one.
• sky.toml — every config key.
• CLI / LSP / Testing.
• Known limitations — current-version constraints + workarounds.
• Compiler journey — how Sky got here (historical context, kept for contributors).

Examples

~50 examples ship in examples/. Each builds clean from a wiped slate (rm -rf sky-out .skycache .skydeps && sky build).

Range	Category
01-08	Hello / CLI / Go-FFI / file / system
09-12	Sky.Cli / Sky.Tui counters & TODOs
13	Stripe-SDK-scale FFI benchmark (76k symbols)
14-25	Sky.Live + Sky.Http.Server apps
26	examples/26-ui-showcase — every Std.Ui primitive
29-31	Sky.Webview + WebGL spike
32-33	SSE relay + WebSocket echo
34-38	Multi-tier + composite-test apps
39	Two Sky.Live apps → one hub (v0.16.6)

Contributing

Issues and PRs welcome at github.com/anzellai/sky. The Rust compiler architecture write-up is the right starting point for compiler work (the Haskell-era docs/history/compiler/ notes are kept as historical reference). Run cargo test --workspace plus the xtask gate suite (cargo run -p xtask -- <gate>) before any PR; scripts/example-sweep.sh validates every example builds.

Licence

Apache 2.0 — © 2025–2026 Anzel Lai. Includes patent grant + trademark clause. Prior-art attribution for derivative files (parts of the type-inference core adapted from elm/compiler under BSD-3-Clause) lives in NOTICE.md. Contributions accepted under the same Apache 2.0 terms — see CONTRIBUTING.md.

Sky was previously distributed under the MIT licence (releases up to and including v0.10.0). Those releases remain available under their original MIT terms; v0.10.1 onwards ships under Apache 2.0.