diff --git a/docs/JOURNAL.md b/docs/JOURNAL.md index b9d0988..1b80b66 100644 --- a/docs/JOURNAL.md +++ b/docs/JOURNAL.md @@ -3395,3 +3395,148 @@ capture, unchanged), 17a (per-fn arena, gated on user discussion of memory management, unchanged). 16c-aux (`std_list::take`/`drop` refactor onto lit patterns) is a separate iter, gated on orchestrator decision. + +## Iter 16b.2 — planning entry (LetRec capture) + +**Status: planning, not implemented.** This entry is orchestrator +work-product, not an iteration log. It captures the design space +for 16b.2 so the user can review the trade-offs before +implementation, and so a future agent has a sharp brief to work +against. + +**Goal (when implemented).** Lift 16b.1's no-capture restriction. +Support `(let-rec name ...)` whose body references one or more +names bound in the enclosing lexical scope, by augmenting the +lifted top-level fn's signature with the captured names as extra +parameters and rewriting every call site of `name` (in body and +in_term) to pass the captures positionally. + +**Why this is non-trivial.** The lifted fn's signature must +include the captures' types. Those types are not always +discoverable at desugar time: + +- **Captured fn-param**: type is in `f.ty.params[i]`. Known. +- **Captured Lam-param**: type is in `param_tys[i]`. Known. +- **Captured Let-binding**: `Term::Let { name, value, body }` + carries no type annotation on `name`. Type is the inferred + type of `value`, which the typechecker computes — but the + desugar pass runs *before* the typechecker. **Unknown at + desugar time.** +- **Captured Match-arm pattern var**: type is the substituted + field type of the matched constructor, requiring an ADT-def + lookup plus arg-substitution. Computable in principle, but + the desugar pass would need to track the scrutinee's type + through the walk — also a small inference engine. + +**Architectural choices.** Pick one path before implementing: + +1. **Stay at desugar; restrict to fn/Lam-param captures only.** + Reject Let-binding and Match-arm captures with a clear + error → `16b.3` (Let captures) and `16b.4` (Match captures). + Lowest-cost path, covers the most common case (recursive + helpers that close over an enclosing fn's input). + +2. **Move LetRec elimination to a post-typecheck pass.** By + then every `Term` has known types; capture types fall out. + Cost: a new pipeline stage, plus updating `DESIGN.md`'s + pipeline section. Pays off if the post-pass is also where + other future lowerings live (e.g. closure conversion). + +3. **Run a lightweight inference inside desugar.** Just enough + to resolve `Term::Let`-bound names to their value's type. + Effectively a Hindley-Milner pass on a subset of the AST. + Cost: significant; basically duplicating part of + `ailang-check`. Rejected on principle — one source of truth. + +**Recommended path.** (1), shipping incrementally. 16b.2 covers +fn/Lam-params; 16b.3 lifts Let-bindings via path (2). The +benefit of (1) first: it surfaces real-world usage and informs +how often Let-binding capture actually matters. + +**Other restrictions for 16b.2 (under path 1).** + +- **Direct-call only.** The LetRec name `f` may appear in + `body` and `in_term` only as the callee of a `Term::App`, + never as a `Term::Var` in any other position (e.g. passed as + an argument, bound to a `let`, or stored in an ADT field). + Reason: with captures-as-extra-params, every use site needs + the extras appended. Treating `f` as a value would require + a closure object that bundles `f` and its captures — that's + 16b.5 / closure conversion. +- **Monomorphic enclosing fn.** If the enclosing fn is + `forall(...). ...`, the captures' types may mention the + outer's type vars. Constructing the lifted fn's `Forall` is + doable but error-prone; defer to 16b.6. +- **Single-level LetRec.** A LetRec whose body contains + another LetRec that captures the outer's name or params is + not supported in 16b.2; reject with a clear error → 16b.7. + +**What 16b.2 ships (under the recommended scope).** + +- `desugar_term`'s `scope` parameter changes from + `&BTreeSet` to `&BTreeMap`, + where `ScopeEntry` is `KnownType(Type) | LetBound | MatchArm`. +- Each binder extends the map: fn/Lam-params with `KnownType`, + Let-bindings with `LetBound`, Match-arm bindings with + `MatchArm`. +- LetRec arm's capture detection: free-vars ∩ scope-keys. + For each capture, look up `ScopeEntry`. If `KnownType(t)`, + proceed. If `LetBound` / `MatchArm`, error. +- Validate: walk body and in_term, assert `name` only appears + as `Term::App.callee`. Helper `validate_callee_only_use`. +- Build augmented fn type: `original.ty` with capture types + appended to `params`. Reject if `original.ty` is `Forall` + (out of scope per restriction 2 above). +- Rewrite call sites: `(app f a b)` → `(app f$lr_N a b cap0 + cap1)`. Use a new helper `subst_call_with_extras` that + walks the term, recognizes `Term::App { callee = Var{f} }` + patterns, rewrites them, and recurses elsewhere. +- Substitute `f` → `f$lr_N` everywhere in body (for the + recursive self-reference at the lifted level). The existing + `subst_var` from 16b.1 handles this, but care needed: it + must run **after** `subst_call_with_extras` so that + recursive calls get both the rename and the extras. +- Append the lifted `FnDef` to `Module.defs`. + +**Risk.** The most likely failure mode is the typechecker +rejecting a synthesized augmented fn signature that we believe +should type-check. Mitigation: implement under restriction 2 +(no Forall) so we never construct a Forall; the augmented type +is plain `Type::Fn` with monomorphic capture types appended. + +**Tests.** + +- `examples/local_rec_capture.ailx`: an enclosing fn with one + Int param, a LetRec that recurses against that param. e2e + asserts an output value derived from that capture. +- Negative tests at the desugar unit-test level: Let-binding + capture errors; Match-arm capture errors; name-as-value + errors; nested LetRec mutual-capture errors. All + `#[should_panic]` (consistent with 16b.1's panic discipline). + +**Adjacent open items.** + +- **16d**: chain-machinery's `Unit` terminator forces a + trailing `_` arm in matches that are otherwise exhaustive, + surfaced by 16c (`categorize_first` fixture). Two design + paths: (a) introduce a polymorphic `__unreachable__` + builtin that codegen lowers to LLVM `unreachable`, used as + the chain default; (b) run an exhaustiveness pre-check in + desugar against the scrutinee's ADT and omit the + terminator when arms cover all ctors. Path (a) is broader + (gives users a primitive for panics/asserts). Path (b) is + purer (terminator never appears for exhaustive matches) + but needs ADT lookup in desugar. +- **16e**: extend `==` from Int-only to Int/Bool/Str. Bool + comparison is i1-equality (trivial). Str comparison + needs a runtime `strcmp`. Surfaced by 16c (`build_eq` + produces `(app == ...)` for Bool/Str/Unit but currently + fails at typecheck because `==` is not declared for them). +- **17a**: per-fn arena allocator. Gated on user + memory-management discussion (separate stored memory). + +**Queue update post-16c.** 16c done. Open: 16b.2 (this entry — +planning only, awaiting user input on path 1 vs path 2), 16d +(planning needed — pick path a vs b), 16e (`==` extension), +17a (gated). All implementation work in this session-arc is +suspended at this planning checkpoint.