diff --git a/AGENTS.md b/AGENTS.md index afd9a1f..27a4c2d 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -22,10 +22,10 @@ Logo dialect. Anything not on this list is aspirational. Do not assume LANGUAGE.md examples run. -- **Lexer** (`crates/iklo-lexer`) — logos-based; produces `Lexeme` values (kebab-case identifiers, numbers, `:name` lexical refs, `+ - * /` operators, parens, `let`, `be`, `set`, newline, `;`). +- **Lexer** (`crates/iklo-lexer`) — logos-based; produces `Lexeme` values (kebab-case identifiers, numbers, `:name` lexical refs, `+ - * /` operators, parens, `let`, `be`, newline, `;`). No `set` token exists yet — see Parser/AST below. - **AST** (`crates/iklo-ast`) — `Program = Vec>`; expressions include `Number`, `LexRef`, `Let`, `Binary`. - **Parser** (`crates/iklo-parser`) — Pratt precedence; whitespace-sensitive infix ops (so `x-1` stays one identifier); newline is a soft terminator (terminates only when the current expression is complete and can't be continued); `;` is a hard terminator; newlines are swallowed inside parens. Supports `let :name be ` as an expression. -- **Runtime** (`crates/iklo-runtime`) — tree-walking interpreter with a transactional live image: `RuntimeImage` is a thin façade over `InMemorySubstrate` (from `iklo-substrate`); `let` and `set` update the image transactionally per top-level expression. +- **Runtime** (`crates/iklo-runtime`) — tree-walking interpreter with a transactional live image: `RuntimeImage` is a thin façade over `InMemorySubstrate` (from `iklo-substrate`); `let` updates the image transactionally per top-level expression. `set` is not implemented (no parser/AST support — see above), so it does not update anything today. - **Substrate** (`crates/iklo-substrate`) — capability boundary trait (`Substrate` + `Transaction`) that hides where the live image lives. Ships with an in-memory implementation (`InMemorySubstrate`), the default. - **Substrate (Turso-backed)** (`crates/iklo-substrate-turso`) — `TursoSubstrate` implementation of `Substrate`, opt-in behind the `turso` Cargo feature (epic [004-turso-substrate-backend](specs/004-turso-substrate-backend/spec.md)); passes the same contract suite as `InMemorySubstrate`. **Local-file-only**: no remote/cloud Turso connectivity (blocker `B001` in that epic's `tasks.md` — a deliberate scoping decision, not a limitation to work around). - **CLI** (`crates/iklo-cli`) — file runner and multi-line REPL. Continuation prompt is `iklo. `; blank line cancels a multi-line input. REPL commands are `/`-prefixed (`/quit`, `/revision`, `/env`), recognized only at a fresh prompt, with tab-completion (per ADR-0004). Also selects the substrate backend — see "Substrate mode selection" below. @@ -35,8 +35,8 @@ Anything not on this list is aspirational. Do not assume LANGUAGE.md examples ru These are decided and shouldn't be casually revisited. If a change is needed, open an ADR. - **Identifiers are kebab-case**, including subtraction-lookalikes: `x-1` is one identifier, `x - 1` is subtraction. Infix `+ - * /` **require whitespace on both sides**. -- **Binding introduction is `let :name be `** (not `=`). `:name` is the lexical-value sigil. `let` is an expression that returns the bound value. -- **`set` mutates an existing binding**; `let` introduces a new one (even if it shadows a previous name). `set` should only reach the mutable engines (graph / dynamic / reactive / synchronized); `set` on a plain lexical binding is an error. +- **`let :name be `** (not `=`) introduces a **lexical** binding — the only engine `let` can target. `:name` is the lexical-value sigil. `let` is an expression that returns the bound value, and is always pure (given a pure ``): lexical bindings are private to the evaluation's own scope and can never be mutated. +- **`set` is the sole write path for the mutable engines** (graph / dynamic / reactive / synchronized): it creates the binding if absent or mutates it if present (upsert), always effectful either way. `set` on a lexical binding is an error; `let` on a mutable engine is a syntax error — the two verbs partition the engines completely, with no overlap (ADR-0007). - **Newline is a soft terminator**: it ends the current expression only when that expression is already complete *and* the next line can't continue it. Newlines are ignored inside `( … )`. - **`;` is a hard terminator** and forces the current expression to end (parse error if incomplete). - **REPL commands use a leading `/`** (`/quit`, `/revision`, `/env`) recognized only at a fresh prompt; tab-completion is backed by a shared gate function (per ADR-0004). `/` mid-line is division, not a command. diff --git a/LANGUAGE.md b/LANGUAGE.md index e8b943c..7b6ff6b 100644 --- a/LANGUAGE.md +++ b/LANGUAGE.md @@ -210,12 +210,15 @@ let (^bool :y) be -false # # Note: **Everything is a value** -# So there's no separate token for type assignment (type declaration + definition). -# Meaning `let` can *always* be used to bind an expression to a token. -# Regardless if is a regular value, a function, a type, or something else entirely... +# So there's no separate token for type assignment (type declaration + definition) -- +# but a bare `^token` (no `:name`) IS a graph binding (the `gra%token`/`^token` +# sugar), so per ADR-0007 it goes through `set`, not `let`: type/interface/ +# computation definitions are new graph bindings, and `set` upserts them. +# A "typed val assignment" (`^Type :name be `, below) stays lexical -- +# there `^Type` is a type *annotation* on a `let`, not a graph binding. # simple enum types - similar to sets -let ^bool be %d{ -true, -false } +set ^bool to %d{ -true, -false } # equivalent values, with different type-checking behavior: let :x be -true # a "free" -true should always be parsed as boolean? @@ -223,14 +226,14 @@ let ^bool :x be -true let :x be ^bool -true # record-like enum types - similar to maps -let ^maybe be d%{ -left = :value, -right = :value } +set ^maybe to d%{ -left = :value, -right = :value } # default construction happens by applying bound type as a function: let :val be (^maybe "value1") let (^maybe :val) be ^maybe "value2" # simple record types use slots, not options -let ^my-record be d%{ :field1 = :value, :field2 = :value, :field3 = d% { -true, -false, -unknown = :unknown-value } } +set ^my-record to d%{ :field1 = :value, :field2 = :value, :field3 = d% { -true, -false, -unknown = :unknown-value } } # describe returns generated constructor + field metadata let (^my-record :my-record) be ^my-record "my-value" "my-unknown-value" @@ -239,7 +242,8 @@ let :my-record be ^my-record :value = "my-value", :unknown-value = "my-unknown-v # named arguments are valid for any form that declares named slots in its interface # graph transaction semantics: -# 1) top-level `let` on graph bindings runs in an implicit transaction +# 1) top-level `set` on graph bindings (create or update — set is an +# upsert, ADR-0007) runs in an implicit transaction # 2) nested graph updates require explicit `graph.begin` ... `graph.commit` # 3) on uncaught error, graph transaction always rolls back # 4) macros can emit graph transactions, but cannot commit a transaction they did not open @@ -408,7 +412,7 @@ form [:a :b, :n] # (form [[:a :b], :n]) | `if%token` | | graph | **Interface binding**: describes the *signature* or *interface* for the *form* and *computation* bindings. | | `cp%token` | | graph | **Computation binding**: describes the *compute*/*body* for *form* and *interface* bindings. | | `key%token` | `~token` | static | **Keyword** or **Option binding**: *self-bound*, *global*, and *static*. **Cannot be rebound**. | -| `val%token` | `:token` | lexical | **Lexical binding**: *Usually immutable* in iklo. Used for *locals*, *function arguments*, etc. | +| `val%token` | `:token` | lexical | **Lexical binding**: *Immutable once bound* (ADR-0007) in iklo. Used for *locals*, *function arguments*, etc. | | `var%token` | `$token` | dynamic | **Variable binding**: *thread-local* identities with a *shared default*. Like clojure **vars**. | | `rx%token` | | reactive | **Reactive binding**: *event-sourced*, *reactive* binding. Like Clojure **agents**. | | `sync%token` | | synchronised | **Entity binding**: *synchronous* and *uncoordinated*. Like Clojure **atoms**. | @@ -424,15 +428,17 @@ form [:a :b, :n] # (form [[:a :b], :n]) - **Synchronous** or **Asynchronous**. - **Coordinated** or **Uncoordinated**. - `graph`, `dynamic`, `reactive` and `synchronized` are always mutable, by definition. -- `lexical` values are *usually* constant, but can be declared mutable with `set`. +- `lexical` values are immutable once bound — `let` alone introduces them; `set` never targets the lexical engine (ADR-0007). ## Assignment ```iklo -# assign an expression to some binding -let be +# introduce a lexical binding (the only engine `let` can target, ADR-0007) +let be +# write a mutable-engine binding -- create or update, always effectful +set to ``` @@ -581,11 +587,18 @@ This is how tokens "interpret themselves" without ambiguous free-form parsing. print $a $b # prints "500 6" - let $a be 500 [ + set $a to 500 + [ print $a $b ] - - # prints "5 6" + + # TBI/BET: this block illustrated scoped shadow-then-restore for a + # dynamic binding (originally written `let $a be 500 [...]`). Per + # ADR-0007, `set` is a flat, permanent upsert with no restore-on-exit + # of its own -- whether/how a scoped dynamic rebind exists at all + # (and what its keyword would be, if not `set`) is unresolved; do not + # assume the "prints 5 6" comment below still holds under plain `set`. + # prints "5 6" -- UNVERIFIED under the current let/set model, see above print $a $b ### Lexical @@ -601,8 +614,10 @@ This is how tokens "interpret themselves" without ambiguous free-form parsing. ```Iklo to some-proc :a :b do # Note `some-lambda` has no prefix - this is the "form" binding - # Same as `let some-lambda [fn :x :y [return :x + :y]]`: - let some-lambda do + # (fm%token, graph engine per the Bindings table) -- per ADR-0007, + # a new graph binding is introduced via `set`, not `let`. + # Same as `set some-lambda to [fn :x :y [return :x + :y]]`: + set some-lambda do fn :x :y do return :x + :y end diff --git a/specs/006-strictness-effects-spike/design-note.md b/specs/006-strictness-effects-spike/design-note.md index 7fdedb4..c3bd1a7 100644 --- a/specs/006-strictness-effects-spike/design-note.md +++ b/specs/006-strictness-effects-spike/design-note.md @@ -24,8 +24,7 @@ | Construct | Strictness | Purity | Effect | Notes | |-----------|-----------|--------|--------|-------| -| Lexical `let :x be ` | strict | pure (binding) | none | Evaluates ``, binds result in the lexical engine. Transactional commit on success. A `let` targeting a mutable engine (e.g. graph `let ^bool :x be …`, §6) commits engine state and is effectful — the pure row is the lexical form only. | -| `set :x to ` | strict | effectful (mutation) | mutates existing binding | Requires mutable binding engine (`graph`, `dynamic`, `reactive`, `sync`). | +| `let :x be ` | strict | pure (binding) | none | Evaluates ``, binds result. Per [ADR-0007](../decisions/ADR-0007-set-effect-classification.md), `let` targets the lexical engine only — no engine-level commit to account for, so it is unconditionally pure (given a pure ``), with no other engine to hedge on. | | `+ - * /` (arithmetic) | strict | pure | none | All operands evaluated before computation. | | `:x` (lexical read) | strict | pure | none | Returns bound value. | | Newline | strict | pure | none | Soft expression terminator; no side effects. | @@ -35,6 +34,7 @@ | Construct | Strictness | Purity | Effect | Notes | |-----------|-----------|--------|--------|-------| +| `set $x to ` | strict | effectful (mutation) | creates or mutates a mutable-engine binding (upsert) | Not implemented — the parser (`crates/iklo-parser/grammar.lalrpop`) has no `set` production and `iklo-ast::Expr` has no `Set` variant today. The sole write path for mutable binding engines (`graph`, `dynamic`, `reactive`, `synchronized`) once implemented — per [ADR-0007](../decisions/ADR-0007-set-effect-classification.md); never targets `:x` (lexical). | | `fn` / `to` (function def) | — | pure (definition) | none | Closure captures lexical env. Body is lazy-evaluated on call. | | `cond` | strict branches | pure (control flow) | none | Each branch is strict; only taken branch is evaluated. | | `repeat` | strict body | pure (control flow) | none | Body evaluated N times. | @@ -171,7 +171,7 @@ Runtime metadata (annotations) should **not** be the primary way to declare puri The recommended approach: 1. **Surface keywords** (`lazy`, `strict`, `run`, `do`) control the most common cases. -2. **Type inference** determines purity from the inferred body alone: no observable mutation (e.g. `set` or a graph `let`) and no boundary-crossing during evaluation (no inline `run`/`do`/`then`/boundary `;`). The produced value's type is not itself a purity condition — building an `^action ^t` and returning it is pure; only running it later is effectful (see [ADR-0006](../decisions/ADR-0006-effect-model.md), which is authoritative on this rule). +2. **Type inference** determines purity from the inferred body alone: no observable mutation (i.e. no `set` — per [ADR-0007](../decisions/ADR-0007-set-effect-classification.md), `let` can only target the lexical engine, so it never needs naming here) and no boundary-crossing during evaluation (no inline `run`/`do`/`then`/boundary `;`). The produced value's type is not itself a purity condition — building an `^action ^t` and returning it is pure; only running it later is effectful (see [ADR-0006](../decisions/ADR-0006-effect-model.md), which is authoritative on this rule). 3. **Runtime enforcement** ensures effects only run in effect boundaries. 4. **Annotations** provide optional hints for tooling and diagnostics. @@ -182,7 +182,7 @@ This avoids the "annotation pollution" problem while keeping effects visible and | Example | Strictness | Purity | Effect | Correct? | |---------|-----------|--------|--------|----------| | `let :x be 1 + 2` | strict | pure | none | Yes — arithmetic is pure and strict. | -| `set :x to 5` | strict | effectful (mutation) | binding mutation | Yes — rebinds an existing `:x` in a mutable engine; effectful despite returning no `^action` (see §5 point 2). | +| `set $x to 5` | strict | effectful (mutation) | binding mutation | Yes — upserts `$x` in the dynamic engine (per [ADR-0007](../decisions/ADR-0007-set-effect-classification.md), `set` never targets lexical `:x`); effectful despite returning no `^action` (see §5 point 2). | | `let :x be lazy 1 + 2` | lazy | pure | none | Yes — thunk created, not evaluated. | | `strict :x` | strict (force) | pure | none | Yes — forces thunk, may error on cycle. | | `let :copy be cp "a" "b"` | strict | pure (builds action) | none (action not run) | Yes — action value created, not executed. | @@ -192,7 +192,7 @@ This avoids the "annotation pollution" problem while keeping effects visible and | `cond (-true) 1 else 2` | strict (branch) | pure | none | Yes — only taken branch evaluated. | | `repeat 4 [forward :side]` | strict (body) | pure | none | Yes — body evaluated 4 times, pure. | | `to adder :n do fn do :n + 1 end end` | — | pure (definition) | none | Yes — defines closure, no side effects. | -| Graph `let ^bool :x be -true` | strict | effectful (mutation) | graph commit | Yes — modifies graph binding engine. | +| Graph `set ^bool to -true` | strict | effectful (mutation) | graph commit | Yes — `set` upserts the graph binding engine; per [ADR-0007](../decisions/ADR-0007-set-effect-classification.md), `let` can no longer target `graph` at all. | | `(vim start)` (shell) | strict | pure (builds action) | process IO only when the action reaches an effect boundary | Yes — builds an `^action ^t`, runs at the same boundaries as any action (top-level runner, `do`, …), per [ADR-0008](../decisions/ADR-0008-shell-executable-calls.md). | | `` `[ a ~:b _:c d ] `` (syntax-quote) | — | pure (compile-time) | none | Yes — macro template, no runtime effect. | | `map %{ a->1, b->2 }` | strict | pure | none | Yes — literal constructor, pure per contract. | diff --git a/specs/decisions/ADR-0006-effect-model.md b/specs/decisions/ADR-0006-effect-model.md index 466d234..8bf9d7a 100644 --- a/specs/decisions/ADR-0006-effect-model.md +++ b/specs/decisions/ADR-0006-effect-model.md @@ -64,12 +64,14 @@ their own ADRs (see Follow-ups). They are **not** decided here. - **Purity is inferred, never declared, and is about evaluation, not the produced value's type.** A form is pure iff *evaluating it* performs no - observable mutation (no `set`, no `let` into a mutable binding engine — - pending ADR-0007's exact line on `set`) and does not itself cross an - effect boundary (no inline `run`/`do`/boundary `;`/`then` fires during its - own evaluation). Whether the *value* a pure form returns happens to be - `^action ^t`-typed is irrelevant — that only means running it *later* is - effectful, not that constructing it now was. `let :copy be cp "a" "b"` + observable mutation (no `set` — per ADR-0007, `set` is the sole write + path for the mutable engines, and `let` can only ever target the lexical + engine, so `let` never needs to be named in this exclusion) and does not + itself cross an effect boundary (no inline `run`/`do`/boundary `;`/`then` + fires during its own evaluation). Whether the *value* a pure form + returns happens to be `^action ^t`-typed is irrelevant — that only + means running it *later* is effectful, not that constructing it now + was. `let :copy be cp "a" "b"` above is pure by this rule: it builds an `^action ^int` but never runs one. A form that mutates a binding is impure regardless of what it returns — that is the failure mode a return-type-only rule would miss @@ -107,9 +109,11 @@ their own ADRs (see Follow-ups). They are **not** decided here. question: forcing a thunk is not on the effect-boundary list in §4 below, and `LANGUAGE.md` requires that forcing "must not execute hidden effects" — so a thunk body that would mutate a binding or cross a boundary (`set`, - a mutable-engine `let`, `run`, `do`, `then`) is **rejected**, not silently - deferred. `lazy (set :x to 5)` is ill-typed, exactly like calling `set` - directly in any other position where a pure expression is required — + `run`, `do`, `then`) is **rejected**, not silently deferred. `lazy (set $x + to 5)` is ill-typed, exactly like calling `set` directly in any other + position where a pure expression is required — note `:x` (the lexical + sigil) could never appear here at all: per ADR-0007, `set` never targets + the lexical engine, so `$x` (dynamic) stands in as the example instead — laziness does not launder an effect into a runtime action. Laziness is a control feature for pure compute, never an effect scheduler (`LANGUAGE.md` §"Design constraints"). Forcing a *value's* effect-typed @@ -148,8 +152,11 @@ semantics": `run` is the primitive executor; `do` and `then` are effect boundaries in their own right that build on it. Nothing else — ordinary expression -evaluation, thunk forcing, macro expansion, `let`/`set` into a lexical -binding — is an effect boundary. +evaluation, thunk forcing, macro expansion, a lexical `let`, or `set` — is +an effect boundary. `set` (per ADR-0007) is effectful, but it mutates +*immediately during ordinary evaluation*, gated by the transaction +contract, not by crossing one of the boundaries above — it is always +effectful without ever needing one. ## Non-decisions diff --git a/specs/decisions/ADR-0007-set-effect-classification.md b/specs/decisions/ADR-0007-set-effect-classification.md index 257cbe1..3680a3d 100644 --- a/specs/decisions/ADR-0007-set-effect-classification.md +++ b/specs/decisions/ADR-0007-set-effect-classification.md @@ -1,4 +1,4 @@ -# ADR-0007 — `set` is an effect; `let` is pure only for the lexical engine +# ADR-0007 — `let` is lexical-only (always pure); `set` is the sole mutable-engine write path (always an effect) - **Status:** Proposed — drafted from the epic 006 design note's open question §4.4. Accepting this ADR means editing this line to `Accepted` @@ -12,12 +12,14 @@ ## Decision (one sentence) -**`set` (mutating an existing binding in a mutable engine) is classified as -an effect, unconditionally and independent of whether the enclosing -transaction ever commits; `let :x be ` (introducing a new binding) is -pure only when it targets the lexical engine *and* `` is itself pure — -matching ADR-0006's engine-scoped `let` rule, restated here for -completeness.** +**`let` is restricted to the lexical engine only — it can no longer target +`graph` / `dynamic` / `reactive` / `synchronized` — which makes lexical +`let :x be ` unconditionally pure whenever `` is pure, with no +engine-dependent exception left; `set` becomes the sole write path for +every mutable engine, creating the binding if absent or mutating it if +present (upsert either way), and is classified as an effect +unconditionally, independent of whether the enclosing transaction ever +commits.** ## Context @@ -33,17 +35,25 @@ kinds), which implements the mutable engines `set` targets. This is a narrow decision, deliberately split out of ADR-0006: ADR-0006 already decided *how* purity works in general (evaluation-based: no -observable mutation, no boundary-crossing) and, as a corollary, that a -`let` targeting a mutable engine is effectful because it commits engine -state — the pure classification is scoped to the lexical engine. What -ADR-0006 left open is `set` specifically, and the transaction-rollback -question the design note raised about it. - -`AGENTS.md` already states the mechanical rule in prose: "`set` mutates an +observable mutation, no boundary-crossing). Its own draft carried a +corollary — a `let` targeting a mutable engine is effectful because it +commits engine state — as a hedge on top of that general rule. Working +through *why* that corollary held surfaced a cleaner option: instead of +`let`'s purity depending on which engine it targets, restrict `let` to the +one engine where introduction never touches shared, mutable state at all. +That is what this ADR decides — not merely restating ADR-0006's corollary, +but replacing it with a syntactic restriction that removes the +engine-dependent hedge entirely. + +Previously, `AGENTS.md`'s non-negotiable rule read: "`set` mutates an existing binding; `let` introduces a new one … `set` should only reach the mutable engines (graph / dynamic / reactive / synchronized); `set` on a -plain lexical binding is an error." This ADR settles the *type-system* -classification, not the mechanics, which were never in question. +plain lexical binding is an error." That rule described introduce-vs-mutate +as the split, with either verb able to reach any engine except that `set` +was barred from lexical. This ADR changes the split itself to +engine-vs-engine — `let` ↔ lexical, `set` ↔ every mutable engine — and, +per `AGENTS.md`'s own instruction that such a non-negotiable rule requires +an ADR to revisit, this is that ADR. §4 below states the amended rule. ## What this commits us to @@ -59,9 +69,15 @@ classification, not the mechanics, which were never in question. - This is unconditional on **which** mutable engine is targeted (`graph` / `dynamic` / `reactive` / `synchronized` — `LANGUAGE.md`'s Transaction contract section abbreviates the last as `sync`; epic 008 - settles the canonical name) and on **whether `` itself is pure** — + settles the canonical name), on **whether `` itself is pure** — evaluating `` may be pure, but the `set` that consumes its result is - not. + not — and on **whether the target binding already exists**. `set` is an + **upsert**: it creates the binding in that engine if absent, or mutates + it if present, and both cases are effectful identically. This is a + deliberate change from `set`'s prior "must already exist" mechanics + (§4 below) — `set` is now the *only* way to write a mutable-engine + binding at all, so it has to cover first introduction too, not just + updates to something `let` already created there. - **`set` is exempt from the `^action ^t` pattern, deliberately.** ADR-0006 models IO effects (`echo`, `cp`, file/network forms) as building an `^action ^t` value that is pure to construct and effectful only when @@ -98,24 +114,68 @@ classification, not the mechanics, which were never in question. depend on other bindings' state, not on `set`'s own arguments, so no static rule could ever correctly grant "purity on rollback." -### 3. `let` is pure only for the lexical engine (restated, not re-decided) - -- Consistent with ADR-0006 §"Effects are a marker type" (its `let` note): - lexical `let :x be ` is pure **when `` is itself pure** — the - lexical engine removes the one extra effect a `let` could otherwise add - (the engine-level commit), it does not exempt whatever `` does. - `let :x be run :copy` is impure: `run` crosses an effect boundary during - evaluation regardless of which engine `:x` lands in. A `let` that - introduces a binding into a mutable engine (e.g. graph - `let ^bool :x be …`) is effectful on top of that, because introducing a - binding there requires the same engine-level commit a mutation does. - Restated here so this ADR gives a complete `let`/`set` picture for - epic 008 to build on, without re-opening ADR-0006. -- The asymmetry is intentional and not arbitrary: `let` *can* target the - lexical engine (where introduction is free of engine commit), but `set` - *cannot* — `AGENTS.md`'s non-negotiable rule is that `set` on a plain - lexical binding is an error. `set` therefore never has a pure case to - begin with; `let` does. +### 3. `let` targets the lexical engine only — and is therefore unconditionally pure + +- **`let` is restricted to the lexical engine.** It can no longer be + written against `graph` / `dynamic` / `reactive` / `synchronized` at + all — those engines are written exclusively through `set` (§1, §4). This + is a real narrowing of `let`'s syntax, not merely a purity reclassification: + the design note's own "Graph `let ^bool :x be …`" example (§6) is no + longer valid syntax under this ADR — see §4's `LANGUAGE.md`/design-note + fixes. +- Because `let` can only ever introduce a **private, per-scope, never-mutated** + lexical name, it never has an engine-level commit to account for — there + is no longer an engine-dependent case to hedge on. `let :x be ` is + pure **iff `` is itself pure** — nothing else to check. `let :x be + run :copy` is impure not because of anything about the lexical engine, + but because `run` crosses an effect boundary during evaluation regardless + of where the result would land. +- The asymmetry with `set` is now total, not partial: `let` can *only* + target lexical; `set` can *only* target a mutable engine (`AGENTS.md`'s + rule that `set` on a lexical binding is an error already established + `set`'s side of this; §4 below establishes `let`'s side). Neither verb + can reach where the other lives. `set` therefore never has a pure case; + `let` always does (given a pure ``). + +### 4. `AGENTS.md`'s non-negotiable rule is amended + +Per `AGENTS.md`'s own instruction that a non-negotiable syntax rule needs +an ADR to revisit, this ADR replaces its `let`/`set` rule. Old text: + +> `set` mutates an existing binding; `let` introduces a new one (even if +> it shadows a previous name). `set` should only reach the mutable engines +> (graph / dynamic / reactive / synchronized); `set` on a plain lexical +> binding is an error. + +The replacement wording was adopted **provisionally, in the same PR that +drafted this ADR** — `AGENTS.md`'s two `let`/`set` bullets already state it. +It is not final until this ADR's own Status line reads `Accepted` (see +header); until then, treat `AGENTS.md`'s current text as the working rule +under review here, not yet a closed decision. This ADR does not quote it +verbatim to avoid two copies drifting out of sync — read `AGENTS.md`'s +"Non-negotiable syntax rules" section for the exact wording. Summary: `let` +introduces a lexical binding, the only engine it can target; `set` is the +sole write path for the mutable engines (graph / dynamic / reactive / +synchronized), upserting and always effectful; `set` on lexical and `let` +on a mutable engine are both errors — the two verbs partition the engines +completely. + +This also corrects two other stale spots the old introduce-vs-mutate +framing left behind: +- `LANGUAGE.md`'s Bindings section ("`lexical` values are *usually* + constant, but can be declared mutable with `set`") directly contradicted + even the *old* rule (`set` was already barred from lexical) — fixed to + state lexical values are immutable once bound, full stop. +- The design note's §2/§5/§6 rows and `LANGUAGE.md`'s "Algebraic Data + Types" example block used `let ^bool be …`-style type/graph-binding + definitions — genuinely *new* graph bindings, written with `let`. Under + this ADR those become `set ^bool to …` etc.: defining a type is + introducing a graph binding, which `set` now owns. +- `LANGUAGE.md`'s "More Examples" section had two more instances of the + same class: a Dynamic-assignment example block-shadowing `$a` via + `let $a be 500 […]`, and a Closure-syntax example defining a form + binding (`fm%token`, graph engine) via `let some-lambda do … end`. Both + fixed to `set`. ## Non-decisions @@ -130,12 +190,25 @@ classification, not the mechanics, which were never in question. - Does **not** add enforcement to a type checker — none exists yet (per ADR-0006's Non-decisions). This ADR fixes the classification so epic 008 and any later checker build to the same target. -- Does **not** revisit ADR-0006's `let`-into-mutable-engine rule; §3 above - restates it, not re-decides it. +- Does **not** decide the concrete parser/runtime mechanism for + distinguishing "`set` creates" from "`set` updates" inside a given + mutable engine (e.g. whether the engine needs to expose that distinction + at all, or an upsert is genuinely uniform all the way down) — epic 009 + implementation detail. §1's upsert rule fixes the *effect classification* + only, not the mechanics. +- Does **not** revisit `key%token`/`~token` ("static" engine, `AGENTS.md`: + "cannot be rebound") — it is neither `let`'s lexical engine nor one of + `set`'s mutable engines, and this ADR says nothing about how it is + introduced. ## Consequences - **Positive** + - The keyword alone now determines both purity and engine, with no + cross-checking needed: `let` is always lexical and always pure (given + a pure ``); `set` is always a mutable engine and always + effectful. The prior rule required knowing *which engine* a `let` + targeted before its purity was decidable — that lookup is gone. - Epic 008 can classify `set` in its binding-mode taxonomy without ambiguity, and epic 009 can implement mutable binding kinds against a fixed effect rule. @@ -156,6 +229,11 @@ classification, not the mechanics, which were never in question. - Authors who want a "try a mutation, roll back, stay pure" pattern must express it some other way (e.g. as an `^action` that a caller explicitly `run`s) rather than relying on `set` retaining purity. + - `set`'s upsert semantics mean there is no longer a way to assert "this + binding must already exist" versus "create it if missing" at the + keyword level — `set`'s single form covers both. If that distinction + ever matters, epic 009 has to add it as a separate check, not recover + it from which verb was used. ## Follow-ups