44fe4ef · knot-legacy · git.iko.soy

git.iko.soy/knot-legacy

Remove effect-row prose from all docs (no effect tracking in impl); correct atomic/serve/fork/race claims

commit44fe4efdf5c33aedd3f9cc53d5828c880507a6f0 authoriko <mail@iko.soy> dateThu 30 Jul 2026, 16:16 (2 months ago) parent4eef0b5

4 files changed+41−51

compare with master

unifiedsplit

DESIGN.md+20−23 README.md+3−4 base.md+7−9 stdlib.md+11−15

DESIGN.md+20−23

@@ -526,12 +526,17 @@ Grouping is executed via SQLite — key columns are inserted into a temp table a

526526

527527## Effects and IO

528528

529−### Unified Effect Model

529+### Unified IO Model

530530

531−All state operations in Knot return IO values. The IO type carries an effect set that distinguishes DB operations from external effects:

531+All state operations in Knot return IO values. `IO a` is a single type

532+constructor taking one argument — the result type — with no effect-row

533+parameter:

532534

533−- **DB operations** return `IO {} value` — the empty effect set `{}` indicates pure database interaction with no external side effects. Source refs (`*rel`), derived refs (`&rel`), and relation writes (`*rel = expr`, `replace *rel = expr`) all return `IO {} value`.

534−- **External effects** carry specific tags: `IO {}`, `IO Text`, `IO Result`, `IO Int Ms`, `IO Float 1`.

535+- **DB operations** return `IO value`. Source refs (`*rel`), derived refs

536+ (`&rel`), and relation writes (`*rel = expr`, `replace *rel = expr`) all

537+ return `IO value`.

538+- **External effects** are also plain `IO`: `IO {}`, `IO Text`, `IO Result`,

539+ `IO (Int Ms)`, `IO Float 1`.

535540

536541This unified model means all stateful code lives in IO do-blocks, while pure comprehensions over plain values remain non-IO.

537542

@@ -540,18 +545,15 @@ This unified model means all stateful code lives in IO do-blocks, while pure com

540545Effectful functions return descriptions of effects (`IO a`) rather than performing them. IO values are thunks that execute when run.

541546

542547```knot

543−-- DB operations return IO with empty effects

548+-- DB operations return IO

544549*people : [Person]

545−-- *people : IO {} [Person]

550+-- a read of *people yields IO [Person]

546551

547−-- println returns an IO action with console effect

548552println : a -> IO {}

549553

550−-- readFile returns an IO action with fs effect

551554readFile : Text -> IO Text

552555

553−-- now returns an IO action with clock effect, tagged with the built-in Ms unit

554−now : IO Int Ms

556+now : IO (Int Ms)

555557```

556558

557559### IO Do-Blocks

@@ -622,11 +624,8 @@ If the body uses a capability not listed in the signature, the compiler rejects

622624

623625### IO and Transactions

624626

625−`atomic` takes an IO body and runs it in a transaction. The body must only contain DB interactions (empty effect set) — no external IO (console, fs, etc.) is allowed inside `atomic`.

626−

627−```knot

628−atomic : IO {} a -> IO {} a

629−```

627+`atomic` takes an IO body and runs it in a transaction. `atomic do ...` is a

628+keyword form (not a `base.` function); the block is an `IO a`.

630629

631630```knot

632631-- DB writes go in `atomic`, IO happens after commit

@@ -727,7 +726,7 @@ loadConfig \path -> do

727726fork : IO a -> IO {}

728727```

729728

730−The spawned action's effect row `r` propagates through `fork` to the caller — a program that forks an IO that calls `println` is visibly typed with `{console}` in its IO row, so the effect system still reflects what the program can do. Do blocks can be passed as arguments without parentheses: `fork do ...`.

729+`fork` spawns an IO action on a new OS thread and returns `IO {}`. Do blocks can be passed as arguments without parentheses: `fork do ...`.

731730

732731```knot

733732*counter : [{n: Int 1}]

@@ -780,10 +779,8 @@ SQLite WAL mode ensures that concurrent readers and writers do not block each ot

780779

781780#### `race`

782781

783−`race` runs two IO actions concurrently and returns as soon as one wins. Each

784−argument carries its own effect row; the result IO's row is the union of both,

785−written `r1 \/ r2`. Any effects required by either side propagate into the

786−result IO. The winner is reported via the built-in `Result a b` ADT —

782+`race` runs two IO actions concurrently and returns as soon as one wins. The

783+winner is reported via the built-in `Result a b` ADT —

787784`Err {error: a}` when the left action wins, `Ok {value: b}` when the right

788785action wins.

789786

@@ -859,7 +856,7 @@ api (serve Api where)

859856main (listen 8080 api)

860857```

861858

862−`serve API where` produces a value of type `Server API _` (a polymorphic row variable when handlers have no concrete effects) or `Server API {effects}` when handlers carry concrete effects — e.g. `Server API {console}` if a handler calls `println`. Each handler receives the request record (path/query/body/header fields) and returns `Result HttpError T`, where `T` is the response type declared on the endpoint and `HttpError = {status: Int 1, message: Text}`. Handler effects propagate through `listen` into the program's IO type. No string routes, no untyped params, no missing handlers.

859+`serve API where` produces a value of type `Server API`. Each handler receives the request record (path/query/body/header fields) and returns `Result HttpError T`, where `T` is the response type declared on the endpoint and `HttpError = {status: Int 1, message: Text}`. `listen : Int u -> Server a -> IO {}` binds the server to a port. No string routes, no untyped params, no missing handlers.

863860

864861#### HTTP Status Codes

865862

@@ -1008,7 +1005,7 @@ CREATE TABLE _knot_rate_limits (

10081005

10091006The check runs in a `BEGIN IMMEDIATE` transaction so concurrent requests for the same client serialize correctly; different keys do not contend.

10101007

1011−**Effects.** Rate limiting reads and writes a hidden table; these effects are internal and not surfaced in user-visible effect rows.

1008+**Effects.** Rate limiting reads and writes a hidden internal table.

10121009

10131010#### Path Prefixes

10141011

@@ -1853,7 +1850,7 @@ type-directedly and would silently match the wrong conversion. See

18531850

18541851### Type Inference

18551852

1856−Full Hindley-Milner style inference extended with row polymorphism (record fields, effect rows, and unit variables) and implicit-dictionary constraints. Type signatures are always optional — the compiler infers everything from usage.

1853+Full Hindley-Milner style inference extended with row polymorphism (record fields and unit variables) and implicit-dictionary constraints. Type signatures are always optional — the compiler infers everything from usage.

18571854

18581855## Full Example

18591856

README.md+3−4

@@ -625,10 +625,9 @@ without a separate instance mechanism. See `examples/ord.knot`,

625625variants, let-generalization, implicit-dictionary constraints, and unit

626626polymorphism.

627627

628−**IO effects.** Every function carries an effect row in its type:

629−`IO Text`, `IO {}`, etc. Atomic blocks are

630−typed `IO {} a -> IO {} a` so the compiler rejects `println` inside a

631−transaction. See `examples/log_test.knot`.

628+**IO.** Effectful functions return `IO a` — a description of an effectful

629+computation producing an `a`. `atomic do ...` runs a block in a transaction.

630+See `examples/log_test.knot`.

632631

633632**Concurrency.** `fork`, `race`, and STM-style `atomic` blocks with

634633`retry`. Row-level read-filter wakeups mean a watcher on `WHERE id = 1`

base.md+7−9

@@ -16,10 +16,9 @@ This file is the complete reference for every field of `base`, grouped by

1616purpose, with the full path, type, and a description. Types are written in

1717Knot's own notation:

1818

19−- `a`, `b`, `r`, `u`, … are type / effect / unit variables (universally

20− quantified).

19+- `a`, `b`, `u`, … are type / unit variables (universally quantified).

2120- `[a]` is a relation (a set) of `a`.

22−- `IO a` is an IO action carrying an effect row.

21+- `IO a` is an IO action producing an `a`.

2322- `Maybe a` is `Nothing {}` or `Just {value: a}`; `Result e a` is

2423 `Err {error: e}` or `Ok {value: a}`.

2524

@@ -352,11 +351,10 @@ base.when (n > 0) (base.println "positive")

352351### `base.forEach`

353352

354353```

355−base.forEach : [a] -> (a -> IO r {}) -> IO r {}

354+base.forEach : [a] -> (a -> IO {}) -> IO {}

356355```

357356

358−Sequence an IO action over each row (in iteration order). The effect row `r`

359−propagates.

357+Sequence an IO action over each row (in iteration order).

360358

361359### `base.not`

362360

@@ -778,12 +776,12 @@ Verify a signature. Args: public key, message, signature.

778776### `base.fork`

779777

780778```

781−base.fork : IO r a -> IO r {}

779+base.fork : IO a -> IO {}

782780```

783781

784782Run an IO action on a new OS thread (fire-and-forget; the result is

785−discarded). The effect row propagates. Each thread gets its own SQLite

786−connection (WAL). The main thread joins all spawned threads before exit.

783+discarded). Each thread gets its own SQLite connection (WAL). The main thread

784+joins all spawned threads before exit.

787785

788786### `base.race`

789787

stdlib.md+11−15

@@ -369,11 +369,9 @@ fork : IO a -> IO {}

369369```

370370

371371Run an IO action on a new OS thread (fire-and-forget). The spawned action can

372−return any value `a` (it is discarded) and may have any effect row `r`. That

373−effect row propagates through `fork` to the caller, so a program that forks an

374−IO performing `println` is visibly typed with `{console}` in its IO row. Each

375−thread gets its own SQLite connection via WAL mode for safe concurrent access.

376−The main thread waits for all spawned threads before exiting.

372+return any value `a` (it is discarded). Each thread gets its own SQLite

373+connection via WAL mode for safe concurrent access. The main thread waits for

374+all spawned threads before exiting.

377375

378376```knot

379377main do

@@ -392,9 +390,7 @@ Do blocks can be passed directly as arguments without parentheses.

392390race : IO a -> IO b -> IO (Result a b)

393391```

394392

395−Run two IO actions concurrently and return the winner. Each argument carries

396−its own effect row; the result IO's row is the union of both (written

397−`r1 \/ r2`). Effects required by either side flow into the result IO.

393+Run two IO actions concurrently and return the winner.

398394

399395The winner is reported via the built-in `Result a b` ADT — `Err {error: a}` when the left action wins, `Ok {value: b}` when the right action wins.

400396

@@ -619,11 +615,11 @@ Read a line of input from stdin.

619615### `when` / `unless`

620616

621617```

622−when : Bool -> IO r {} -> IO r {}

623−unless : Bool -> IO r {} -> IO r {}

618+when : Bool -> IO {} -> IO {}

619+unless : Bool -> IO {} -> IO {}

624620```

625621

626−Run an IO action conditionally. `when cond a` runs `a` if `cond` is `True {}`; `unless cond a` runs `a` if `cond` is `False {}`. The skipped branch becomes `yield {}`. The action's effect row `r` propagates to the result.

622+Run an IO action conditionally. `when cond a` runs `a` if `cond` is `True {}`; `unless cond a` runs `a` if `cond` is `False {}`. The skipped branch becomes `yield {}`.

627623

628624```knot

629625when (n > 0) (println "positive")

@@ -635,7 +631,7 @@ unless verbose do

635631### `forEach`

636632

637633```

638−forEach : [a] -> (a -> IO r {}) -> IO r {}

634+forEach : [a] -> (a -> IO {}) -> IO {}

639635```

640636

641637Sequence an IO action over each row of a relation. Iteration follows the relation's deterministic order (after any `sortBy`).

@@ -946,11 +942,11 @@ The HTTP types and primitives are defined in the language spec (`DESIGN.md`). Th

946942### `listen` / `listenOn`

947943

948944```

949−listen : Int u -> Server a r -> IO {}

950−listenOn : Text -> Int u -> Server a r -> IO {}

945+listen : Int u -> Server a -> IO {}

946+listenOn : Text -> Int u -> Server a -> IO {}

951947```

952948

953−Start an HTTP server built with `serve API where ...`. `listen` binds to all interfaces; `listenOn` takes an explicit bind address. The `r` row variable unifies with the server's effect row, so handler effects (e.g. `console` from a handler that calls `println`) flow into the program's IO type.

949+Start an HTTP server built with `serve API where ...`. `listen` binds to all interfaces; `listenOn` takes an explicit bind address.

954950

955951### `fetch` / `fetchWith`

956952