hale
v0.23 · prerelease
/examples

Programs, and what the compiler says about them

Each program sits beside a deliberate break. The run output and the compiler's refusal are captured from hale 0.23.0 at build time, so nothing under a machine label is typed by hand.

Everyday Hale

Arguments, files, JSON, HTTP and config. The level you would use Python or Node for.

A CLI converter

Read a positional argument with a default, parse it with the error addressed on the same line, print the answer. hale build turns it into one static executable, with no interpreter and no packaging step. The break shows the fallback being typed: a default that could not stand in for the parse result is refused.

Read CLI arguments & config →
convert.hleveryday
fn main() {
    let raw = std::env::arg_or(1, "100");
    let celsius = std::str::parse_int(raw) or 0;
    let fahrenheit = celsius * 9 / 5 + 32;
    println(raw, "°C = ", fahrenheit, "°F");
}
$ hale run convert.hl
100°C = 212°F
Default with the wrong type.
std::str::parse_int(raw) or 0
std::str::parse_int(raw) or "0"
$ hale check convert.hl
convert.hl:3:19: type error: `or <substitute>`: fallback type `String` does not match success type `Int`
        let celsius = std::str::parse_int(raw) or "0";
                      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

JSON into a typed value

The json: tags on the type are the whole codec. from_json walks the document once into a typed value and to_json writes it back. A missing field is an error with a name, caught at the parse, and the parse is fallible, so skipping the handler is a compile error.

Read JSON without a schema language →
orders.hleveryday
type Order {
    id: Int          `json:"id"`;
    price: Int       `json:"px"`;
    currency: String = "USD";
}

fn main() {
    let body = "{\"id\": 7, \"px\": 1899}";
    let o = Order::from_json(body) or { println("bad order: ", err.field); return; };
    let marked = Order { id: o.id, price: o.price * 105 / 100, currency: o.currency };
    println(Order::to_json(marked));
}
$ hale run orders.hl
{"id":7,"px":1993,"currency":"USD"}
Skip the error the parse can raise.
Order::from_json(body) or { println("bad order: ", err.field); return; }

$ hale check orders.hl
orders.hl:9:13: type error: `Order::from_json` can fail (JsonError) and this call says nothing about it: write `or raise` to hand the failure to the caller, `or <fallback>` for a value to use instead, `or handler(err)` to deal with it here, or `or discard` when losing it is the intent. A bare call to a fallible entry point is an error since v0.22.0 (GH #738).
        let o = Order::from_json(body);
                ^^^^^^^^^^^^^^^^^^^^^^

Walk a directory and count what matters

Write, list, read and summarize with the one-shot std::io::fs calls, each fallible and each addressed where it happens. Inside a fallible helper an unhandled error propagates to the caller. At main it stops, and the break shows the compiler refusing to let it ride.

Read files & the filesystem →
logsum.hleveryday
@form(vec)
locus Names { capacity { heap items of String; } }
@form(vec)
locus Lines { capacity { heap items of String; } }

fn count_errors(text: String) -> Int {
    let lines = Lines { };
    std::str::split_into(text, "\n", lines);
    let mut errors = 0;
    for line in lines.items {
        if std::str::starts_with(line, "ERROR") { errors += 1; }
    }
    return errors;
}

fn summarize() fallible(IoError) {
    std::io::fs::mkdir("logs") or discard;
    std::io::fs::write_file("logs/api.log", "ok\nERROR timeout\nok\n") or raise;
    std::io::fs::write_file("logs/db.log", "ERROR lock\nERROR retry\n") or raise;

    let found = Names { };
    let count = std::io::fs::list_dir_count("logs") or raise;
    let mut i = 0;
    while i < count {
        found.push(std::io::fs::list_dir_at("logs", i) or raise);
        i += 1;
    }
    let names = Names { };
    found.sort_into(names);

    for name in names.items {
        let text = std::io::fs::read_file("logs/" + name) or "";
        println(name, ": ", count_errors(text), " error(s)");
    }
}

fn main() {
    summarize() or { println("io error"); };
}
$ hale run logsum.hl
api.log: 1 error(s)
db.log: 2 error(s)
Let the helper's errors ride past main.
summarize() or { println("io error"); };
summarize();
$ hale check logsum.hl
logsum.hl:38:5: type error: `summarize` can fail (IoError) and this call says nothing about it: write `or raise` to hand the failure to the caller, `or <fallback>` for a value to use instead, `or handler(err)` to deal with it here, or `or discard` when losing it is the intent. A bare call to a fallible entry point is an error since v0.22.0 (GH #738).
        summarize();
        ^^^^^^^^^^^

One HTTP request

std::http::get returns a response or an error with a kind. Connection refused and a bad URL are different values, and the or-block is where the caller decides what a failure means. Run output is not captured at build time because CI has no network.

Read HTTP clients & servers →
fetch.hleveryday
fn main() {
    let url = std::env::arg_or(1, "https://hale-lang.org/llms.txt");
    let resp = std::http::get(url) or {
        println("fetch failed: ", err.kind);
        return;
    };
    let body = std::str::from_bytes(resp.body);
    println("status ", resp.status, ", ", len(body), " bytes");
}

Layered config

One resolver states the precedence: positional argument, then $APP_HOST, then the built-in default. An app locus receives the result as typed params. Params are a contract, so constructing one the locus never declared is the break, and the diagnostic names the field.

Read CLI arguments & config →
configured.hleveryday
locus App {
    params { host: String = "0.0.0.0"; port: Int = 8080; }

    run() {
        println("listening on ", self.host, ":", self.port);
    }
}

fn main() {
    let cfg = std::cli::Resolver {
        env_prefix: "APP_",
        argv_keys: "host\nport\n",
    };
    App {
        host: cfg.get("host", "0.0.0.0"),
        port: cfg.get_int("port", 8080),
    };
}
$ hale run configured.hl
listening on 0.0.0.0:8080
Configure a param that doesn't exist.
host: cfg.get("host", "0.0.0.0"),
hostname: cfg.get("host", "0.0.0.0"),
$ hale check configured.hl
configured.hl:15:9: type error: locus `App` has no field `hostname`
            hostname: cfg.get("host", "0.0.0.0"),
            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

The same locus, compiled for the browser

target wasm { } is a declaration the typechecker enforces. The portable standard library and the typed bus work as they do natively, and the syscall-backed namespaces are refused at compile time. The break reaches for std::http inside the sandbox and is told why not. @export methods become the module's exports, and the page drives them.

Read WebAssembly & the browser →Run Hale in the playground ↗
counter.hleveryday
target wasm { }

@ffi("js") fn console_log(msg: String);

@export locus Counter {
    params { clicks: Int = 0; }

    birth() { console_log("counter ready"); }

    fn bump() {
        self.clicks += 1;
        console_log("clicks: " + to_string(self.clicks));
    }
}
Reach for sockets inside the sandbox.
birth() { console_log("counter ready"); }
        console_log("counter ready");
        let r = std::http::get("https://example.com/config") or { return; };
    }
$ hale check counter.hl
counter.hl:10:17: type error: `std::http::get` is unavailable under `target wasm`: the `std::http` server is built on raw TCP and isn't available in the browser
            let r = std::http::get("https://example.com/config") or { return; };
                    ^^^^^^^^^^^^^^

Complete programs

Whole programs, read top to bottom. The code on each page concatenates to the exact program the build verified.

80 lines · chat.hlA chat server that runs itselfRooms as keyed topics, a sealed session signer, supervision that recovers on the page, and a rule about who may sign.48 lines · orders-api.hlA small JSON APITyped JSON in and out, a stateful handler, a router and a server, all from the standard library.23 lines · intake.hlTwo binaries, one lawSeparate builds sharing a topic over a socket, composed and checked as a fleet. Drift in either binary fails the plan.81 lines · pipeline.hlA sharded sensor pipelineKeyed fan-out, placement, a certified hot path, a causal boundary, and the whole run recorded and replayed.

One guarantee at a time

The same discipline at snippet scale: the honest version and a one-line break, with the compiler's refusal beside it.

A sharded job queue

A keyed topic delivers each job only to the worker whose key it carries. The handler never sees the other shards. The routing contract is typed: the break removes the field the topic shards on.

Read the job-queue tutorial →
workers.hlsystems
type Job { queue_id: Int; body: String; }
topic JobReady { payload: Job; keyed_by queue_id; }

locus Worker {
    params { queue_id: Int = 0; done: Int = 0; }
    bus { subscribe JobReady as perform where key == self.queue_id; }
    fn perform(job: Job) {
        self.done = self.done + 1;
        println("worker ", self.queue_id, " took ", job.body);
    }
}

main locus App {
    params { a: Worker = Worker { queue_id: 1 }; b: Worker = Worker { queue_id: 2 }; }
    bus { publish JobReady; }
    run() {
        JobReady <- Job { queue_id: 1, body: "resize" };
        JobReady <- Job { queue_id: 2, body: "transcode" };
        JobReady <- Job { queue_id: 1, body: "thumbnail" };
    }
}
fn main() { App { }; }
$ hale run workers.hl
worker 1 took resize
worker 2 took transcode
worker 1 took thumbnail
Drop the field the topic shards on.
type Job { queue_id: Int; body: String; }
type Job { body: String; }
$ hale check workers.hl
workers.hl:2:41: type error: topic `JobReady`'s `keyed_by` references field `queue_id`, which does not exist on payload type `Job`
    topic JobReady { payload: Job; keyed_by queue_id; }
                                            ^^^^^^^^
workers.hl:17:27: type error: type `Job` has no field `queue_id`
            JobReady <- Job { queue_id: 1, body: "resize" };
                              ^^^^^^^^^^^
workers.hl:18:27: type error: type `Job` has no field `queue_id`
            JobReady <- Job { queue_id: 2, body: "transcode" };
                              ^^^^^^^^^^^
workers.hl:19:27: type error: type `Job` has no field `queue_id`
            JobReady <- Job { queue_id: 1, body: "thumbnail" };
                              ^^^^^^^^^^^

A causal boundary

The dependency set is checked transitively through the bus graph, so a republisher cannot launder an undeclared source into this locus. Subscribe to one topic the declaration does not name, and the build stops.

Read effects and causality →
risk-view.hlsystems
type Snapshot { id: Int; }
type Config   { limit: Int; }
type Tick     { n: Int; }

topic RiskSnapshot { payload: Snapshot; }
topic RiskConfig   { payload: Config; }
topic Clock        { payload: Tick; }

@effects(depends: {RiskSnapshot, RiskConfig})
locus RiskView {
    params { seen: Int = 0; }
    bus {
        subscribe RiskSnapshot as update;
        subscribe RiskConfig as configure;
    }
    fn update(s: Snapshot) { self.seen = self.seen + 1; }
    fn configure(c: Config) { self.seen = self.seen + 1; }
}

main locus App {
    params { v: RiskView = RiskView { }; }
    bus { publish RiskSnapshot; publish RiskConfig; publish Clock; }
    run() { RiskSnapshot <- Snapshot { id: 1 }; }
}
fn main() { App { }; }
Listen to the clock without declaring it.
        subscribe RiskConfig as configure;
        subscribe Clock as tick;
    fn configure(c: Config) { self.seen = self.seen + 1; }
    fn tick(t: Tick) { self.seen = self.seen + 1; }
$ hale check risk-view.hl
risk-view.hl:9:10: type error: declared dependency set violated: `RiskView` can transitively depend on `Clock` through the bus, which its `@effects(depends: …)` does not declare. It is subscribed directly by `RiskView`. Add the subject to the set, or route the input through a subject this locus doesn't reach.
    @effects(depends: {RiskSnapshot, RiskConfig})
             ^^^^^^^

A certified hot path

This path promises to avoid the kernel, waiting and allocation, and the compiler holds it to that. It follows the callees and rejects the build when the promise stops being true, counting the exact allocation that broke it.

Read effects and contracts →
score.hlsystems
type Sample { a: Float; b: Float; w: Float; }

@no_block @no_syscall @deterministic
@budget(alloc_per_call = 0)
fn score(sample: Sample) -> Float {
    return sample.a * sample.w + sample.b * (1.0 - sample.w);
}

fn main() {
    let s = Sample { a: 0.9, b: 0.4, w: 0.75 };
    println("score ", score(s));
}
$ hale run score.hl
score 0.775
Build a label on the hot path.
    return sample.a * sample.w + sample.b * (1.0 - sample.w);
    let label = "sample-" + to_string(sample.w);
$ hale check score.hl
score.hl:5:4: type error: hot-path budget exceeded: `score` declares `@budget(alloc_per_call = 0)` but the compiler counts 1 arena allocation(s) per call. For a zero-alloc hot path: hoist per-iteration allocations to reused fields, read with `recv_into` into a reused `std::bytes::BytesBuilder`, and keep locus instantiation out of the fn. If the allocation is intentional, drop `@budget` for `@unbounded fn`.
    fn score(sample: Sample) -> Float {
       ^^^^^
score.hl:6:17: type error: counts against `score`'s alloc budget: a string concatenation (each `+` builds a fresh String)
        let label = "sample-" + to_string(sample.w);
                    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

A confined secret

A sealed locus owns its params outright; everyone else holds a handle; the key stays inside. Reading the field from outside fails the build, and the diagnostic names the method to call instead.

Read the secrets article →
signer.hlsystems
@sealed locus Signer {
    params { key: Int = 7; }
    @effects(is: {secret_use})
    fn sign(msg: Int) -> Int { return msg * 31 + self.key; }
}

locus Gateway {
    params { s: Signer = Signer { }; }
    fn tag(msg: Int) -> Int {
        return self.s.sign(msg);
    }
}

fn main() {
    let g = Gateway { };
    println("sig ", g.tag(41));
}
$ hale run signer.hl
sig 1278
Read the key instead of asking for a signature.
        return self.s.sign(msg);
        let direct = self.s.key;
        return msg * 31 + direct;
$ hale check signer.hl
signer.hl:10:22: type error: `Signer` is `@sealed`: its `params` are readable only from inside its own methods, and `Signer.key` reads one from outside — call one of its methods instead (sign)
            let direct = self.s.key;
                         ^^^^^^^^^^

A claim with a witness

Two lines of law about the program itself. Wire a signer into the plugin host and the violation names the exact call chain that crosses the boundary, as a counterexample.

Read the claims article →
app.hlsystems
@sealed locus Signer {
    params { key: Int = 7; }
    @effects(is: {secret_use})
    fn sign(msg: Int) -> Int { return msg * 31 + self.key; }
}

locus Gateway {
    params { s: Signer = Signer { }; }
    fn issue(msg: Int) -> Int { return self.s.sign(msg); }
}

locus PluginHost {
    params { n: Int = 0; }
    fn render(x: Int) -> Int { return x + self.n; }
}

group plugins  = { PluginHost };

main locus App {
    params { g: Gateway = Gateway { }; p: PluginHost = PluginHost { }; }
    claims {
        plugins_never_sign:
            forbid reaches(plugins, effects(secret_use));
    }
    run() { let sig = self.g.issue(41); }
}
fn main() { App { }; }
Hand the plugin host a signer.
locus PluginHost {
    params { n: Int = 0; }
    fn render(x: Int) -> Int { return x + self.n; }
}
    params { n: Int = 0; s: Signer = Signer { }; }
    fn render(x: Int) -> Int { return self.s.sign(x); }
$ hale check app.hl
app.hl:22:9: type error: claim `plugins_never_sign` violated: `plugins` reaches `effects(secret_use)` — witness: `PluginHost::render` -> `Signer::sign`
            plugins_never_sign:
            ^^^^^^^^^^^^^^^^^^
app.hl:14:39: type error: claim `plugins_never_sign`: the boundary into `effects(secret_use)` is crossed by this call
        fn render(x: Int) -> Int { return self.s.sign(x); }
                                          ^^^^^^^^^^^^^^
app.hl:1:15: type error: claim `plugins_never_sign`: the forbidden destination `Signer` is declared here
    @sealed locus Signer {
                  ^^^^^^

Record and replay

Twenty readings of a random sensor, recorded: the schedule and the journaled inputs. The replay serves the same random values back in the same per-consumer order, and the comparison signs off. No logging calls and no instrumentation; the runtime is the thing delivering the messages.

Read the record & replay article →
sensor.hlsystems
type Reading { v: Int; }

locus Aggregator {
    params { total: Int = 0; count: Int = 0; }
    bus { subscribe Sensor as ingest; }
    fn ingest(r: Reading) {
        self.total = self.total + r.v;
        self.count = self.count + 1;
    }
}

topic Sensor { payload: Reading; }

locus Probe {
    bus { publish Sensor; }
    run() {
        let mut i = 0;
        while i < 20 {
            Sensor <- Reading { v: std::rand::next_int(100) };
            i = i + 1;
        }
    }
}

main locus App {
    params { a: Aggregator = Aggregator { }; p: Probe = Probe { }; }
    placement { p: pinned(core = 0); }
    run() { std::time::sleep(700ms); }
}
fn main() { App { }; }
$ LOTUS_OBS_RECORD=session.halerec hale run sensor.hl
$ hale replay session.halerec sensor.hl --allow-live-effects --diff
hale replay: journal served fully — 0 divergences, 20 consumes
replay matches the recording (110 ring records). Compared, by category:
  public bus events:     40 across 1 consumer (publish + deliver, subject-aligned)
  payloads:              20 (sizes and identities; contents not canonicalised)
  queued consumes:       20 across 1 consumer (per consumer, in recorded order)
  async schedule steps:  not exercised: no async pool scheduling steps were recorded
  journal reads:         20 (kind, args, withheld state, value)
A category reported as not exercised was NOT verified by this match.

The whole progression

The browser tour moves from ordinary functions to loci, typed topics, supervision and deployment without changing tools.

Open the playground