The showcase

#!/usr/bin/env weir
#sig git
// weir showcase — one runnable tour of the language.
// `weir check examples/showcase.weir` finds every error before any
// line runs; `weir examples/showcase.weir [--verbose] [--tag x]`
// executes. Portable by construction: the only external heads are
// `weir` itself and `git`, so the tour runs on Linux, macOS, and
// Windows alike (coreutils are cmd builtins there — nothing for a
// resolver to find). The POSIX escape hatch is still a feature:
// sh -c "..." on POSIX, cmd /c on Windows — spelled here in prose
// because a named head must resolve on your platform.
// The tour now hosts its own module (showcase-lib.weir), a vendored
// schema and a hand-written git signature (examples/.weir/ — checked
// in, so `check` needs no restore and no network). Still not here,
// each with its reason: the REPL (interactive by nature) and
// `weir add sig` generation (spawns the probed tool — this tour
// stays deterministic; the signature here is hand-written instead,
// which demos the partial-by-default ruling).

a user module: import goes before all declarations

// qualified access always; the module is declaration-only by law

import "./showcase-lib.weir" as Lib

typed argv: flags derive from a record

type Cli = {
    [<Short "v">]
    /// chatty progress on stderr
    verbose: bool

    [<Default 6>]
    /// upper bound for the number demos
    limit: int

    [<Default 30s>]
    /// a Duration flag: --timeout 90s or 1m30s parses at the boundary
    timeout: Duration

    [<Default 0.5>]
    /// a float flag: --rate 0.25 parses; the default renders in --help
    rate: float

    /// optional label stamped into the YAML demo
    tag: Option<string>
}

let cli = Args.load Cli

typed environment

type Level = Debug | Info | Quiet

type EnvCfg = {
    /// absent on stock Windows — Option is the honest type
    HOME: Option<string>

    /// POSIX spelling of the temp root
    TMPDIR: Option<string>

    /// Windows spelling of the temp root
    TEMP: Option<string>

    /// enum env vars match case-insensitively: =debug, =DEBUG, =Debug
    WEIR_SHOWCASE_LEVEL: Option<Level>
}

let env = Env.load EnvCfg
let level = env.WEIR_SHOWCASE_LEVEL |> Option.defaultValue Info
let home = env.HOME |> Option.defaultValue "(no HOME)"

printerr $"starting under {home} (level {level}, pid {Self.pid})"

if cli.verbose then printerr (show cli)

// the platform's own temp root — Option combinators over a match
let tmpBase =
    env.TMPDIR
    |> Option.orElse env.TEMP
    |> Option.defaultValue "/tmp"

// the showcase's helper scripts live beside this file — Self.scriptPath
// is absolute and cd-proof, so the tour runs from any cwd
let helperDir = Path.dir Self.scriptPath
let echoArgs = Path.combine helperDir "echo-args.weir"
let probe = Path.combine helperDir "probe.weir"

strings: five kinds, one meaning everywhere

let who = "world"
print $"hello {who} with {{literal braces}}"
print @"C:\verbatim\no-escapes"
print """say "hi" with no escapes at all"""
// the raw interpolated kind [D:interp-raw]: escapes off and holes on — a
// backslash, a quote and a splice in one literal, which is what generating
// weir from weir needs (there is no $@"…"; one spelling)
print $"""raw+holes: File.read "{who}\keep" — no escape pass, one splice"""

// ranges are lazy; comprehensions are eager
let squares = [for n in [1..cli.limit] -> n * n]
print $"sum of squares to {cli.limit}: {squares |> Seq.sum}"

the heredoc blocks: multiline lines, holes on the $ forms

// line-end <<< opens the plain block: every byte below is content ($ and
// { included), indentation is relative to the first line, and the value
// is seq<string> — File.write, pipes and Seq take it unchanged

let plain = <<<
    $HOME and {braces} are bytes here
    a second line

print $"plain heredoc: {plain |> Seq.length} lines, every byte literal"

// $<<< is the interpolated twin with the string forms' hole rules:
// {expr} substitutes, {{ }} are literal braces, $ still stays a byte;
// the blank line above `print` is layout — trailing blanks clip
let motd = $<<<
    hello {who} from the heredoc
        deeper indent survives; $PATH and {{braces}} are bytes

motd |> Seq.iter print

// $$<<< is the splice twin for brace-heavy text [D:heredoc-splice]:
// $name and ${expr} substitute, $$ is a literal $, and braces and
// quotes are all literal — where $<<< opens {expr} holes and needs
// {{ }} for literal braces, $$<<< keeps a pasted JSON blob intact and
// splices with the $ forms instead. It substitutes raw, so the proof
// here is a round trip: the templated text parses through the json
// adapter (reach for `to json` when a value is untrusted)
let dbHost = "db.internal"
let conf = $$<<<
    {"server": "$dbHost", "port": ${4000 + cli.limit}, "glob": "src/{a,b}"}
|> from json {| server: string; port: int; glob: string |}

print $"spliced json parses: {conf.server}:{conf.port} glob {conf.glob}"

tuples, records, copy-and-update

let pair = 3, "three"
let n0, name0 = pair
print $"{n0} spells {name0} (fst = {fst pair})"

// the qualified literal: a module's record type, built here — types
// cross the boundary, and inference names the literal Lib.Ctx { … }
let ctx = Lib.Ctx { name = "tour"; port = 4040 }
print (Lib.label ctx)

type Endpoint = { Host: string; Port: int }

let dev = { Host = "localhost"; Port = 8080 }
let prod = { dev with Port = 443 }
print $"{prod.Host}:{prod.Port}"
// a hole renders any Show value — records included; `show` itself is
// for point-free positions (Seq.map show) and Secrets (masked)
print $"{prod}"

unions, match, guards

type Verdict =
    | Pass of int
    | Again of string * int
    | Reject

let judge score =
    if score > 90 then Pass score
    elif score > 50 then Again ("close", score)
    else Reject

// constructor patterns need a known scrutinee — the pipeline types v
[95; 100; 60; 10]
    |> Seq.map judge
    |> Seq.map (fun v ->
        match v with
        | Pass n when n == 100 -> "perfect"
        | Pass n -> $"pass ({n})"
        | Again (why, n) -> $"retry {n}: {why}"
        | Reject -> "reject")
    |> Seq.iter print

// or-patterns share one arm [D:or-patterns]: each alternative counts
// toward exhaustiveness, so dropping a case is still a check error
let inPlay v =
    match v with
    | Pass _ | Again _ -> true
    | Reject -> false

print $"in play: {[95; 60; 10] |> Seq.map judge |> Seq.map inPlay |> Seq.freeze}"

inferred constraints: == is generic, zero runtime checks

let same x y = x == y
let sameInts = same 1 1
let sameStrs = same "a" "a"
print $"generic == on ints: {sameInts}; on strings: {sameStrs}"

Duration and floats: time as a type, decimals at the edges

// the same / glyph, two algebras: a Duration is integer ms by law,
// so Duration / int stays integer (half is 15s, no fraction) …
let half = cli.timeout / 2
// … while toSeconds returns floats, so THIS / is float division —
// visible in the output: 60.0 keeps its .0 (a float never renders
// as an int; finite-only, and == on floats is a check error)
let ratio = Duration.toSeconds cli.timeout / Duration.toSeconds 1m
print $"budget {cli.timeout}, half {half}"
print $"ratio {ratio} of {Duration.toSeconds 1m} seconds, at rate {cli.rate}"
Duration.sleep 1ms // takes a Duration, not a number; module-qualified so coreutils sleep stays reachable

// absolute time is `Instant` [D:instant] — a point on the UTC timeline, the
// boring subset: no local zones and no calendar arithmetic, so the only
// algebra is the one above — two instants subtract to a Duration
let cut = Instant.parse "2026-08-09T12:00:00Z"
let later = Instant.parse "2026-08-16T18:30:00Z"
print $"between the two tags: {later - cut} (from {cut})"

// retry: the bounded condition loop (a bool body IS the predicate,
// yields unit; poll is the time-bounded twin — timeout=/interval=)
retry attempts=2 delay=10ms
    weir -e "print 7" | succeeds

// poll, the wall-clock twin, with the `until` segment: a value body
// cannot be its own predicate, so `until` names the body's binding
// and reads it — two segments, both heads at column 0; the block
// yields the value once the condition holds
let polled = poll timeout=2s interval=10ms
    let r = weir -e "print 9" | complete
    r
until r
    r.exitCode == 0
print (polled.stdout |> Seq.exactlyOne)

seqs: Regex patterns, choose, seq patterns, fold

let logs = ["ok 200 /index"; "noise"; "ok 404 /missing"; "ok 200 /api"]

let hits =
    logs
    |> Seq.choose (fun l ->
        match l with
        | Regex @"ok (\d+) (\S+)" (code, path) -> Some (code, path)
        | _ -> None)
    |> Seq.freeze

hits |> Seq.iter (fun (c, p) -> print $"{c} <- {p}")

let headline =
    match hits with
    | [] -> "no hits"
    | (code, _) :: rest -> $"first code {code}, {rest |> Seq.length} more"

print headline

type Tally = { Big: int; Small: int }

let step t n =
    if n > 4 then { t with Big = t.Big + 1 }
    else { t with Small = t.Small + 1 }

let tally = [1..9] |> Seq.fold step { Big = 0; Small = 0 }
print $"{tally}"

let normalize = Str.trim >> Str.toLower
print (normalize "  MiXeD Case  ")

let jumps =
    [3; 7; 12; 20]
    |> Seq.pairwise
    |> Seq.map (fun (a, b) -> $"{b - a}")

// print streams a seq<string> one line per element (the pointwise
// spelling, `Seq.iter print`, does exactly the same — one wins here)
jumps |> print

// the scrape idiom: every match's groups, lazily, deduped
let page = "see https://weir.dev/a then https://weir.dev/b then https://weir.dev/a"

Str.rmatchAll @"(https://\S+)" page
    |> Seq.map Seq.head
    |> Seq.distinct
    |> Seq.iter print

commands: argv is data, never a string

// a child weir is the portable effectful command — same argv law on
// every platform, no shell between us and it

let banner = "showcase"
weir $echoArgs tag $banner (40 + 2) $"--label={banner}"

// extras is typed seq<string> by the splat's demand below
let extras = []
weir $echoArgs empty splat drops $@extras zero words

let words = ["alpha"; "beta"; "gamma"]
weir $echoArgs three words: $@words

let caught = weir -e "[\"one\"; \"two\"] |> Seq.iter print" |> Seq.length
print $"captured {caught} lines"

weir $probe --out "effect streams"

// exit codes are data: the reifier family
let found = weir $probe --out hit | succeeds
print found

let r = weir $probe --out out --err err --code 3 | complete
print $"complete: code {r.exitCode}, {r.stdout |> Seq.length} out, {r.stderr |> Seq.length} err"

let code = weir $probe --code 0 | exitCode
print $"exitCode reified: {code}"

weir $probe --out assert-me | orFail "the probe broke"

// | line reifies a one-value command [D:reify-line]: exactly one
// trimmed line of stdout, captured as a string — the
// $(cmd) |> Seq.exactlyOne mouthful as one reifier; a nonzero exit
// and zero-or-many lines both raise
let solo = weir -e "print \"solo\"" | line
print $"line-reified: {solo}"

// | text is its multi-line sibling [D:reify-text]: the whole stdout as
// one string, trailing blank lines dropped (bash's $(…))
let both = weir -e "print \"top\"; print \"bottom\"" | text
print $"text-reified: {both |> Str.replace "\n" " / "}"

// a weir seq pipes into an external's stdin
let loud = ["alpha"; "beta"] | weir $probe --upper |> Seq.head
print $"stdin-piped upcase: {loud}"

// typed command output: the Regex pattern for line shapes, the json
// adapter for structure. The #sig at the file head checks git's
// flags: `--porcelian` here would warn with a did-you-mean (partial
// signature — the e2e battery carries the executable proof)
let staged =
    git status --porcelain
    |> Seq.choose (function
        | Regex @"^[^ ?]. (.*)$" path -> Some path
        | _ -> None)
    |> Seq.length

print $"staged files here: {staged}"

type Peer = { host: string; port: int; note: Option<string> }

// a heredoc block is a seq<string> value — it pipes straight into the
// json adapter, no escaped-quote seq literal needed
let peer = <<<
    {"host": "a.example", "port": 9000}
|> from json Peer

print $"peer {peer.host}:{peer.port} (note {peer.note})"

// a record field splices as one argv word [D:field-splices]
weir $echoArgs peer $peer.host

files, paths, glob — inside `within tmp`

// the scope creates the directory and deletes it at block end: the
// cleanup is the scope, not a trailing chore (redirects are functions)

within tmp scratch
    let store = Path.combine scratch "roundtrip.txt"
    words |> File.write store
    ["delta"] |> File.append store
    let back = File.read store
    print $"file roundtrip: {back |> Seq.length} lines in {Path.fileName store}"
    // xs[0] raises out of range (it IS Seq.item 0); tryItem asks instead
    print $"first back: {back[0]}; missing 99th: {back |> Seq.tryItem 99}"
    let txts = Path.glob (Path.combine scratch "*.txt") |> Seq.freeze
    print $"glob sees {txts |> Seq.length} txt file(s); stem = {Path.stem store}"
    // File.size is a `Size`, not an int: binary units, comparable directly
    // (`> 10MiB` needs no arithmetic), which is why the row carries the type
    print $"size {File.size store}; over a KiB? {File.size store > 1KiB}"
always
    // any scope takes a trailing always [D:within-always-any]: it runs on
    // every exit, inside the scope — the directory is still there
    print $"always sees scratch: {Dir.exists scratch}"

Path.home and the XDG trio: the typed stand-in for ~

// a typed ~ in a command line is home, expanded when the line runs
// (`cat ~/.bashrc`) [D:tilde]; in an expression the path is built:
// Path.home and configHome/stateHome/cacheHome are pure
// unit -> string queries with platform-native resolution (the
// XDG vars with ~/.config-style fallbacks on POSIX, the APPDATA pair
// on Windows). Read-only here: resolve where a config would live and
// probe for it — nothing under home is written

let cfgHome = Path.configHome ()
let weirCfg = Path.combine cfgHome "weir"
print $"config root leaf: {Path.fileName cfgHome}; a weir config dir there: {Dir.exists weirCfg}"
print $"home resolves: {(Path.home () |> Str.length) > 0}; state/cache leaves: {Path.stateHome () |> Path.fileName} + {Path.cacheHome () |> Path.fileName}"

env overlays: one command, a block, a capture

let envFile = Path.combine tmpBase $"weir-showcase-{Self.pid}.env"
["GREETING=bonjour"; "SECRET=hunter2"] |> File.write envFile
let ev = Env.fromFile envFile

// the same command twice: first captured under the overlay…
let greetz = $ev(weir $probe --greet | line)
print greetz

// …then run under it — streams to the terminal, raises on failure
within env ev
    weir $probe --greet

let ready = true

// within env distributes the overlay over a whole block
within env ev
    weir $probe --greet --out "scoped one"
    weir $probe --greet --out "scoped two"

// literal variables need no file: NAME=value sets them for one command
// [D:env-prefix], and the same words on within env scope a block
// [D:within-env-pairs]
GREETING=hola weir $probe --greet
within env GREETING=salut
    weir $probe --greet --out "pairs scope"

// within cd is the third scope kind (tmp ran the files section above):
// the working directory changes for the block and restores at its end
within cd helperDir
    // pwd is a weir builtin (like ls/cd) — no PATH head resolves here,
    // so the weir+git-only portability claim in the header holds
    let here = pwd
    print $"cd-scoped: running beside {Path.fileName here}"

// commands are ordinary statements inside any block — parsed and
// checked before anything ran, no mode gate needed
if ready then
    weir $echoArgs bare block line one
    weir $probe --code 0 | orFail "the probe broke"

iteration: for/do effects, parallel fan-out

for w in words do print $"word: {w}"

for f in $(weir -e "[\"one\"; \"two\"] |> Seq.iter print") do weir $echoArgs iter $f

for s in ["first"; "second"] do
    weir $echoArgs command block $s

let shouts =
    ["fan"; "out"]
    |> Seq.pmap (fun w -> weir $probe --out $w | line)

shouts |> print

// a lambda body takes command lets, like a for body [D:lambda-lets]
words |> Seq.take 1 |> Seq.iter (fun w ->
    let r = weir $probe --out $w | complete
    print $"lambda let: {w} exit {r.exitCode}")

YAML: nodes, adapters, and the checked template district

// YMap/YStr (with YInt, YSeq, …) are YAML node values built directly —
// a YMap keeps your insertion order, where a record renders in declared
// field order; both are one `to yaml` away from text
let ordered = YMap ["zulu", YStr "keeps"; "alpha", YStr "your order"]
ordered |> to yaml |> print

type PeerDoc = { host: string; port: int }

// a top-level sequence document reads through the seq form — the
// declared type names the top level (streams are one-document-only)
let peers =
    ["- host: a.example"; "  port: 9000"; "- host: b.example"; "  port: 9001"]
    |> from yaml seq<PeerDoc>

peers |> Seq.iter (fun p -> print $"peer {p.host}:{p.port}")

// the yaml DISTRICT: a checked block literal. Structure errors are
// check errors; splices are typed values, so no YAML injection exists
// for the same reason no argv injection does; a None splice omits its
// entry; `for k, v in pairs` destructures each pair to a dynamic key
// (`$k:`) and its value; ambiguous scalars auto-quote.
// a real Service shape (the live-check finding: `annotation` was a
// typo the schema validator caught unprompted, and replicas/rollout
// were Deployment concepts on a Service — the district now describes
// the resource it names). The "on" annotation keeps the auto-quote
// demo: unquoted it would read as YAML's boolean.
let manifest name port tag pairs = yaml
    apiVersion: v1
    kind: Service
    metadata:
        name: $name
        annotations:
            weir.dev/tag: $tag
            weir.dev/switch: "on"
        labels:
            for k, v in pairs
                $k: $v
    spec:
        selector:
            app: $name
        ports:
            - port: $port

let svc = manifest "web" 8080 cli.tag ["app", "web"; "tier", "edge"]
svc |> to yaml |> print

// a district validated against a vendored schema (examples/.weir/
// schemas/, committed + locked): structure errors become check errors
// — misspell `apiVersion` and this file refuses to run
let cm = yaml schema=k8s-configmap
    apiVersion: v1
    kind: ConfigMap
    metadata:
        name: showcase-config
    data:
        mode: tour

cm |> to yaml |> print

cleanup: File.delete asserts its target exists

// envFile stays manual on purpose: ev outlives any one block (the
// sigil pair and the within env section both use it), so a tmp scope
// cannot own it — and the one remaining delete demos the member.
// (the tmp scope already deleted its own files at block end)

File.delete envFile

bindings shadow commands; ^ still reaches PATH

// order is load-bearing: this section stays last — the binding shadows
// the `weir` command for every line after it

let weir = "a local binding now shadows the command name"
print $"shadow: {weir}"

let v = ^weir --version | line
print $"^weir still reaches the binary: {v}"

exit is explicit; unit prints nothing

// the default run shows only the Info arm — WEIR_SHOWCASE_LEVEL=debug
// (or =quiet) steers the others
match level with
| Debug -> printerr "debug: every section ran"
| Info -> printerr "done"
// unit prints nothing — quiet really is silent
| Quiet -> print ()

print "showcase complete"