# lib/guest/static-types-bidirectional — design-diary plan Capture the dispatch skeleton of bidirectional type checking (synthesis/checking judgments, context as a value, pluggable subtyping and unification) as `lib/guest/static-types-bidirectional/`, so static-typed guest languages that aren't Hindley-Milner-inferred cost ~300 lines of language-specific rules instead of re-inventing the checker plumbing. Reference: `plans/lib-guest.md` (parent — two-language rule, stratification), `lib/guest/hm.sx` (sister module — full Hindley-Milner for inference-heavy languages like Haskell-on-SX), Go-on-SX (planned first consumer), TBD second consumer. **Branch:** `architecture`. SX files via `sx-tree` MCP only. ## Thesis `lib/guest/hm.sx` covers languages where the user writes few type annotations and the checker infers the rest globally (Haskell-on-SX, an eventual ML port, a typed-Scheme-with-Damas-Milner). But most modern statically-typed languages in actual production — Go, Rust, Swift, TypeScript, Kotlin, Scala 3, Hack — do **bidirectional checking instead**: declarations carry annotations, locals are inferred from immediate context, return types thread inwards from call sites. This isn't a weaker form of HM; it's a different design that scales better to mutation, subtyping, ad-hoc polymorphism, and gradual typing — none of which HM handles cleanly. If `lib/guest/` is going to credibly host the next decade of statically-typed languages, it needs a bidirectional kit alongside `hm.sx`. They're sisters, not rivals. **This plan is a design diary, not an implementation queue.** The two-language rule blocks extraction until two consumers exist. Go-on-SX is the first; the second is TBD. Until then, this plan documents what the API surface *should* be based on a single consumer, openly acknowledging that the second consumer will revise it. ## Current state (2026-05-26) - `lib/guest/hm.sx` exists, used by Haskell-on-SX. 180 lines. The HM kit is the sister extraction this plan complements. - No bidirectional kit anywhere in `lib/guest/`. - Go-on-SX does not exist yet. When it does, `lib/go/types.sx` will be the first consumer. - Second consumer is unidentified. Most likely candidates, in order: 1. **TypeScript-on-SX** — purely structural, gradual typing, the most- popular bidirectional language alive. Natural pair. 2. **Rust-on-SX** — bidirectional with substantial extras (lifetimes, traits, borrow checking). Heavyweight; lifetimes don't go in this kit. 3. **Typed Racket subset** — if anyone ports it. Bidirectional + gradual. 4. **Hack / Flow / Python-with-types** — same shape. **Status: Phase 0 (literature survey).** No code in this plan yet. ## Why bidirectional, not HM (for the languages that need it) Five reasons HM doesn't fit these languages: 1. **Subtyping.** HM unification requires equality of types; subtyping requires a different judgment (`t ⊑ u`). Go's `interface{}` accepts any concrete type that satisfies it — subtyping, not unification. 2. **Mutation.** HM's let-polymorphism interacts pathologically with mutable references (the value restriction). Go, Rust, TS all have first-class mutation and need rules that handle it directly. 3. **Annotations as ground truth.** Bidirectional treats declared types as *given*, then propagates them. HM treats every type as a variable to be solved. For languages where annotations are expected, bidirectional is the natural shape. 4. **Generics with constraints.** Go's type parameters carry constraints (`type T comparable`); Rust has trait bounds. HM has typeclasses but they're orthogonal to its constraint solver. Bidirectional weaves constraints into the checking rules naturally. 5. **Gradual typing.** TS's `any`, Hack's pessimistic mode, Python's `Any` — gradual checking is built on bidirectional's "check or skip" distinction. HM either checks or it doesn't. These languages collectively are the majority of new statically-typed code. Hosting them on lib/guest at all requires the bidirectional shape. ## API surface (proposed — design only, will revise with second consumer) ``` ;; --- judgments --- (synth ctx expr) -> {:type T} | {:error msg} ;; "expr synthesises type T in context ctx." ;; Used at function calls (arg types known), let bindings, literals. (check ctx expr expected-type) -> :ok | {:error msg} ;; "expr checks against expected-type in context ctx." ;; Used in function bodies (return type known), arguments (param type known), ;; assignments (LHS type known). ;; --- context --- (make-ctx) -> ctx (ctx-extend ctx name type) -> ctx ;; functional update (ctx-lookup ctx name) -> type | nil ;; --- pluggable rules --- (register-synth-rule! kit ast-tag synth-fn) -> nil ;; ast-tag: a keyword identifying the AST node shape (eg. :call :let :lit-int) ;; synth-fn: (ctx node) -> {:type T} | {:error msg} (register-check-rule! kit ast-tag check-fn) -> nil ;; check-fn: (ctx node expected-type) -> :ok | {:error msg} (register-type-equiv! kit pred) -> nil ;; pred: (t1 t2) -> bool. The "are these types compatible" predicate. ;; For Go: structural-interface-match-or-equal. ;; For TS: structural-equality-with-any-bidirectional-bottom. ;; For Rust: nominal equality + trait obligations. (register-subtype! kit pred) -> nil ;; pred: (sub super) -> bool. Optional; defaults to type-equiv. ;; Go has no subtyping between concrete types but interface satisfaction ;; is morally subtyping. TS has structural subtyping properly. (register-unify! kit unifier) -> nil ;; Optional; for type-variable resolution (generics). ;; unifier: (t1 t2 subst) -> {:subst s'} | {:error msg} ;; --- driver --- (make-kit) -> kit (check-program kit ctx program) -> {:ok ctx'} | {:error msg path-to-error} ``` Design notes: - **The kit dispatches on AST tags**, which is what makes it pluggable. Each language registers rules for its node types. There's no hardcoded set of expression shapes in the kit. - **Synth and check are mutually recursive.** Inside a synth-rule for `call`, the rule synthesises the function's type, then `check`s each argument against the corresponding parameter type. Inside a check-rule for `lambda`, the rule pulls argument types from the expected function type and `synth`s the body. This pingponging is the bidirectional core. - **Pluggable type-equiv + subtype + unify** is the three-knob shape. Pierce & Turner ("Local Type Inference") and Dunfield & Krishnaswami ("Sound and Complete Bidirectional Typechecking") both factor it this way. - **No type variables in the core API.** Generics handling is a kit *extension*: when a language registers a `unify` predicate, the kit threads a substitution through synth/check. Languages without generics (early Go) leave it null. - **Errors carry a path.** `{:error msg path}` where path is a list of AST tags leading to the failure. Good error messages are why bidirectional is practical; the kit must support them. ## What's NOT in the kit (language-layer concerns) Per the chiselling discipline, the kit is the dispatch skeleton; rules stay in the language. Specifically: - **The literal type table.** Go's `42` is `untyped int` until contextualised; TS's `42` is the literal type `42`. Each language ships its own. - **Specific subtyping rules.** Go's interface satisfaction is recursive structural matching against method sets. TS's depends on object property satisfaction. Each language ships its own predicate. - **Generics constraint solving.** Go's type-set-based constraints, Rust's trait bounds, TS's conditional types — each is non-trivial and language- specific. The kit threads a substitution; the language defines what's in it. - **Effects, lifetimes, ownership.** Rust's borrow checker is not a type checker in the bidirectional-kit sense — it's a separate dataflow pass. Out of scope. - **Gradual fallback.** TS's `any` lets unchecked code coexist with checked code. The kit supports this via "check returns :ok on a sentinel any-type" but the sentinel is registered by the language. ## Build order — phases ### Phase 0 — Literature survey + Go's type system specifics ⬜ - Read: Pierce & Turner "Local Type Inference" (2000); Dunfield & Krishnaswami "Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism" (2013, 2019 revision); the Go language spec § "Types" + "Expressions". - Survey how Rust / TS / Kotlin / Scala 3 implement bidirectional in practice (their compilers are open source). Note where they diverge. - Output: a short summary section "Bidirectional design space (captured 2026-MM-DD)" appended to this plan. Specifically: list every place language implementations diverge, so we can predict which divergences will show up between Go and the second consumer. - **Acceptance:** survey committed to this plan. No code. ### Phase 1 — Go independent implementation ⬜ - During Go-on-SX, implement `lib/go/types.sx` from scratch. Do not write with extraction in mind — write the simplest Go-specific bidirectional checker. - Hit Go's distinctive type-system features: untyped constants, interface satisfaction (structural), generics (Go 1.18 type parameters with type-set constraints — defer this if scope explodes). - Pass Go's type-checker conformance tests. - **Acceptance:** Go conformance scoreboard includes type-checker tests, all passing. - **Output:** one consumer. Two-language rule still not met; no extraction. ### Phase 2 — Pick + start the second consumer ⬜ - Decide between TS, Rust-subset, or typed-Scheme-subset. Recommendation: **TypeScript** — most-different from Go (gradual, structural everywhere), testing the kit's range maximally. Rust's lifetime/borrow machinery isn't part of this kit, so a Rust port wouldn't actually exercise the kit very hard. - Implement just enough of the second language to type-check a non-trivial function. Don't port the whole language; port the type checker. - **Acceptance:** second consumer's type checker green on its small slice. ### Phase 3 — Diff and proposed kit ⬜ - Side-by-side: Go's checker vs the second consumer's checker. Where do they agree (the kit). Where does each diverge (the language). - Draft `lib/guest/static-types-bidirectional/api.sx` (signatures only). - Compare against the API sketch in this plan. The API WILL change at this step; that's the whole point of having two consumers. - **Acceptance:** revised API committed to this plan; agreement that both consumers can adopt it. ### Phase 4 — Implement the kit ⬜ - `lib/guest/static-types-bidirectional/` with the agreed API. Kit tests in `lib/guest/static-types-bidirectional/tests/` — using a minimal "toy" language (synth-rule for `:int`, check-rule for `:lambda`) to verify the dispatch skeleton works. - **Acceptance:** kit tests pass; both consumers' scoreboards still green with their own implementations. ### Phase 5 — Refactor both consumers to use the kit ⬜ - Go: `lib/go/types.sx` becomes a thin layer over the kit — registers Go's synth/check/equiv rules, calls `check-program`. Lifecycle code shrinks. - Second consumer: same exercise. - **No-regression gate:** both consumers' conformance scoreboards unchanged. - **Acceptance:** both `lib//types.sx` files meaningfully smaller; kit is doing real work. ### Phase 6 — Documentation + chiselling diary ⬜ - Document the API in lib/guest's README index. - Diary section in this plan: what we considered putting in the kit but ended up keeping language-specific, and why. - **Acceptance:** documentation present; diary captured. ## Two-language rule — gating Same as `lib-guest-scheduler.md`. The kit does not exist until both consumers independently work AND we've reviewed the diff AND we believe the shared skeleton is real. Rejected-extraction is a valid outcome. ## Relationship to `lib/guest/hm.sx` Sister modules, not rivals. Some languages will use HM (full inference, let-polymorphism); some will use bidirectional (annotation-driven, subtyping- friendly). Some might use both — Scala-on-SX, hypothetically, has local-type- inference in expressions and global-HM-style constraint solving in implicit resolution. The kit boundaries are: - `hm.sx` — unification-based, whole-expression inference. Damas-Milner core. Best for: ML family, Haskell, OCaml subset, Standard ML. - `static-types-bidirectional/` — synth/check judgments, pluggable equiv + subtype. Best for: Go, Rust, TS, Kotlin, Swift, Scala 3, Hack. A language can call into both: bidirectional for the surface, HM-style unification inside generics resolution. That's actually how Scala 3 works. The kits compose; design accordingly. ## Open questions - **Variance.** Go has none; TS has covariant/contravariant/bivariant; Rust has variance markers per type parameter. Does the kit need a variance predicate as a fourth pluggable knob? Probably yes, but defer until the second consumer forces the question. - **Effect tracking.** Some bidirectional checkers (Koka, Eff, certain capability-effect TS variants) track effects in types. Out of scope for v1; the kit must not actively prevent it though. - **Refinement types.** TS has narrowing (`typeof x === "string"` refines `x` to `string`); Hack and Flow are similar. These layer above the kit (the kit's `check` returns a refined context as part of `:ok`). Sketch this in Phase 3 if TS is the second consumer. - **Error recovery.** Real-world type checkers don't halt on first error; they recover and continue to surface as many errors as possible. The kit needs an error-accumulation mode. Design it in Phase 4. - **Performance.** For toy languages, naive synth/check is fine. For Go- sized programs, the checker has to be memoised on synthesised types of subexpressions. Not a v1 concern; flag if it bites. ## Progress log _Newest first. Append one dated entry per milestone landed._ - 2026-05-27 — Follow-up from Phase 3 scaffold: **assignability** has landed as a separate relation from structural equality. Go's untyped-constant flow (`var x float64 = 42 / 7` — 42/7 stays untyped int, then converts to float64) is one instance of a broader pattern: the value's "natural" type isn't quite the slot's type, but they're compatible under a per-language relation. **Design insight for the kit**: `check` should *not* call `equal?` on the synthesised vs expected types. It should call a pluggable `assignable?` predicate that each consumer supplies: ``` (check CTX EXPR EXPECTED) → let GOT = (synth CTX EXPR) if (assignable? GOT EXPECTED) :ok else (:mismatch EXPECTED GOT) ``` Go's `assignable?` handles untyped constants → numeric-type conversion. TS would supply structural subtyping (`{a: number, b: string}` assignable to `{a: number}`). Rust supplies lifetime-aware type identity with implicit `&T -> &U` where `T: Deref`. None of the consumers need to rewrite synth or the judgment skeleton — only swap in their variance discipline. Concretely the kit interface looks like: ``` (check-with assignable? CTX EXPR EXPECTED) — kit primitive ``` Source: Go-on-SX commit landing `go-type-assignable?` in `lib/go/types.sx`. - 2026-05-27 — From Go-on-SX Phase 3 scaffold (`lib/go/types.sx` first cut): the **independent synth/check shape** has landed. Two judgments, both consuming a context-as-value: ``` (go-synth CTX EXPR) → TYPE-NODE | (:type-error TAG ...) (go-check CTX EXPR EXPECTED) → :ok | (:type-error TAG ...) ``` Context is an association list of `(NAME TYPE)` bindings; the load-bearing extension primitive is `go-ctx-extend-field` which takes a `(:field NAMES TYPE)` binding-group node and binds every NAME to TYPE. This validates the earlier cross-deliverable observation: the parser produces `:field` once, the type checker consumes it once, same shape across struct fields / func params / var-decls. **Design insight for the kit**: the synth/check pair is the canonical judgment skeleton. `check` deferring to `synth + structural-equality` is the v0 default that every consumer overrides for subtype-ish relationships. The kit's `check` should accept a `subtype?` predicate parameter so Go (untyped-constant flow), TS (variance), and Rust (lifetime subtyping) each plug in their own variance discipline without rewriting the whole judgment. The kit's `synth` stays uniform. Error shape `(:type-error TAG ...)` with first-class tags (`:unbound`, `:mismatch`, `:unsupported-synth`) gives consumers and IDE tooling structured errors to dispatch on. Untyped-constant flow and binop-synth — the canonical Go pitfall (`var x float64 = 42 / 7`) — arrive next. Source: Go-on-SX commit landing `lib/go/types.sx`. - 2026-05-27 — From Go-on-SX Phase 2 (func decls landing): parser-side observation that's load-bearing for any bidirectional checker. Go's parser ended up with a single shape — `(list :field NAMES TYPE)` — that recurs in five contexts: struct fields, var decls, const decls, func params, and method receivers. Each represents "these names are bound to this type" — exactly the input shape `check` would consume to seed the context with typed bindings. **Design insight**: the canonical bidirectional checker should accept `:field`-shaped AST nodes uniformly across these contexts rather than each context defining a bespoke shape. The kit's `check Γ e T` judgment can dispatch on the enclosing form (struct vs var vs func-param vs ...) but the local per-binding shape stays identical. This is what statically-typed guest #2 should also produce — if it does, the kit can ship a `field-bindings → context-extension` helper that all consumers reuse. Cross-ref Go-on-SX plan's Blockers entry on `ast-binding-group` for the parallel AST-kit proposal that supports this. Source: Go-on-SX commit `parse.sx — func declarations`. - 2026-05-26 — Plan drafted as design diary. Phase 0 unstarted. Gated on Go-on-SX (first consumer) and a TBD second consumer (recommendation: TypeScript). No code yet — kit cannot exist before two consumers do.