@@ -60,7 +60,15 @@ let (module, parse_diags) = parser.parse_module();
6060
6161### Runtime (`crates/knot-runtime/`)
6262
63−Compiled as a `staticlib` (with `rlib` for workspace dependency resolution). All functions use `extern "C"` ABI, called by Cranelift-generated code via symbol references.
63+Compiled as a `staticlib` (with `rlib` for workspace dependency resolution). All functions use `extern "C"` ABI, called by Cranelift-generated code via symbol references. `lib.rs` is the main runtime; `log.rs` implements the leveled logger used by `logInfo`/`logWarn`/`logError`/`logDebug` (TTY-colored on stderr or one JSON record per line; `--debug` arg scanned by `debug_enabled()` gates `logDebug`); `tui.rs` is the `db` subcommand's terminal-UI database explorer (parses `_knot_schema`, paginates rows, drills into individual records).
64+
65+Compiled programs expose a common CLI without any user wiring:
66+- `--debug` — enable `logDebug` output
67+- `--help` — print usage including any compile-time overrides exposed via `knot_override_check_help` (the compiler emits this list at codegen time)
68+- `--http-max-body-bytes=N` — cap HTTP request and response bodies (`K`/`M`/`G` suffixes, default `16M`); applies to both `listen` and `fetch`
69+- `--<name>=<value>` — override a compile-time constant declared in the source (same flags accepted both at `knot build` and at run time)
70+- `<program> db` — dispatched by `knot_db_handle` to `tui::run_db_explorer`, opens the program's `<name>.db` in an interactive explorer
71+- `<program> api <RouteName>` — dispatched by `knot_api_handle`, prints an OpenAPI 3.0 JSON spec for the named route (generated by `generate_openapi`)
6472
6573- All Knot values are `*mut Value` (heap-allocated tagged enum); integers are unbounded (`num_bigint::BigInt`); IO actions are `Value::IO(fn_ptr, env)` thunks executed via `knot_io_run`
6674- `rusqlite` with `bundled` feature statically links SQLite into every compiled binary
@@ -78,12 +86,12 @@ Compiled as a `staticlib` (with `rlib` for workspace dependency resolution). All
7886### Compiler (`crates/knot-compiler/`)
7987
8088- **Desugaring** (`desugar.rs`): Transforms "pure comprehension" do blocks into nested calls to `__bind`, `__yield`, and `__empty`. A pure comprehension is a do block with only Bind/Where/Let/Yield statements (no bare side-effecting expressions or `groupBy`). Do blocks that are direct values of `set`/`replace` expressions are NOT desugared (preserves SQL optimization patterns). Do blocks containing `groupBy` are NOT desugared (require loop-based codegen for the collect/group/re-iterate pattern). Do blocks containing constructor pattern binds (`Ctor pat <- expr`) are NOT desugared (the desugarer cannot syntactically distinguish value pattern matches from monadic binds; direct codegen handles both). Do blocks containing IO-returning expressions are NOT desugared — the desugarer's `expr_is_io` recognizes both external IO builtins (`println`, `readFile`, `now`, etc.) and relation operations (`SourceRef`, `DerivedRef`, `Set`, `ReplaceSet`, `At`) as IO, excluding these do blocks from desugaring so they go through the dedicated IO codegen path (`compile_io_do`) which runs each IO action with `knot_io_run` and wraps the result in `knot_io_pure`; this ensures IO do blocks inside if/then/else branches are typed correctly as IO rather than defaulting to relational. Mixed/sequential do blocks remain as `Do(stmts)` nodes for imperative codegen. The desugared `__bind`/`__yield`/`__empty` dispatch through Monad/Applicative/Alternative trait impls — the monad type is resolved at compile time via HKT unification (`monad_info` maps spans to `MonadKind::Relation`, `MonadKind::Adt(name)`, or `MonadKind::IO`), and codegen calls the appropriate `Monad_{type}_bind`, `Applicative_{type}_yield`, or `Alternative_{type}_empty` mangled function. This allows `do` blocks to work with any type implementing the Monad/Applicative/Alternative traits, not just `[]`.
81−- **Type inference** (`infer.rs`): Hindley-Milner type inference with row-polymorphic records and row-polymorphic variants, let-generalization, unification with occurs check, ADT constructor typing, trait method registration, associated type erasure, higher-kinded type polymorphism (`TyCon`/`App` type nodes with normalization-based unification), IO monad type (`Ty::IO(BTreeSet<IoEffect>, Box<Ty>)` with effect tracking for `Console`, `Fs`, `Network`, `Clock`, `Random`), units of measure (`Ty::IntUnit(UnitTy)`/`Ty::FloatUnit(UnitTy)` with normalized exponent-map representation `BTreeMap<String, i32>` plus optional `UnitVar` for polymorphism; unit algebra: `+`/`-` require unit match, `*`/`/` compose units, negation preserves units; plain `Int`/`Float` are unit-agnostic and unify with any `IntUnit`/`FloatUnit`; `Scheme` quantifies over both `TyVar`s and `UnitVar`s — instantiation freshens both; all stdlib functions with numeric types are unit-polymorphic — `avg` registered as `∀a u. (a -> Float<u>) -> [a] -> Float<u>`; `sum` already fully polymorphic in return type; `randomInt` as `∀u. Int<u> -> IO {random} Int<u>` (preserves bound unit in result); `randomFloat` as `∀u. IO {random} Float<u>`; `now` as `IO {clock} Int<Ms>`; `sleep` as `Int<Ms> -> IO {clock} {}`; `Ms` registered as built-in unit (milliseconds) for clock operations; `count` as `∀a u. [a] -> Int<u>`; `length` as `∀u. Text -> Int<u>`; `take`/`drop` as `∀u. Int<u> -> Text -> Text`; `listen` as `∀a b u. Int<u> -> (a -> b) -> IO {network} {}`; `bytesLength` as `∀u. Bytes -> Int<u>`; `bytesSlice` as `∀u1 u2. Int<u1> -> Int<u2> -> Bytes -> Bytes`; `bytesGet` as `∀u1 u2. Int<u1> -> Bytes -> Int<u2>`; unit declarations collected in `collect_types`; derived unit aliases expand at use site), refined types (`type Nat = Int where \x -> x >= 0` — refined type aliases stay nominal as `Ty::Con(name, vec![])`, NOT resolved to base type; stored in `refined_types: HashMap<String, (Ty, Expr)>` mapping name to base type and predicate; subsumption rule in `unify`: when `Con(name, [])` is a refined type, unify with its base type — enables bidirectional compatibility `Nat ↔ Int`; `refine expr` typed as `Result RefinementError alpha` where `alpha` is fresh and constrained by context — post-inference resolves `alpha` to the refined type name for codegen; `RefinementError` registered as a type alias to `{typeName: Text, violations: [{field: Maybe Text, message: Text}]}`; `TypeKind::Refined { base, predicate }` in AST for inline refinements, stripped to base during schema resolution; `refine_vars: Vec<(Span, TyVar, Ty)>` tracks refine expressions for post-inference target resolution; `RefineTargets` and `RefinedTypeInfoMap` exported to codegen), and trait bound checking (explicit `TraitName a =>` constraints on function signatures are validated at call sites against known `impl` declarations; trait method calls automatically carry their trait's constraint). All relation operations return IO: `SourceRef` returns `IO {} [T]`, `DerivedRef` returns `IO {} [T]`, `Set`/`ReplaceSet` return `IO {} {}`; `Set`/`ReplaceSet` unify target and value by unwrapping IO from both sides. `Atomic` is typed as `IO {} a -> IO {} a` — body must be IO, enforced via unification; `in_atomic: bool` flag tracks context for `retry` validation. Built-in registrations include `fork : ∀r. IO r {} -> IO r {}` (the spawned IO's effect row propagates through `fork`, so its effects remain visible in the caller's IO type), `race : ∀a b r. IO r a -> IO r b -> IO r (Result a b)` (both args share an effect row that propagates to the result), `randomUuid : IO {random} Uuid`, and `retry : ∀a. a` (bottom type). New primitive `Ty::Uuid` in `infer.rs` with parser/printer/erasure plumbing parallel to `Ty::Bytes`. Built-in ADTs registered in `register_builtins`: `Maybe a` (`Nothing`/`Just`), `Result e a` (`Err`/`Ok`), `Bool` (`True`/`False`) — `Bool` constructors map to the primitive `Ty::Bool` (not `Ty::Con`), so `True {}` and `False {}` produce the same type as `true`/`false` literals; `Result` has built-in Functor/Applicative/Monad/Alternative impls for do-block support. Constructor patterns in `case` and do-bind create open variant types `<Ctor {} | r>` (the scrutinee only needs to *contain* the matched constructor), enabling row-polymorphic variant matching; when all constructors of a known data type are covered without a wildcard, the row variable is closed and exhaustiveness is checked normally; open variants require a wildcard `_` case
89+- **Type inference** (`infer.rs`): Hindley-Milner type inference with row-polymorphic records and row-polymorphic variants, let-generalization, unification with occurs check, ADT constructor typing, trait method registration, associated type erasure, higher-kinded type polymorphism (`TyCon`/`App` type nodes with normalization-based unification), IO monad type (`Ty::IO(BTreeSet<IoEffect>, Box<Ty>)` with effect tracking for `Console`, `Fs`, `Network`, `Clock`, `Random`), units of measure (`Ty::IntUnit(UnitTy)`/`Ty::FloatUnit(UnitTy)` with normalized exponent-map representation `BTreeMap<String, i32>` plus optional `UnitVar` for polymorphism; unit algebra: `+`/`-` require unit match, `*`/`/` compose units, negation preserves units; plain `Int`/`Float` are unit-agnostic and unify with any `IntUnit`/`FloatUnit`; `Scheme` quantifies over both `TyVar`s and `UnitVar`s — instantiation freshens both; all stdlib functions with numeric types are unit-polymorphic — `avg` registered as `∀a u. (a -> Float<u>) -> [a] -> Float<u>`; `sum` already fully polymorphic in return type; `randomInt` as `∀u. Int<u> -> IO {random} Int<u>` (preserves bound unit in result); `randomFloat` as `∀u. IO {random} Float<u>`; `now` as `IO {clock} Int<Ms>`; `sleep` as `Int<Ms> -> IO {clock} {}`; `Ms` registered as built-in unit (milliseconds) for clock operations; `count` as `∀a u. [a] -> Int<u>`; `length` as `∀u. Text -> Int<u>`; `take`/`drop` as `∀u. Int<u> -> Text -> Text`; `listen` as `∀a r u. Int<u> -> Server a r -> IO {network | r} {}` (and `listenOn` with an extra leading `Text` for the bind address); `bytesLength` as `∀u. Bytes -> Int<u>`; `bytesSlice` as `∀u1 u2. Int<u1> -> Int<u2> -> Bytes -> Bytes`; `bytesGet` as `∀u1 u2. Int<u1> -> Bytes -> Int<u2>`; unit declarations collected in `collect_types`; derived unit aliases expand at use site), refined types (`type Nat = Int where \x -> x >= 0` — refined type aliases stay nominal as `Ty::Con(name, vec![])`, NOT resolved to base type; stored in `refined_types: HashMap<String, (Ty, Expr)>` mapping name to base type and predicate; subsumption rule in `unify`: when `Con(name, [])` is a refined type, unify with its base type — enables bidirectional compatibility `Nat ↔ Int`; `refine expr` typed as `Result RefinementError alpha` where `alpha` is fresh and constrained by context — post-inference resolves `alpha` to the refined type name for codegen; `RefinementError` registered as a type alias to `{typeName: Text, violations: [{field: Maybe Text, message: Text}]}`; `TypeKind::Refined { base, predicate }` in AST for inline refinements, stripped to base during schema resolution; `refine_vars: Vec<(Span, TyVar, Ty)>` tracks refine expressions for post-inference target resolution; `RefineTargets` and `RefinedTypeInfoMap` exported to codegen), and trait bound checking (explicit `TraitName a =>` constraints on function signatures are validated at call sites against known `impl` declarations; trait method calls automatically carry their trait's constraint). All relation operations return IO: `SourceRef` returns `IO {} [T]`, `DerivedRef` returns `IO {} [T]`, `Set`/`ReplaceSet` return `IO {} {}`; `Set`/`ReplaceSet` unify target and value by unwrapping IO from both sides. `Atomic` is typed as `IO {} a -> IO {} a` — body must be IO, enforced via unification; `in_atomic: bool` flag tracks context for `retry` validation. Built-in registrations include `fork : ∀a r. IO {| r} a -> IO {| r} {}` (the spawned IO's effect row propagates through `fork`, so its effects remain visible in the caller's IO type), `race : ∀a b r1 r2. IO {| r1} a -> IO {| r2} b -> IO {| r1 \/ r2} (Result a b)` (each arg carries its own effect row; the result row is the union of both, expressed in the type with the `\/` operator — `ast_type_to_ty` registers the effect-union constraint and `generalize` captures it on the scheme), `randomUuid : IO {random} Uuid`, and `retry : ∀a. a` (bottom type). New primitive `Ty::Uuid` in `infer.rs` with parser/printer/erasure plumbing parallel to `Ty::Bytes`. Built-in ADTs registered in `register_builtins`: `Maybe a` (`Nothing`/`Just`), `Result e a` (`Err`/`Ok`), `Bool` (`True`/`False`) — `Bool` constructors map to the primitive `Ty::Bool` (not `Ty::Con`), so `True {}` and `False {}` produce the same type as `true`/`false` literals; `Result` has built-in Functor/Applicative/Monad/Alternative impls for do-block support. Constructor patterns in `case` and do-bind create open variant types `<Ctor {} | r>` (the scrutinee only needs to *contain* the matched constructor), enabling row-polymorphic variant matching; when all constructors of a known data type are covered without a wildcard, the row variable is closed and exhaustiveness is checked normally; open variants require a wildcard `_` case
8290- **Effect inference** (`effects.rs`): Infers per-declaration effects (`{r *rel}`, `{w *rel}`, `{rw *rel}` for both, `{console}`, `{clock}`, etc.), checks IO-in-atomic constraints (atomic blocks must only contain DB interactions — no console/fs/clock/random), validates that atomic blocks actually interact with relations (have reads or writes), validates explicit effect annotations against inferred effects. `rw *x` is shorthand for `r *x, w *x` — parsed as both effects, and the display coalesces matching pairs back to `rw *x`.
8391- **Type resolution** (`types.rs`): Resolves aliases (including multi-variant ADTs to `ResolvedType::Adt`), computes SQLite schemas from Knot type annotations, collects subset constraints; refined type aliases separated during collection — predicates stored in `refined_types: HashMap<String, Expr>`, base types stored in `aliases` for schema resolution; `TypeKind::Refined` transparent for schema — `resolve_type` and `apply_type_subst` recurse into base; `source_refinements: HashMap<String, Vec<(Option<String>, String, Expr)>>` maps source names to their field-level and whole-element refinement predicates (collected by `collect_source_refinements` walking source type ASTs)
8492- **Codegen** (`codegen.rs`): Cranelift IR generation — the `build_function` pattern moves `ctx`/`builder_ctx` out of `self` to avoid borrow conflicts while allowing `self.method()` calls during IR building
8593- **Linker** (`linker.rs`): Invokes `cc` with platform-appropriate flags
86−- **CLI** (`main.rs`): `knot build <file.knot>` entry point
94+- **CLI** (`main.rs`): subcommands `knot build <file.knot> [-o <path>] [--<name>=<value> …]` (compile to native executable; `--<name>=<value>` overrides compile-time constants), `knot fmt [--check] [--stdout] <file.knot> …` (in-place formatter; `--check` exits non-zero on diff, `--stdout` writes to stdout), and `knot help`. Object file is emitted next to the source then linked via `linker::link`; runtime is embedded via `build.rs` into `EMBEDDED_RUNTIME` and extracted to a temp file if `libknot_runtime.a` isn't found next to the compiler or via `KNOT_RUNTIME_LIB`.
8795
8896Key codegen patterns:
8997- All values are pointer-typed (`ptr_type`) in Cranelift IR — uniform representation
@@ -112,7 +120,7 @@ Key codegen patterns:
112120
113121## Supported Language Features
114122
115−Currently compiled: source declarations, type aliases, data declarations, functions, literals, records, field access, record updates, relation literals, nested relations (record fields holding `[T]` stored as JSON in SQLite, queryable via `m <- t.field` bind), binary/unary operations, if/else, do blocks (bind/where/yield/let/groupBy — pure comprehension do blocks are desugared to `__bind`/`__yield`/`__empty` calls that dispatch through Monad/Applicative/Alternative trait impls — works with any monad, not just `[]` (e.g., `Maybe`); monad type resolved at compile time via HKT unification; IO do blocks are excluded from desugaring and use the dedicated `compile_io_do` path; mixed/sequential do blocks use direct loop codegen; set-value do blocks preserved for SQL optimization; do blocks can appear in atom position as function arguments — `f do ...` and `f (do ...)` both work; `groupBy {key}` collects rows, groups by key, and rebinds the variable to each group sub-relation — field access on a group returns the first element's field, aggregates like `count` operate on the group), set expressions, lambdas, closures, function application, case expressions (with exhaustiveness checking for ADTs), constructors (including built-in `True {}`/`False {}` for `Bool` — interchangeable with `true`/`false` literals, usable in `case` patterns), atomic transactions, migrations (schema tracking + `migrate` blocks), schema lockfile (`<name>.schema.lock`), views (`*view = do { ... yield {...} }` with bidirectional read/write, constant column filtering, auto-fill on write), derived relations (`&name = expr` — read-only computed relations, compiled as 0-param functions recomputed on each access; recursive derived relations with self-references use Datalog-style fixpoint iteration via `knot_relation_fixpoint` runtime function, converging when the relation stabilizes), traits and impls (single-dispatch on runtime type tags for primitives and ADTs, default methods, deriving from defaults, supertrait enforcement, associated types with type-level pattern matching), trait bounds (`Display a => [a] -> [Text]` syntax — explicit constraints on function type signatures validated at call sites; trait method calls automatically carry constraints; multiple bounds via `Trait1 a => Trait2 a => Type`; compile-time error when a concrete type lacks a required impl), type inference (Hindley-Milner with row polymorphism for both records and variants, let-generalization, ADT/trait/view-aware, higher-kinded type polymorphism), higher-kinded types (trait params with kind annotations like `(f : Type -> Type)`, type-level application `f a` in method signatures, `[]` and ADT names as bare type constructors in impl args, `TyCon`/`App` internal representation with normalization-based unification), IO monad (`IO {effects} a` type for pure effect descriptions — all relation operations (`*rel`, `&rel`, `set`, `replace`) return `IO {} value` with empty effect set, external builtins like `println`, `readFile`, `now` return IO with specific effects; IO do-blocks sequence actions via bind; effects tracked in the type: `IO {console} {}`, `IO {fs} Text`, `IO {clock} Int`, `IO {} [T]` for DB ops; `knot_io_run` executes IO thunks at the top level in `main`), concurrency (`fork : ∀r. IO r {} -> IO r {}` fire-and-forget OS thread spawning with independent SQLite connections via WAL mode, deep-cloned environments — the spawned IO's effect row propagates through `fork`, so its effects remain visible in the caller's IO type; `race : ∀a b r. IO r a -> IO r b -> IO r (Result a b)` runs two IO actions concurrently with cooperative aggressive cancellation via per-thread `CancelToken` checked between IO thunks and inside `sleep`, winner is reported via the built-in `Result a b` ADT — `Err {error: a}` if left wins, `Ok {value: b}` if right wins; both args share an effect row that propagates to the result; `race` cannot appear inside `atomic`; `retry` for STM-style atomic retry — inside `atomic` blocks, causes rollback and waits for relation changes via Condvar with row-level read-filter wakeups so a watcher on `WHERE id = 1` is not woken by writes to `id = 2`, predicates support equality, ordered comparison (`<`/`<=`/`>`/`>=`), and `IN` sets; UPDATE/DELETE paths emit per-row `WriteEvent::Rows` so STM watchers can filter on those too; `atomic : IO {} a -> IO {} a` runs IO body in a transaction with savepoint-based retry loop, body must contain only DB interactions), pattern matching in do-bind (`Circle c <- *shapes` filters relation to matching constructors and destructures; `InProgress ip <- t.status` matches a single value and skips if no match), built-ins (println, print, show, union, count, countWhere, now, filter, match, map, fold, single, any, diff, inter, sum, avg, minOn, maxOn, min, max, toUpper, toLower, take, drop, length, trim, contains, reverse, chars, id, not, stripUnit/withUnit (Int<u> ↔ Int identity for unit conversion), stripFloatUnit/withFloatUnit (Float versions), toJson, parseJson, readFile, writeFile, appendFile, fileExists, removeFile, listDir, readLine, randomInt, randomFloat, randomUuid, fork, race, retry, sleep, logInfo/logWarn/logError/logDebug — leveled logging to stderr, colored when TTY / JSON otherwise; logDebug only emits when the program is run with `--debug` — IO-returning builtins produce `IO {effect} a` values; aggregates `count`/`countWhere`/`sum`/`avg`/`minOn`/`maxOn` push down to SQL (`COUNT(*)`/`COUNT(*) WHERE`/`SUM`/`AVG`/`MIN`/`MAX`) when applied to a source relation or its bound alias, including `filter`-then-aggregate, do-block-then-aggregate, and pipe forms (`*rel |> filter ... |> minOn ...`); `minOn`/`maxOn` use `knot_source_query_value` runtime which returns Int/Float/Text matching the SQLite column type and panics on empty relations; binary `min`/`max` (prelude functions, `Ord a => a -> a -> a`) operate on two values; modulo operator `%` dispatches through `Num.mod`, calls `knot_value_mod` at runtime (panics on division by zero), pushes down to SQLite's `%` operator inside SQL-compilable comprehensions; postfix type annotations on any expression (`expr : Type`) parse without surrounding parens — useful for unit ascription on literals; `Uuid` primitive type registered alongside `Bytes` in inference and resolution, stored as TEXT in SQLite, generated via `randomUuid : IO {random} Uuid` (RFC 9562 UUIDv7 — time-ordered, suitable as primary key); `Maybe` ships with built-in `Functor`/`Applicative`/`Monad`/`Alternative` impls in the prelude (parsed from `PRELUDE_SOURCE`, skipped when the user defines their own impl for the same `(trait, type)` pair via `user_impls` tracking in `inject_prelude`)), units of measure (`unit M`, `unit N = Kg * M / S^2` declarations — concrete units are uppercase; `Float<M>`, `Int<Usd>` type annotations; `42.0<M>` literal syntax; compile-time unit algebra — `+`/`-` require unit match, `*`/`/` compose units, negation preserves units; plain numeric types are unit-agnostic; unit polymorphism via lowercase unit variables in type annotations `Float<u> -> Float<u>` — lowercase names in `<...>` that are not declared units become polymorphic unit variables, freshened on each instantiation; units fully erased at runtime; all stdlib functions with numeric types are unit-polymorphic: `avg` as `∀a u. (a -> Float<u>) -> [a] -> Float<u>`, `sum`/`minOn`/`maxOn` fully polymorphic `(a -> b) -> [a] -> b` (units flow through naturally), `countWhere` as `∀a u. (a -> Bool) -> [a] -> Int<u>`, `randomInt` as `∀u. Int<u> -> IO {random} Int<u>` (preserves bound unit), `randomFloat` as `∀u. IO {random} Float<u>`, `now` as `IO {clock} Int<Ms>`, `sleep` as `Int<Ms> -> IO {clock} {}` (built-in `Ms` unit for clock ops), `count` as `∀a u. [a] -> Int<u>`, `length` as `∀u. Text -> Int<u>`, `take`/`drop` as `∀u. Int<u> -> Text -> Text`, `bytesLength`/`bytesSlice`/`bytesGet` also unit-polymorphic; derived unit aliases expand at use site; `(expr : Type)` annotation syntax for explicit unit ascription), refined types (`type Nat = Int where \x -> x >= 0` — base type restricted by predicate function; per-field `{age: Int where \x -> x >= 0}`, cross-field `{...} where \p -> p.lo <= p.hi`, ADT constructor `Circle {radius: Float where \r -> r > 0.0}` refinements; `refine expr` returns `Result RefinementError T` with target refined type inferred from context — `case refine x of Ok {value: n} -> ... | Err {error: e} -> ...`; refined types are nominal in inference (`Ty::Con(name, [])`) with subsumption in unification enabling `Nat ↔ Int` compatibility; `set` validates refined fields via `knot_refinement_validate_relation` before writes — panics on violation; route handlers auto-validate refined body fields after JSON decoding — return HTTP 400 on failure; `RefinementError = {typeName: Text, violations: [{field: Maybe Text, message: Text}]}`; `Result` has built-in monad impls via `knot_result_bind`/`knot_result_yield`/`knot_result_empty` for do-block support), effect inference (per-declaration effect tracking for reads/writes/console/clock/network/fs/random, IO-in-atomic validation, explicit annotation checking), subset constraints (`*orders.customer <= *people.name` for referential integrity, `*users <= *users.email` for uniqueness — validated at runtime before each write commits), routes (`route Name where` with HTTP method/path/body/query/response declarations, path prefix nesting, `route Name = A | B` composition, `headers {field: Type}` for typed request/response headers — request headers appear after query params and before `->`, response headers appear after the response type; header field names use camelCase and auto-convert to HTTP-Header-Case (`authorization` → `Authorization`, `contentType` → `Content-Type`); optional headers use `Maybe` type (`headers {authorization: Maybe Text}` — server gets `Nothing` if absent, `Just {value: "..."}` if present; fetch skips `Nothing` headers); request header fields become constructor fields like body/query/path params; routes desugar to ADTs whose constructors carry only request inputs (no `respond` field) — handlers are bound per-endpoint via `serve API where Ctor = handler` producing a value of type `Server API _` (a row variable when handlers have no concrete effects) or `Server API {effects}` (when handlers carry concrete effects), and each handler returns `Result HttpError T` where `T` is the response type declared in the route and `HttpError = {status: Int, message: Text}`. `Ok {value: T}` responds 200; `Err {error: {status, message}}` responds with the given status (clamped to 100..=599) and a JSON `{"error": message}` body. When response headers are declared, the success body is `{body: T, headers: H}` (still wrapped inside `Ok`); the listen loop extracts body for JSON and headers for HTTP response headers. Error responses do not carry custom headers. `listen : Int<u> -> Server a r -> IO {network | r} {}` starts a `tiny_http` server, dispatching requests to the appropriate handler with JSON request/response serialization; the row variable unifies with the server's effect row so handler effects (e.g. `console`) flow into the IO type of the program calling `listen`. `fetch url (Ctor {fields})` is a type-safe HTTP client reusing route declarations — response type inferred from route's `response:` annotation, returns `IO {network} (Result {status: Int, message: Text} ResponseType)` or `IO {network} (Result ... {body: ResponseType, headers: {h: T}})` when response headers declared. `fetchWith url {headers: [...]} (Ctor {fields})` variant merges ad-hoc headers with route-declared headers, uses `ureq` for HTTP requests. Per-endpoint rate limiting via the `rateLimit <expr>` clause placed after the response type/headers and before `=`: the expression has type `RateLimit input a = {key: input -> RequestCtx -> Maybe a, limit: {requests: Int, window: Int<Ms>}}` with `Ord a` enforced via a deferred constraint; `input` is the same record the handler receives (built from path params + query params + body fields + request headers — `route_input_record_ty` factored out of `serve_handler_type` for shared use); absence of the clause means unlimited; `key` returning `Nothing` exempts the request, `Just v` keys the bucket on `show v`. Token-bucket algorithm refilled lazily, persisted in `_knot_rate_limits (route TEXT, key TEXT, tokens REAL, last_refill INTEGER, PRIMARY KEY(route, key)) WITHOUT ROWID`, created on first use; check runs in `BEGIN IMMEDIATE` so concurrent same-key requests serialize. Codegen: parser introduces an `Option<Expr>` field on `RouteEntry`; type checker validates the expression in `check_rate_limit_expr` (called from `infer_declarations` Route arm); `can_start_type_atom` stops at `rateLimit` so the response type doesn't eat the keyword; runtime registers configs via `knot_route_set_rate_limit(table, ctor, rate_limit_value)` which unpacks the `{key, limit}` record; both the main_init route table loop and the `listen`/`listenOn` codegen path register them on their respective tables; check happens in the worker thread inside `catch_unwind`, after the input record is built but before refinement validation, so the user's `key_fn` sees the same destructured input the handler will. The worker's Err type is `(u16, String, Option<i64>)` where the third element is `retry_after_ms` — the response handler attaches `Retry-After: <seconds>` when present and uses `Content-Type: application/json` body `{"error":"..."}`; rate-limit rejections return `Err((429, "Rate limit exceeded", Some(retry_after_ms)))`).
123+Currently compiled: source declarations, type aliases, data declarations, functions, literals, records, field access, record updates, relation literals, nested relations (record fields holding `[T]` stored as JSON in SQLite, queryable via `m <- t.field` bind), binary/unary operations, if/else, do blocks (bind/where/yield/let/groupBy — pure comprehension do blocks are desugared to `__bind`/`__yield`/`__empty` calls that dispatch through Monad/Applicative/Alternative trait impls — works with any monad, not just `[]` (e.g., `Maybe`); monad type resolved at compile time via HKT unification; IO do blocks are excluded from desugaring and use the dedicated `compile_io_do` path; mixed/sequential do blocks use direct loop codegen; set-value do blocks preserved for SQL optimization; do blocks can appear in atom position as function arguments — `f do ...` and `f (do ...)` both work; `groupBy {key}` collects rows, groups by key, and rebinds the variable to each group sub-relation — field access on a group returns the first element's field, aggregates like `count` operate on the group), set expressions, lambdas, closures, function application, case expressions (with exhaustiveness checking for ADTs), constructors (including built-in `True {}`/`False {}` for `Bool` — interchangeable with `true`/`false` literals, usable in `case` patterns), atomic transactions, migrations (schema tracking + `migrate` blocks), schema lockfile (`<name>.schema.lock`), views (`*view = do { ... yield {...} }` with bidirectional read/write, constant column filtering, auto-fill on write), derived relations (`&name = expr` — read-only computed relations, compiled as 0-param functions recomputed on each access; recursive derived relations with self-references use Datalog-style fixpoint iteration via `knot_relation_fixpoint` runtime function, converging when the relation stabilizes), traits and impls (single-dispatch on runtime type tags for primitives and ADTs, default methods, deriving from defaults, supertrait enforcement, associated types with type-level pattern matching), trait bounds (`Display a => [a] -> [Text]` syntax — explicit constraints on function type signatures validated at call sites; trait method calls automatically carry constraints; multiple bounds via `Trait1 a => Trait2 a => Type`; compile-time error when a concrete type lacks a required impl), type inference (Hindley-Milner with row polymorphism for both records and variants, let-generalization, ADT/trait/view-aware, higher-kinded type polymorphism), higher-kinded types (trait params with kind annotations like `(f : Type -> Type)`, type-level application `f a` in method signatures, `[]` and ADT names as bare type constructors in impl args, `TyCon`/`App` internal representation with normalization-based unification), IO monad (`IO {effects} a` type for pure effect descriptions — all relation operations (`*rel`, `&rel`, `set`, `replace`) return `IO {} value` with empty effect set, external builtins like `println`, `readFile`, `now` return IO with specific effects; IO do-blocks sequence actions via bind; effects tracked in the type: `IO {console} {}`, `IO {fs} Text`, `IO {clock} Int`, `IO {} [T]` for DB ops; `knot_io_run` executes IO thunks at the top level in `main`), concurrency (`fork : ∀a r. IO {| r} a -> IO {| r} {}` fire-and-forget OS thread spawning with independent SQLite connections via WAL mode, deep-cloned environments — the spawned IO's effect row propagates through `fork`, so its effects remain visible in the caller's IO type; `race : ∀a b r1 r2. IO {| r1} a -> IO {| r2} b -> IO {| r1 \/ r2} (Result a b)` runs two IO actions concurrently with cooperative aggressive cancellation via per-thread `CancelToken` checked between IO thunks and inside `sleep`, winner is reported via the built-in `Result a b` ADT — `Err {error: a}` if left wins, `Ok {value: b}` if right wins; each arg carries its own effect row and the result row is the union of both (`r1 \/ r2`), so both sides' effects propagate to the caller; `race` cannot appear inside `atomic`; `retry` for STM-style atomic retry — inside `atomic` blocks, causes rollback and waits for relation changes via Condvar with row-level read-filter wakeups so a watcher on `WHERE id = 1` is not woken by writes to `id = 2`, predicates support equality, ordered comparison (`<`/`<=`/`>`/`>=`), and `IN` sets; UPDATE/DELETE paths emit per-row `WriteEvent::Rows` so STM watchers can filter on those too; `atomic : IO {} a -> IO {} a` runs IO body in a transaction with savepoint-based retry loop, body must contain only DB interactions), pattern matching in do-bind (`Circle c <- *shapes` filters relation to matching constructors and destructures; `InProgress ip <- t.status` matches a single value and skips if no match), built-ins (println, putLine (alias for println), print, show, union, count, countWhere, now, filter, match, map, fold, single, any, all, diff, inter, sum, avg, minOn, maxOn, min, max, toUpper, toLower, take, drop, length, trim, contains, elem, reverse, chars, sortBy, head, findFirst, upsertBy ((a -> Bool) -> a -> [a] -> [a] — replace matching rows or append if none match), when, unless, forEach, id, not, stripUnit/withUnit (Int<u> ↔ Int identity for unit conversion), stripFloatUnit/withFloatUnit (Float versions), toJson, parseJson, hash (BLAKE3, polymorphic over any value type — Bytes/Text hash raw contents, structured values hash a canonical serialization so equal logical values produce equal digests), generateKeyPair (X25519, IO {random}), generateSigningKeyPair (Ed25519, IO {random}), encrypt (sealed-box X25519+ChaCha20-Poly1305, IO {random}), decrypt, sign (Ed25519), verify (Ed25519), textToBytes, bytesToText (Maybe Text on UTF-8 error), bytesToHex, bytesFromHex/hexDecode, bytesConcat, bytesGet, bytesSlice, bytesLength, readFile, writeFile, appendFile, fileExists, removeFile, listDir, readLine, randomInt, randomFloat, randomUuid, fork, race, retry, sleep, logInfo/logWarn/logError/logDebug — leveled logging to stderr, colored when TTY / JSON otherwise; logDebug only emits when the program is run with `--debug` — IO-returning builtins produce `IO {effect} a` values; aggregates `count`/`countWhere`/`sum`/`avg`/`minOn`/`maxOn` push down to SQL (`COUNT(*)`/`COUNT(*) WHERE`/`SUM`/`AVG`/`MIN`/`MAX`) when applied to a source relation or its bound alias, including `filter`-then-aggregate, do-block-then-aggregate, and pipe forms (`*rel |> filter ... |> minOn ...`); `minOn`/`maxOn` use `knot_source_query_value` runtime which returns Int/Float/Text matching the SQLite column type and panics on empty relations; binary `min`/`max` (prelude functions, `Ord a => a -> a -> a`) operate on two values; modulo operator `%` dispatches through `Num.mod`, calls `knot_value_mod` at runtime (panics on division by zero), pushes down to SQLite's `%` operator inside SQL-compilable comprehensions; postfix type annotations on any expression (`expr : Type`) parse without surrounding parens — useful for unit ascription on literals; `Uuid` primitive type registered alongside `Bytes` in inference and resolution, stored as TEXT in SQLite, generated via `randomUuid : IO {random} Uuid` (RFC 9562 UUIDv7 — time-ordered, suitable as primary key); `Maybe` ships with built-in `Functor`/`Applicative`/`Monad`/`Alternative` impls in the prelude (parsed from `PRELUDE_SOURCE`, skipped when the user defines their own impl for the same `(trait, type)` pair via `user_impls` tracking in `inject_prelude`)), units of measure (`unit M`, `unit N = Kg * M / S^2` declarations — concrete units are uppercase; `Float<M>`, `Int<Usd>` type annotations; `42.0<M>` literal syntax; compile-time unit algebra — `+`/`-` require unit match, `*`/`/` compose units, negation preserves units; plain numeric types are unit-agnostic; unit polymorphism via lowercase unit variables in type annotations `Float<u> -> Float<u>` — lowercase names in `<...>` that are not declared units become polymorphic unit variables, freshened on each instantiation; units fully erased at runtime; all stdlib functions with numeric types are unit-polymorphic: `avg` as `∀a u. (a -> Float<u>) -> [a] -> Float<u>`, `sum`/`minOn`/`maxOn` fully polymorphic `(a -> b) -> [a] -> b` (units flow through naturally), `countWhere` as `∀a u. (a -> Bool) -> [a] -> Int<u>`, `randomInt` as `∀u. Int<u> -> IO {random} Int<u>` (preserves bound unit), `randomFloat` as `∀u. IO {random} Float<u>`, `now` as `IO {clock} Int<Ms>`, `sleep` as `Int<Ms> -> IO {clock} {}` (built-in `Ms` unit for clock ops), `count` as `∀a u. [a] -> Int<u>`, `length` as `∀u. Text -> Int<u>`, `take`/`drop` as `∀u. Int<u> -> Text -> Text`, `bytesLength`/`bytesSlice`/`bytesGet` also unit-polymorphic; derived unit aliases expand at use site; `(expr : Type)` annotation syntax for explicit unit ascription), refined types (`type Nat = Int where \x -> x >= 0` — base type restricted by predicate function; per-field `{age: Int where \x -> x >= 0}`, cross-field `{...} where \p -> p.lo <= p.hi`, ADT constructor `Circle {radius: Float where \r -> r > 0.0}` refinements; `refine expr` returns `Result RefinementError T` with target refined type inferred from context — `case refine x of Ok {value: n} -> ... | Err {error: e} -> ...`; refined types are nominal in inference (`Ty::Con(name, [])`) with subsumption in unification enabling `Nat ↔ Int` compatibility; `set` validates refined fields via `knot_refinement_validate_relation` before writes — panics on violation; route handlers auto-validate refined body fields after JSON decoding — return HTTP 400 on failure; `RefinementError = {typeName: Text, violations: [{field: Maybe Text, message: Text}]}`; `Result` has built-in monad impls via `knot_result_bind`/`knot_result_yield`/`knot_result_empty` for do-block support), effect inference (per-declaration effect tracking for reads/writes/console/clock/network/fs/random, IO-in-atomic validation, explicit annotation checking), subset constraints (`*orders.customer <= *people.name` for referential integrity, `*users <= *users.email` for uniqueness — validated at runtime before each write commits), routes (`route Name where` with HTTP method/path/body/query/response declarations, path prefix nesting, `route Name = A | B` composition, `headers {field: Type}` for typed request/response headers — request headers appear after query params and before `->`, response headers appear after the response type; header field names use camelCase and auto-convert to HTTP-Header-Case (`authorization` → `Authorization`, `contentType` → `Content-Type`); optional headers use `Maybe` type (`headers {authorization: Maybe Text}` — server gets `Nothing` if absent, `Just {value: "..."}` if present; fetch skips `Nothing` headers); request header fields become constructor fields like body/query/path params; routes desugar to ADTs whose constructors carry only request inputs (no `respond` field) — handlers are bound per-endpoint via `serve API where Ctor = handler` producing a value of type `Server API _` (a row variable when handlers have no concrete effects) or `Server API {effects}` (when handlers carry concrete effects), and each handler returns `Result HttpError T` where `T` is the response type declared in the route and `HttpError = {status: Int, message: Text}`. `Ok {value: T}` responds 200; `Err {error: {status, message}}` responds with the given status (clamped to 100..=599) and a JSON `{"error": message}` body. When response headers are declared, the success body is `{body: T, headers: H}` (still wrapped inside `Ok`); the listen loop extracts body for JSON and headers for HTTP response headers. Error responses do not carry custom headers. `listen : Int<u> -> Server a r -> IO {network | r} {}` starts a `tiny_http` server, dispatching requests to the appropriate handler with JSON request/response serialization; the row variable unifies with the server's effect row so handler effects (e.g. `console`) flow into the IO type of the program calling `listen`. `fetch url (Ctor {fields})` is a type-safe HTTP client reusing route declarations — response type inferred from route's `response:` annotation, returns `IO {network} (Result {status: Int, message: Text} ResponseType)` or `IO {network} (Result ... {body: ResponseType, headers: {h: T}})` when response headers declared. `fetchWith url {headers: [...]} (Ctor {fields})` variant merges ad-hoc headers with route-declared headers, uses `ureq` for HTTP requests. Per-endpoint rate limiting via the `rateLimit <expr>` clause placed after the response type/headers and before `=`: the expression has type `RateLimit input a = {key: input -> RequestCtx -> Maybe a, limit: {requests: Int, window: Int<Ms>}}` with `Ord a` enforced via a deferred constraint; `input` is the same record the handler receives (built from path params + query params + body fields + request headers — `route_input_record_ty` factored out of `serve_handler_type` for shared use); absence of the clause means unlimited; `key` returning `Nothing` exempts the request, `Just v` keys the bucket on `show v`. Token-bucket algorithm refilled lazily, persisted in `_knot_rate_limits (route TEXT, key TEXT, tokens REAL, last_refill INTEGER, PRIMARY KEY(route, key)) WITHOUT ROWID`, created on first use; check runs in `BEGIN IMMEDIATE` so concurrent same-key requests serialize. Codegen: parser introduces an `Option<Expr>` field on `RouteEntry`; type checker validates the expression in `check_rate_limit_expr` (called from `infer_declarations` Route arm); `can_start_type_atom` stops at `rateLimit` so the response type doesn't eat the keyword; runtime registers configs via `knot_route_set_rate_limit(table, ctor, rate_limit_value)` which unpacks the `{key, limit}` record; both the main_init route table loop and the `listen`/`listenOn` codegen path register them on their respective tables; check happens in the worker thread inside `catch_unwind`, after the input record is built but before refinement validation, so the user's `key_fn` sees the same destructured input the handler will. The worker's Err type is `(u16, String, Option<i64>)` where the third element is `retry_after_ms` — the response handler attaches `Retry-After: <seconds>` when present and uses `Content-Type: application/json` body `{"error":"..."}`; rate-limit rejections return `Err((429, "Rate limit exceeded", Some(retry_after_ms)))`).
116124
117125## Version Control
118126