rose-ash/plans/lib-guest-static-types-bidirectional.md

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 checks each argument against the corresponding parameter type. Inside a check-rule for lambda, the rule pulls argument types from the expected function type and synths 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/<lang>/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-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.