Pre-register top-level defn types for mutual recursion (eigentrust pitfall #4)#14
Pre-register top-level defn types for mutual recursion (eigentrust pitfall #4)#14kumavis wants to merge 1 commit into
Conversation
…itfall #14) The reader accepts type applications like `[PVec Rat]`, `[Map Keyword Nat]`, `[Set Nat]`, etc. — per the Prologos syntax convention that `[]` is the universal functional/type-context delimiter while `()` is reserved for parser keywords (match, the, def, relational goals). Pre-fix, the pretty-printer emitted `(PVec Rat)`, `(Set Nat)`, `(Map K V)` in parens, producing a cosmetic divergence between how types are read vs printed. EigenTrust implementation (2026-04-23) flagged this as pitfall #14: "the reader accepts `@[1/4 1/4 1/4 1/4]` and the type-checker reports the value as `(PVec Rat)` — but the output ... writes `(PVec Rat)` in parens where the type signature of a `spec` would say `[PVec Rat]`." Choice: broad fix. The pitfall observation generalizes — the same `(T A)` printing was used by Map, Set, PVec, TVec, TMap, TSet (type forms) and by set-empty, set-insert, set-member?, set-delete, set-size, set-union, set-intersect, set-diff, set-to-list, pvec-empty annotation (operation forms). Per `.claude/rules/prologos-syntax.md` ALL functional contexts use `[]`, so all of these are switched together. Existing forms like `[Vec ...]`, `[Sigma ...]`, `[map-assoc ...]`, `[pvec-push ...]` already followed this convention; this brings the rest into alignment. Snapshot updates: 4 existing tests had hard-coded `(...)` snapshots: - tests/test-pvec.rkt (PVec type pp) - tests/test-set.rkt (Set type pp + "s : (Set Nat) defined" message) - tests/test-map.rkt (Map type pp + "m : (Map Keyword Nat) defined") - tests/test-implicit-map-02.rkt ("@[:admin :active] : (PVec Keyword)") All updated to the new `[T A]` form. New test file: tests/test-pretty-print-pvec.rkt covers the primary fix plus operation forms and nested type applications, with regression guards on already-correct forms (Vec, simple application). https: //claude.ai/code/session_01MbncYJnrvjzhbVWw4xGi5x Co-authored-by: kumavis <1474978+kumavis@users.noreply.github.com>
2c73c62 to
ada6016
Compare
|
missing argument in defn for odd? and even? |
|
hiero doesn't like pre-register-defn-types! and thinks there should already be a mechanism for this. this may be affected by the in-flight elaboration refactor. so this can wait. |
Adds a pre-pass before the main process-command loop that pre-registers
each spec'd defn's name in the global env with its declared type. This
makes forward references between top-level defns resolve regardless of
source order, so the canonical even?/odd? pattern (and any other mutual
or forward-reference cycle) works without source-order workarounds.
Approach: (b) — leverage the existing spec system. The pre-pass calls
expand-top-level on each surf, walks surf-def and surf-def-group, and
for each annotated def elaborates ONLY the type and installs the name
via global-env-add-type-only. The main loop's process-def then
overwrites the entry with the freshly-zonked type once the body is
elaborated. Approach (b) was preferred over (a) placeholder types and
(c) SCC analysis because Prologos's idiomatic style already pairs
defns with specs, and a placeholder type would have required taught
the type-checker to tolerate it.
Pre-registration uses the legacy parameter path (current-prelude-env)
rather than the cell path: it's visible to global-env-lookup-type via
Layer 2 fallback, is properly test-isolated (run-ns-* helpers reset
the parameter), and gets overwritten by the cell-path write in the
main pass.
Behavior on spec-less mutual recursion: Prologos already handles this
via inferred hole-typed defns ('_ -> _'). The pre-pass skips defs
without a type annotation, so spec-less defns continue to elaborate
through their existing path. Both spec'd and spec-less mutual
recursion now resolve.
Three call sites updated (one per top-level entry path):
- process-string-inner (sexp string)
- process-surfs (WS string, common tail)
- process-file-inner (.prologos file)
Tests:
- tests/test-mutual-recursion.rkt: 7 tests covering canonical
forward reference, two-way mutual cycle, three-way chain,
self-recursion regression, and spec-less mutual recursion.
- All pre-existing tests still pass (test-multi-body-defn,
test-spec-ordering, test-process-ws-01/02, test-spec,
test-pattern-defn-01/02, test-elaborator,
test-elaborator-network, test-module-network-01,
test-process-parse-01: 227 tests total).
Co-authored-by: kumavis <1474978+kumavis@users.noreply.github.com>
ada6016 to
e42482e
Compare
…itfall #14) The reader accepts type applications like `[PVec Rat]`, `[Map Keyword Nat]`, `[Set Nat]`, etc. — per the Prologos syntax convention that `[]` is the universal functional/type-context delimiter while `()` is reserved for parser keywords (match, the, def, relational goals). Pre-fix, the pretty-printer emitted `(PVec Rat)`, `(Set Nat)`, `(Map K V)` in parens, producing a cosmetic divergence between how types are read vs printed. EigenTrust implementation (2026-04-23) flagged this as pitfall #14: "the reader accepts `@[1/4 1/4 1/4 1/4]` and the type-checker reports the value as `(PVec Rat)` — but the output ... writes `(PVec Rat)` in parens where the type signature of a `spec` would say `[PVec Rat]`." Choice: broad fix. The pitfall observation generalizes — the same `(T A)` printing was used by Map, Set, PVec, TVec, TMap, TSet (type forms) and by set-empty, set-insert, set-member?, set-delete, set-size, set-union, set-intersect, set-diff, set-to-list, pvec-empty annotation (operation forms). Per `.claude/rules/prologos-syntax.md` ALL functional contexts use `[]`, so all of these are switched together. Existing forms like `[Vec ...]`, `[Sigma ...]`, `[map-assoc ...]`, `[pvec-push ...]` already followed this convention; this brings the rest into alignment. Snapshot updates: 4 existing tests had hard-coded `(...)` snapshots: - tests/test-pvec.rkt (PVec type pp) - tests/test-set.rkt (Set type pp + "s : (Set Nat) defined" message) - tests/test-map.rkt (Map type pp + "m : (Map Keyword Nat) defined") - tests/test-implicit-map-02.rkt ("@[:admin :active] : (PVec Keyword)") All updated to the new `[T A]` form. New test file: tests/test-pretty-print-pvec.rkt covers the primary fix plus operation forms and nested type applications, with regression guards on already-correct forms (Vec, simple application). https: //claude.ai/code/session_01MbncYJnrvjzhbVWw4xGi5x Co-authored-by: kumavis <1474978+kumavis@users.noreply.github.com>
…-pp01 pretty-print: emit type-applied forms with [T A] syntax (eigentrust pitfall #14)
hierophantos
left a comment
There was a problem hiding this comment.
Substantive review. The fix solves a real and important bug — mutual recursion is a fundamental FP idiom — and the PR shows careful work: honest framing of Approach b vs a/c, self-correction during development (the "Subtle bug avoided" disclosure), and 7 well-targeted tests including 3-way and spec-less cases.
Holding for revision per your own "pending revisit after elaboration refactor" flag in #19. Four architectural concerns I'd flag for the revision direction:
1. Triplicated call site (pre-register-defn-types! × 3). Same call at process-string-inner, process-surfs, process-file-inner with identical ~10-line comment blocks. This is the Two-Context Boundary anti-pattern in our .claude/rules/pipeline.md. Cleaner shape: one helper wrapping (pre-pass + parameterize-and-loop), called from each path.
2. Defensive with-handlers exn:fail? -> void swallows real failures. Three instances across the new helpers, with comment "never block main pass". But if pre-registration fails for a real reason (bug in expand-top-level, malformed surf, type elaboration against uninitialized cells), the user gets "Unbound variable" with no diagnostic about why. Per our workflow.md adversarial-framing rule, this is a flagged pattern: is the guarded condition structurally possible? If so, surface the diagnostic instead of swallowing.
3. "Layer 2 fallback" reliance pushes against migration direction. The "Subtle bug avoided" disclosure shows the fix depends on the legacy parameter path (current-prelude-env) and global-env-lookup-type's Layer 2 fallback. Our project is mid-migration AWAY from parameter-based state TOWARD cell-based state (PM Track 12). New feature on the legacy fallback adds debt.
4. PPN 4C interaction worth flagging specifically. pre-register-single-def! parameterizes fresh meta stores but doesn't initialize the propagator network's universe cells. With our active PPN 4C universe migration (S2.b-iv etc.), type elaboration that creates a type meta in the pre-pass will hit cells that aren't fully initialized. The defensive with-handlers catches the failure silently, defeating pre-registration without diagnostic. Today it works because the migration is partway; tomorrow it might silently break.
Revision direction worth considering:
- Single dispatch helper (not 3 call sites)
- Surface diagnostic info when pre-registration fails (or prove failure modes are structurally impossible)
- Coordinate with the cell-migration direction
- Consider whether SCC-based topology phase becomes reachable post-refactor
Not blocking — happy to engage further as revision lands.
Add Phase 4 to the addendum design doc as a future sub-phase covering
process-command sequential orchestrator retirement. Closes the gap
between the thesis ("no sequential orchestrators alongside the BSP
scheduler") and the original phase breakdown (which delivered only the
in-form orchestrator retirement at metavar-store).
Three locations updated in 2026-04-21_PPN_4C_PHASE_9_DESIGN.md:
§1.1 Thesis: extended from three architectural moves to four. Move 2
"Orchestration" retitled to "Orchestration (in-form)" to disambiguate
from the new move 4 "Orchestration (between-form)".
§1.2 Phase scope: added Phase 4 description with bullets covering
process-command retirement, BSP-stratum-handler dispatch per form
type, topology-phase semantics, mutual recursion as falling-out, and
coordination with PM Track 12 + PM Track 10. LoC TBD; mini-design at
phase open per addendum methodology.
§3 Progress Tracker: added Phase 4 row before V (Capstone) row,
status ⬜, references #22 + PR #14.
Designed when current Phase 1 (tropical fuel) and Phase 2 (in-form
strata) close. Motivating use case: mutual recursion (PR #14, kumavis
pitfall #4) currently scaffolded via pre-pass; structural fix lands
with this phase.
Tracking issue: #22
Dailies entry: 2026-04-26 dailies "Parallel session — external
contributor PR review pass"
Wires the OCapN port to a real Racket toolchain and fixes the issues
the test run surfaced.
Library fixes
- vat.prologos: rename `spawn` -> `vat-spawn` (collision with the
reserved surface form recognised in macros.rkt:`'spawn`),
`spawn-actor` -> `vat-spawn-actor`. Same in core.prologos and the
acceptance file.
- vat.prologos: drop the `Sigma Vat Nat` return shape for spawn /
fresh-promise / send. Replace with a named `Allocated` struct +
`alloc-vat` / `alloc-id` accessors. The Sigma form ran into
"could not infer" elaborator errors when the body destructured
via `match | pair a b -> ...` and then re-constructed a Sigma;
`[fst p]` / `[snd p]` reused on the same `p` tripped QTT
multiplicity. The named struct sidesteps both.
- vat.prologos: reorder `resolve-promise` / `break-promise` BEFORE
`apply-effect` (forward-reference rule — module elaboration is
single-pass top-to-bottom). Also reorder `step-after-act` before
`deliver-msg` and `list-length-helper` before `queue-length`.
- vat.prologos: drop the queued-pipeline-flush in resolve-promise /
break-promise. PromiseState's queue is `List SyrupValue` (wire
repr); the vat queue is `List VatMsg` (decoded); flushing across
the boundary would need re-encoding. Phase 1.
Test-fixture fix (load-bearing)
- All 8 OCapN test files were updated to capture and restore
`current-ctor-registry` and `current-type-meta` across the setup-
-> run boundary. The standard fixture pattern from
`test-hashable-01.rkt` does NOT preserve these — fine for tests
that only declare traits, but breaks once a preamble's imports
declare new `data` types (every `data` in our 8 modules). Without
it, the reducer sees a stale ctor-registry and refuses to fire
pattern arms over user constructors; results print as un-reduced
`[reduce ... | vat x y z a -> x] : Nat` strings.
Documented as goblin-pitfall #12; the canonical fixture in
test-support.rkt should grow this for every future test.
Compat fence
- driver.rkt: guard
`(current-parallel-executor (make-parallel-thread-fire-all))` with
a feature-detection try/catch on `thread #:pool 'own`. Racket 9
ships parallel threads; Racket 8 does not. Fence preserves the
Racket-9 fast path and falls back to sequential firing on 8.
Acceptance
- examples/2026-04-27-ocapn-acceptance.prologos updated to match
the new vat-spawn/Allocated API and verified to run clean via
process-file.
Pitfalls catalogue (docs/tracking/2026-04-27_GOBLIN_PITFALLS.md)
- #0 (sandbox/no-Racket): closed.
- +#11 — Racket-8 vs Racket-9 `thread #:pool` compat
- +#12 — test fixture loses ctor-registry/type-meta across calls
[highest-impact; canonical fixture pattern needs update]
- +#13 — `spawn` is a reserved surface keyword; collides silently
- +#14 — `match | pair a b ->` on Sigma + Sigma reconstruction =>
"could not infer"
- +#15 — QTT multiplicity on `[fst p]`/`[snd p]` reused thrice
- +#16 — single-pass module elaboration: forward references error
- +#17 — promise-queue (Syrup) vs vat-queue (VatMsg) type clash
on flush — design pitfall, scope cut
Test results
refr 6/6 syrup 22/22 promise 16/16 message 19/19
behavior 13/13 vat 21/21 pipeline 5/5 captp 7/7
e2e 8/8 total 117/117 PASS
Per user direction: - Replace the body of every DELETED entry with a single-sentence explanation. Numbers reserved per prior instruction. - Delete #15 (QTT multiplicity on fst/snd thrice). I re-tested with a real Racket — `pair [snd p] [fst p]` then a third use of `fst p` works fine; no multiplicity error. The failure I had conflated this with was actually #14's "match-and-reconstruct Sigma" issue. Result: pitfalls doc shrinks from 765 to 534 lines. Remaining real claims: #1, #4, #5, #11, #12, #13, #14, #16, #17, #18, #19, #20 (the user has reviewed only #0-10 so far; #11-20 still pending their review).
Adds `BridgeState` (a side data structure carried alongside the
Vat) and a state-aware dispatcher `captp-incoming-with-state`
that updates BOTH Vat and BridgeState per inbound op.
Phase 11's `incoming-captp-op` was no-op for op:listen and
op:gc-*; this commit captures them in the bridge state.
Module additions to captp-bridge.prologos:
data Listener — (target-promise-id, resolver-position-on-peer)
data GcExportReq — (export-pos, count)
data BridgeState — (listeners, gc-export-requests, gc-answer-positions)
data BridgeStep — concrete (Vat, BridgeState) struct (avoids
Sigma-pattern-match issue per pitfall #14)
bridge-state-empty : BridgeState
bs-listeners / bs-gc-exports / bs-gc-answers — accessors
bs-add-listener / bs-add-gc-export / bs-add-gc-answer — pure updates
captp-incoming-with-state : CapTPOp -> Vat -> BridgeState -> BridgeStep
Dispatch table:
op:deliver → enqueue VatMsg in vat (state unchanged)
op:deliver-only → send-only on vat (state unchanged)
op:abort → no-op (vat unchanged, state unchanged)
op:start-session → no-op (vat unchanged, state unchanged)
op:listen → bs-add-listener tgt resolver state
op:gc-export → bs-add-gc-export pos cnt state
op:gc-answer → bs-add-gc-answer pos state
Test additions (4 cases, total 12 in test-ocapn-bridge.rkt).
Tests: 12/12 green on Racket 9.1.
https://claude.ai/code/session_01YM6gc3cMNH2Ymor4jdZY8u
Wires the OCapN port to a real Racket toolchain and fixes the issues
the test run surfaced.
Library fixes
- vat.prologos: rename `spawn` -> `vat-spawn` (collision with the
reserved surface form recognised in macros.rkt:`'spawn`),
`spawn-actor` -> `vat-spawn-actor`. Same in core.prologos and the
acceptance file.
- vat.prologos: drop the `Sigma Vat Nat` return shape for spawn /
fresh-promise / send. Replace with a named `Allocated` struct +
`alloc-vat` / `alloc-id` accessors. The Sigma form ran into
"could not infer" elaborator errors when the body destructured
via `match | pair a b -> ...` and then re-constructed a Sigma;
`[fst p]` / `[snd p]` reused on the same `p` tripped QTT
multiplicity. The named struct sidesteps both.
- vat.prologos: reorder `resolve-promise` / `break-promise` BEFORE
`apply-effect` (forward-reference rule — module elaboration is
single-pass top-to-bottom). Also reorder `step-after-act` before
`deliver-msg` and `list-length-helper` before `queue-length`.
- vat.prologos: drop the queued-pipeline-flush in resolve-promise /
break-promise. PromiseState's queue is `List SyrupValue` (wire
repr); the vat queue is `List VatMsg` (decoded); flushing across
the boundary would need re-encoding. Phase 1.
Test-fixture fix (load-bearing)
- All 8 OCapN test files were updated to capture and restore
`current-ctor-registry` and `current-type-meta` across the setup-
-> run boundary. The standard fixture pattern from
`test-hashable-01.rkt` does NOT preserve these — fine for tests
that only declare traits, but breaks once a preamble's imports
declare new `data` types (every `data` in our 8 modules). Without
it, the reducer sees a stale ctor-registry and refuses to fire
pattern arms over user constructors; results print as un-reduced
`[reduce ... | vat x y z a -> x] : Nat` strings.
Documented as goblin-pitfall #12; the canonical fixture in
test-support.rkt should grow this for every future test.
Compat fence
- driver.rkt: guard
`(current-parallel-executor (make-parallel-thread-fire-all))` with
a feature-detection try/catch on `thread #:pool 'own`. Racket 9
ships parallel threads; Racket 8 does not. Fence preserves the
Racket-9 fast path and falls back to sequential firing on 8.
Acceptance
- examples/2026-04-27-ocapn-acceptance.prologos updated to match
the new vat-spawn/Allocated API and verified to run clean via
process-file.
Pitfalls catalogue (docs/tracking/2026-04-27_GOBLIN_PITFALLS.md)
- #0 (sandbox/no-Racket): closed.
- +#11 — Racket-8 vs Racket-9 `thread #:pool` compat
- +#12 — test fixture loses ctor-registry/type-meta across calls
[highest-impact; canonical fixture pattern needs update]
- +#13 — `spawn` is a reserved surface keyword; collides silently
- +#14 — `match | pair a b ->` on Sigma + Sigma reconstruction =>
"could not infer"
- +#15 — QTT multiplicity on `[fst p]`/`[snd p]` reused thrice
- +#16 — single-pass module elaboration: forward references error
- +#17 — promise-queue (Syrup) vs vat-queue (VatMsg) type clash
on flush — design pitfall, scope cut
Test results
refr 6/6 syrup 22/22 promise 16/16 message 19/19
behavior 13/13 vat 21/21 pipeline 5/5 captp 7/7
e2e 8/8 total 117/117 PASS
Per user direction: - Replace the body of every DELETED entry with a single-sentence explanation. Numbers reserved per prior instruction. - Delete #15 (QTT multiplicity on fst/snd thrice). I re-tested with a real Racket — `pair [snd p] [fst p]` then a third use of `fst p` works fine; no multiplicity error. The failure I had conflated this with was actually #14's "match-and-reconstruct Sigma" issue. Result: pitfalls doc shrinks from 765 to 534 lines. Remaining real claims: #1, #4, #5, #11, #12, #13, #14, #16, #17, #18, #19, #20 (the user has reviewed only #0-10 so far; #11-20 still pending their review).
Adds `BridgeState` (a side data structure carried alongside the
Vat) and a state-aware dispatcher `captp-incoming-with-state`
that updates BOTH Vat and BridgeState per inbound op.
Phase 11's `incoming-captp-op` was no-op for op:listen and
op:gc-*; this commit captures them in the bridge state.
Module additions to captp-bridge.prologos:
data Listener — (target-promise-id, resolver-position-on-peer)
data GcExportReq — (export-pos, count)
data BridgeState — (listeners, gc-export-requests, gc-answer-positions)
data BridgeStep — concrete (Vat, BridgeState) struct (avoids
Sigma-pattern-match issue per pitfall #14)
bridge-state-empty : BridgeState
bs-listeners / bs-gc-exports / bs-gc-answers — accessors
bs-add-listener / bs-add-gc-export / bs-add-gc-answer — pure updates
captp-incoming-with-state : CapTPOp -> Vat -> BridgeState -> BridgeStep
Dispatch table:
op:deliver → enqueue VatMsg in vat (state unchanged)
op:deliver-only → send-only on vat (state unchanged)
op:abort → no-op (vat unchanged, state unchanged)
op:start-session → no-op (vat unchanged, state unchanged)
op:listen → bs-add-listener tgt resolver state
op:gc-export → bs-add-gc-export pos cnt state
op:gc-answer → bs-add-gc-answer pos state
Test additions (4 cases, total 12 in test-ocapn-bridge.rkt).
Tests: 12/12 green on Racket 9.1.
https://claude.ai/code/session_01YM6gc3cMNH2Ymor4jdZY8u
… LOCKED (§18.21.25) + (iii) capture in PM 12B §10 / PM 13 §9 Grounding wf_dc6f6166-dfa (6 facets + critic @ ed8e220; R-lens-verified) + probes (G1 pinned: PR #14 = spec'd single-arity mutual = a CYCLE -> SCC pass gate-critical) + co-design. Six reframes incl. D3-premise dissolution (dormant+broken reset template; live discard = reset-meta-store!; forms/NET-1 survive — NET-2 state dies). Locks: (ii-b) + A1 pending-arm + (c-1)===(c-2) unified assumption-env + demand-driven sweep (DEF-vs-USE amended) + tier principle + multi-arity->12B + partition a/b/c. No production .rkt changes (design-doc only).
Fixes pitfall #4 from
docs/tracking/2026-04-23_eigentrust_pitfalls.md.Summary
failed with
Unbound variable: odd?— the seconddefnwas textually after the first, but the first's body referenced it. Same problem in either order.Approach (b) — two-phase, leveraging the spec system
A new
pre-register-defn-types!pass runs once before the mainprocess-commandloop. For each top-level surf, it callsexpand-top-level, then forsurf-def(or each clause ofsurf-def-group) with a declared type, elaborates the type only and installs the name viaglobal-env-add-type-only. The main loop'sprocess-deflater overwrites the entry with the freshly-zonked type after body elaboration.Why (b) over alternatives:
defnwithspec, so the spec system already knows the type before the body is elaboratedBehavior on spec-less mutual recursion
Surprise: it already works via Prologos's inferred hole-typed
defnpath (_ → _). The pre-pass skips defs without type annotations; the existing inference path handles them. So both spec'd and spec-less mutual recursion now resolve uniformly.Files changed
racket/prologos/driver.rkt—pre-register-defn-types!helper (~100 lines), called from each of the three top-level processing paths:process-string-inner(sexp),process-surfs(WS string common tail), andprocess-file-inner(.prologosfile)racket/prologos/tests/test-mutual-recursion.rkt(new, 7 cases)examples/2026-04-25-mutual-recursion-repro.prologos(canonical even?/odd? repro)Test plan
benchmarks/micro/info.rktskip; redundant once PR Migrate bench-bsp-le-track2.rkt to current ATMS API (CI unblock) #10's actual migration lands first)Subtle bug avoided
First iteration parameterized
current-prelude-env-prop-net-boxin the pre-pass, which leaked definition cell content acrossprocess-stringcalls and broke test isolation. Switching to the legacy parameter path (noparameterize) fixed it becauserun-ns-*helpers resetcurrent-prelude-env, andglobal-env-lookup-type's Layer 2 fallback finds the pre-registered names. Documented in the commit message.Commits
f6ca8ad— primary fix indriver.rkt+ test file + repro example2c73c62— CI fix (skip stale bench)https://claude.ai/code/session_01MbncYJnrvjzhbVWw4xGi5x
Generated by Claude Code