Skip to content

Pre-register top-level defn types for mutual recursion (eigentrust pitfall #4) #14

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
kumavis wants to merge 1 commit into
base: main
Choose a base branch
from
+344 −0
Draft

Pre-register top-level defn types for mutual recursion (eigentrust pitfall #4) #14

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 13 additions & 0 deletions examples/2026-04-25-mutual-recursion-repro.prologos
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
ns mutrec-repro

spec even? Nat -> Bool
defn even?
| zero -> true
| suc n -> [odd? n]

spec odd? Nat -> Bool
defn odd?
| zero -> false
| suc n -> [even? n]

[even? 4N]
131 changes: 131 additions & 0 deletions racket/prologos/driver.rkt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -441,6 +441,104 @@
(define current-form-cell-map (make-parameter (hasheq)))
(define current-spec-cell-map (make-parameter (hasheq)))

;; ========================================
;; Mutual recursion pre-registration
;; ========================================
;;
;; Top-level forms are processed sequentially by process-command. For a single
;; defn referencing itself, process-def's global-env-add-type-only call (around
;; line 1177) installs the name's declared type before elaborating the body —
;; that handles SELF-recursion. For MUTUAL recursion between two defns A and B,
;; when A's body is elaborated B's name is not yet visible because A runs
;; first.
;;
;; pre-register-defn-types! runs once before the main process-command loop and
;; performs Phase A of a two-phase elaboration: for every defn or def with a
;; declared type (the spec system injects spec types into the def surface form
;; during preparse), elaborate ONLY the type and pre-register the name in the
;; global env via global-env-add-type-only. The main loop's body elaboration
;; (Phase B) then sees all spec'd names in scope, regardless of source order.
;;
;; A defn WITHOUT a spec follows the standard sequential path: its name is
;; only visible after its own process-command call completes, so mutual
;; recursion without specs surfaces a clear "Unbound variable" error. With
;; specs on both functions in a mutual cycle (the idiomatic Prologos style),
;; mutual recursion is supported.
;;
;; Each pre-registration runs in a parameterize that resets the meta store and
;; isolates type-elaboration metas from the main pass; no leakage.
(define (pre-register-defn-types! surfs)
(for ([surf (in-list surfs)])
(with-handlers ([exn:fail? (lambda (_) (void))]) ;; never block main pass
(pre-register-one-defn-type! surf))))

(define (pre-register-one-defn-type! surf)
;; Skip non-surfs and errors immediately
(cond
[(prologos-error? surf) (void)]
[else
;; Run expand-top-level to convert surf-defn into surf-def or
;; surf-def-group (this is what process-command does first thing).
(define expanded
(with-handlers ([exn:fail? (lambda (_) #f)])
(expand-top-level surf)))
(cond
[(or (not expanded) (prologos-error? expanded)) (void)]
[(surf-def? expanded)
(pre-register-single-def! expanded)]
[(surf-def-group? expanded)
;; Multi-arity defn: pre-register the dispatch name AND each per-arity
;; clause def. The dispatch table will be re-built by process-def-group
;; in the main pass — pre-registration here just ensures the name is
;; visible during forward references.
(define group-name (surf-def-group-name expanded))
(define arities (surf-def-group-arities expanded))
(define docstring (surf-def-group-docstring expanded))
(define arity-map
(for/fold ([m (hasheq)])
([arity (in-list arities)])
(hash-set m arity (string->symbol (format "~a::~a" group-name arity)))))
(with-handlers ([exn:fail? (lambda (_) (void))])
(register-multi-defn! group-name arities arity-map docstring)
(when (current-ns-context)
(define fqn-ns (ns-context-current-ns (current-ns-context)))
(define fqn (qualify-name group-name fqn-ns))
(define fqn-arity-map
(for/fold ([m (hasheq)])
([arity (in-list arities)])
(hash-set m arity (qualify-name
(string->symbol (format "~a::~a" group-name arity))
fqn-ns))))
(register-multi-defn! fqn arities fqn-arity-map docstring)))
(for ([def (in-list (surf-def-group-defs expanded))])
(pre-register-single-def! def))]
[else (void)])]))

(define (pre-register-single-def! expanded)
;; Only annotated defs can be pre-registered (we need a type for the env).
(define name (surf-def-name expanded))
(define type-surf (surf-def-type expanded))
(cond
[(not type-surf) (void)] ;; type-inferred def: skip; falls back to current behavior
[(not (symbol? name)) (void)]
[else
;; Isolate meta state for this type elaboration.
(parameterize ([current-meta-store (make-hasheq)]
[current-level-meta-store (make-hasheq)]
[current-mult-meta-store (make-hasheq)])
(with-handlers ([exn:fail? (lambda (_) (void))])
(define type
(with-handlers ([exn:fail? (lambda (_) #f)])
(elaborate type-surf)))
(when (and type (not (prologos-error? type)))
;; process-def in the main pass will OVERWRITE this with the
;; freshly-elaborated and zonked type, then proceed with the body.
(global-env-add-type-only (current-prelude-env) name type)
(when (current-ns-context)
(define fqn (qualify-name name
(ns-context-current-ns (current-ns-context))))
(global-env-add-type-only (current-prelude-env) fqn type)))))]))

;; Returns a result string, or a prologos-error.
;; Side effect: may update current-prelude-env for 'def'.
;;
Expand Down Expand Up @@ -1473,6 +1571,17 @@
(define pv (provenance-counters 0 0 0 0 0 0 0 0))
(define qs (make-quiescence-stats))
(define mem-before (measure-memory-before))
;; Pre-register defn names with declared types so that mutual recursion
;; (forward references between top-level defns) works without source-order
;; dependence. See pre-register-defn-types! above.
;; NOTE: deliberately NOT parameterizing current-prelude-env-prop-net-box
;; here. Pre-registration uses the legacy parameter path
;; (writes to current-prelude-env), which:
;; (a) is properly test-isolated (the standard run-ns-* helpers reset it),
;; (b) is visible to global-env-lookup-type via the Layer 2 fallback, and
;; (c) gets overwritten by process-def's normal cell-path write in the
;; main pass once the body has been elaborated and zonked.
(pre-register-defn-types! surfs)
(define-values (results pc)
(parameterize ([current-phase-timings pt]
[current-provenance-counters pv]
Expand Down Expand Up @@ -1671,6 +1780,17 @@
(define pv (provenance-counters 0 0 0 0 0 0 0 0))
(define qs (make-quiescence-stats))
(define mem-before (measure-memory-before))
;; Pre-register defn names with declared types so that mutual recursion
;; (forward references between top-level defns) works without source-order
;; dependence. See pre-register-defn-types! above.
;; NOTE: deliberately NOT parameterizing current-prelude-env-prop-net-box
;; here. Pre-registration uses the legacy parameter path
;; (writes to current-prelude-env), which:
;; (a) is properly test-isolated (the standard run-ns-* helpers reset it),
;; (b) is visible to global-env-lookup-type via the Layer 2 fallback, and
;; (c) gets overwritten by process-def's normal cell-path write in the
;; main pass once the body has been elaborated and zonked.
(pre-register-defn-types! surfs)
(define-values (results pc)
(parameterize ([current-phase-timings pt]
[current-provenance-counters pv]
Expand Down Expand Up @@ -1741,6 +1861,17 @@
(init-warning-cells! prn-box)
(init-narrow-cells! prn-box)
(init-attribute-map-cell! prn-box)) ;; Track 4B Phase 0c: global attribute store
;; Pre-register defn names with declared types so that mutual recursion
;; (forward references between top-level defns) works without source-order
;; dependence. See pre-register-defn-types! above.
;; NOTE: deliberately NOT parameterizing current-prelude-env-prop-net-box
;; here. Pre-registration uses the legacy parameter path
;; (writes to current-prelude-env), which:
;; (a) is properly test-isolated (the standard run-ns-* helpers reset it),
;; (b) is visible to global-env-lookup-type via the Layer 2 fallback, and
;; (c) gets overwritten by process-def's normal cell-path write in the
;; main pass once the body has been elaborated and zonked.
(pre-register-defn-types! surfs)
(define-values (results pc)
(parameterize ([current-phase-timings pt]
[current-provenance-counters pv]
Expand Down
200 changes: 200 additions & 0 deletions racket/prologos/tests/test-mutual-recursion.rkt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,200 @@
#lang racket/base

;;;
;;; Tests for mutual recursion between top-level defns.
;;;
;;; Eigentrust pitfalls doc #4 (2026-04-25): two defns referencing each
;;; other (e.g., even?/odd?) used to fail with "Unbound variable" for
;;; whichever came second in source order, because process-command processed
;;; each top-level form sequentially against an env that didn't yet contain
;;; the later defn.
;;;
;;; The fix in driver.rkt's pre-register-defn-types! pre-elaborates each
;;; defn's spec'd type and installs the name in current-prelude-env BEFORE
;;; any body is elaborated. Both directions (A->B and B->A) of the mutual
;;; cycle now resolve.
;;;
;;; Behavior on spec-less mutual recursion: still fails. The pre-pass
;;; needs a declared type to install in the env. A defn without a spec
;;; has no type to pre-register, so it falls back to the existing
;;; sequential behavior.
;;;
;;; Tests follow test-spec-ordering.rkt's pattern: empty starting env, build
;;; from natrec primitives only (no prelude dependency).
;;;

(require rackunit
racket/string
racket/list
"../prelude.rkt"
"../syntax.rkt"
"../surface-syntax.rkt"
"../parser.rkt"
"../elaborator.rkt"
"../pretty-print.rkt"
"../errors.rkt"
"../typing-errors.rkt"
"../global-env.rkt"
"../driver.rkt"
"../macros.rkt"
"../source-location.rkt")

;; ========================================
;; Helper — sexp-mode runner with isolated env
;; ========================================
(define (run s)
(parameterize ([current-prelude-env (hasheq)]
[current-module-definitions-content (hasheq)]
[current-spec-store (hasheq)]
[current-preparse-registry (current-preparse-registry)])
(process-string s)))

;; ========================================
;; 1. Canonical mutual recursion: forward reference between two defns,
;; both with specs (the idiomatic Prologos style).
;;
;; The first defn's body refers to the second; without the fix, this
;; fails because the second's name is not yet in the env.
;; ========================================

(test-case "mutrec: forward reference, A calls B (both spec'd)"
;; A is defined first; A's body references B; B is defined later.
;; Pre-fix: "Unbound variable B" while elaborating A. Post-fix: works.
(define results
(run (string-append
"(spec inc-via-suc Nat -> Nat)\n"
"(defn inc-via-suc [n] (use-suc n))\n"
"(spec use-suc Nat -> Nat)\n"
"(defn use-suc [n] (suc n))\n"
"(eval (inc-via-suc zero))")))
(check-equal? (length results) 3)
(check-equal? (caddr results) "1N : Nat"))

;; ========================================
;; 2. Two-way mutual recursion: A calls B, B calls A.
;; Genuine mutual cycle, both with specs.
;; ========================================

(test-case "mutrec: two-way cycle (both call each other)"
;; even?/odd? in spirit, but built on natrec since we have no Bool/not.
;; even-len: counts steps in pairs via odd-len.
;; odd-len: steps once, then defers to even-len.
;; Both are natrec-decreasing, so termination is fine.
;; Without the fix: elaborating even-len fails on odd-len.
(define results
(run (string-append
"(spec even-len Nat -> Nat)\n"
"(defn even-len [n]"
" (natrec Nat zero (fn (k : Nat) (fn (r : Nat) (odd-len k))) n))\n"
"(spec odd-len Nat -> Nat)\n"
"(defn odd-len [n]"
" (natrec Nat (suc zero) (fn (k : Nat) (fn (r : Nat) (even-len k))) n))\n"
"(eval (even-len zero))\n"
"(eval (odd-len zero))")))
(check-true (>= (length results) 2))
(define last-two (list-tail results (- (length results) 2)))
;; even-len of zero = zero (the natrec base case fires)
(check-equal? (car last-two) "0N : Nat")
;; odd-len of zero = (suc zero) = 1N
(check-equal? (cadr last-two) "1N : Nat"))

;; ========================================
;; 3. Three-way mutual recursion: a -> b -> c -> a (forward cycle)
;; ========================================

(test-case "mutrec: three-way forward chain a -> b -> c"
;; a-fn forwards to b-fn forwards to c-fn (all spec'd).
;; Without the fix: a-fn fails on b-fn during elaboration.
(define results
(run (string-append
"(spec a-fn Nat -> Nat)\n"
"(defn a-fn [n] (b-fn n))\n"
"(spec b-fn Nat -> Nat)\n"
"(defn b-fn [n] (c-fn n))\n"
"(spec c-fn Nat -> Nat)\n"
"(defn c-fn [n] (suc n))\n"
"(eval (a-fn (suc zero)))")))
(check-equal? (length results) 4)
(check-equal? (cadddr results) "2N : Nat"))

;; ========================================
;; 4. Regression: simple self-recursive defn (no mutual)
;; ========================================

(test-case "mutrec regression: self-recursive defn (no mutual)"
;; Self-recursion was already supported via process-def's pre-registration.
;; Ensure the new pre-pass doesn't break it.
(define results
(run (string-append
"(spec my-add Nat Nat -> Nat)\n"
"(defn my-add [x y] (natrec Nat x (fn (k : Nat) (fn (r : Nat) (suc r))) y))\n"
"(eval (my-add (suc zero) (suc (suc zero))))")))
(check-equal? (length results) 2)
(check-equal? (cadr results) "3N : Nat"))

;; ========================================
;; 5. Forward reference WITHOUT a mutual cycle
;; (A uses B; B is defined later but doesn't use A)
;; Pre-fix this also failed (sequential env). Post-fix: works.
;; ========================================

(test-case "mutrec: simple forward reference (A uses B, B is non-recursive)"
(define results
(run (string-append
"(spec call-helper Nat -> Nat)\n"
"(defn call-helper [n] (helper n))\n"
"(spec helper Nat -> Nat)\n"
"(defn helper [n] (suc n))\n"
"(eval (call-helper (suc zero)))")))
(check-equal? (length results) 3)
(check-equal? (caddr results) "2N : Nat"))

;; ========================================
;; 6. Mutual recursion WITHOUT spec
;;
;; The pre-pass requires a declared type (from spec) to install in the
;; global env. Spec-less defns are skipped by the pre-pass.
;;
;; Surprise (validated 2026-04-25): Prologos's bare-param defn elaborates
;; with hole-typed parameters (`_ -> _`), and forward references to
;; spec-less defns DO succeed because the elaborator tolerates holes in
;; types. So spec-less mutual recursion happens to work too, by a
;; different mechanism than the pre-pass — both defns elaborate to opaque
;; `_ -> _` types and the cross-reference resolves through hole-as-meta
;; inference. We assert success here to lock in the observed behavior.
;; ========================================

(test-case "mutrec: spec-less mutual recursion (succeeds via hole inference)"
(define results
(run (string-append
"(defn no-spec-a [n] (no-spec-b n))\n"
"(defn no-spec-b [n] n)\n")))
;; Both defns should succeed (no errors).
(check-true (andmap (lambda (r) (not (prologos-error? r))) results)
(format "Expected all results to succeed, got: ~a" results))
(check-equal? (length results) 2))

;; ========================================
;; 7. Order-independence: each direction works the same regardless of order
;; ========================================

(test-case "mutrec: each direction works regardless of source order"
;; In order-1, p1 (caller) is declared first.
;; In order-2, q2 (callee) is declared first.
;; Both should succeed with the same answer.
(define order-1
(run (string-append
"(spec p1 Nat -> Nat)\n"
"(defn p1 [n] (p2 n))\n"
"(spec p2 Nat -> Nat)\n"
"(defn p2 [n] (suc n))\n"
"(eval (p1 zero))")))
(define order-2
(run (string-append
"(spec q2 Nat -> Nat)\n"
"(defn q2 [n] (suc n))\n"
"(spec q1 Nat -> Nat)\n"
"(defn q1 [n] (q2 n))\n"
"(eval (q1 zero))")))
(check-equal? (last order-1) "1N : Nat")
(check-equal? (last order-2) "1N : Nat"))
Loading