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-28 — From Go-on-SX Phase 8 first slice — value-type kinds confirm the "kind-tag + payload" shape as cross-runtime primitive. When the stdlib landed, packages joined the existing registry of value-type kinds:

  • (:go-struct TY-NAME FIELDS) — composite by-field state
  • (:go-slice ELEMS) — sequential by-position state
  • (:go-map ENTRIES) — keyed state
  • (:go-chan ACCESSORS) — closure-bundle (channel)
  • (:go-fn PARAMS BODY) — user function value
  • (:go-method RECV PARAMS BODY) — method value
  • (:go-builtin NAME) — name-dispatched builtin
  • (:go-builtin-fn FN) — closure-dispatched builtin (NEW)
  • (:go-package NAME ENTRIES) — namespace value (NEW)
  • (:go-panic V) — unwinding-control value
  • (:go-defer CALLEE ARGS) — frame-cleanup record

  All eleven kinds use the same (:KIND-TAG PAYLOAD...) shape. None of them are AST nodes (those are :func-decl, :literal, etc.); they're VALUES the evaluator produces. The orthogonal axes the kit should care about:

  1. AST nodes (parser output, evaluator input)
  2. Value-type kinds (evaluator output, predicate input)
  3. Sentinel signals (control-flow: return/break/panic/etc.)

  All three subscribe to the same first-class-tag discipline: (first x) answers "what kind is this?" and the rest is payload. The kit's kind? and kind-of predicates work uniformly across all three axes.

  For the bidirectional checker specifically, this means the assignable?(got, expected) predicate isn't special — it's just one predicate that operates on value-type kinds. The synth / check skeleton processes AST nodes; the validators it calls operate on value-type kinds. Clean separation: AST is what you parse, value-types are what you check, sentinels are what you propagate. None of them bleed into each other.

  Phase 7's index-synth and Phase 8's package-lookup both fit the same template: AST kind triggers a synth/lookup, returning a value-type kind. The validator-table dispatch from earlier diary entries is the right abstraction; the kit should expose it as a PROTOCOL (Go would phrase this as an interface, Haskell as a typeclass) so all three axes can be extended without modifying the kit.

• 2026-05-28 — From Go-on-SX Phase 7 closing — the "shape is the parser, role is the validator" lemma. After landing canonical generic Map/Filter/Reduce/First plus 25+ typer tests, a clear pattern has emerged across THREE distinct deliverables of the Go-on-SX loop:

  1. Binding-groups (struct fields / var-decls / params / receivers / type-params): SAME parser, SAME (:field NAMES TY) shape, 5 different validators based on what role TY plays.

  2. Control-flow sentinels (return-value / break / continue / eval-error / go-panic): SAME (go-panic? r)-style dispatch at 4+ AST control-flow sites, each calling the same predicate list — would collapse to a single propagates? helper.

  3. Index synthesis (xs[0] for slice / array / map): SAME (:index OBJ IDX) AST, 3 element-type extraction rules dispatching on OBJ's type. The validator differs per role, but the parser shape is one.

  The recurring lemma: the kit's primary primitive is shape recognition (parser + AST); the kit's secondary primitive is a role-validator dispatch table. Consumers (Go, Erlang, future guests) plug their semantics into the role table; they never need to define new shapes for things that already match an existing AST.

  Architectural payoff: at extraction time, the kit's API should expose:

  • parse-XXX → AST shape (one per shape)
  • validate-AST(role, ctx) → either ctx or error (one per role)
  • dispatch-table(role) → which-validator-fires-for-this-AST

  Reuse across guest evaluators happens automatically because the shape is shared. New guests only register new role handlers; they don't extend the parser.

  Concretely for the bidirectional checker: the synth/check skeleton is the shape; assignable? and constraint-satisfies? are roles. Adding a new language means adding a row to the role table, not a column to the AST.

• 2026-05-28 — From Go-on-SX Phase 7 foundation — the field binding-group is a cross-deliverable shape, confirmed by its 6th consumer (type-parameter lists). Previously documented uses: struct fields, var-decls, const-decls, func params, method receivers. Now type-parameters re-use the EXACT same parser (gp-parse-decl-param-group) and the same (list :field NAMES TY) shape — only the meaning of TY differs (it's a constraint type, not a value type).

  This is the strongest evidence yet that the kit's primary shape should be a generic binding-group<TyKind> parametric over the role TY plays. Five roles emerge:

  1. value-typing (struct fields, var-decls, params, receivers): TY is the type of values that bind to NAMES.
  2. value-pinning (const-decls): TY is the type of compile- time-known values.
  3. constraint-binding (type-parameter lists): TY is a constraint that the type-variables NAMES must satisfy.
  4. kind-binding (anticipated for higher-kinded types): TY would be a kind that type-constructors NAMES inhabit.
  5. trait-binding (anticipated for Rust-style impl blocks): TY would be the trait the implementations NAMES provide.

  All five share parser + AST shape; they differ in (a) which predicate validates the relationship between NAMES and TY, and (b) what scope NAMES are visible in. The kit should expose a single parse-binding-group consumer and let each role plug in its own validator. This is the same lesson the assignable? + constraint-satisfies? pluggable-predicate work surfaced — kit primitives are SHAPES, validators are PLUGINS.

  Concretely: when the kit extracts, the bidirectional checker exposes extend-ctx-with-binding-group(role, group) where role selects the validator. Go's type-params bind via role= "constraint-binding"; struct fields bind via "value-typing". Erlang's pattern bindings will bind via something else again.

• 2026-05-27 — From Go-on-SX Phase 3 — interface satisfaction is the third pluggable predicate the kit should ship, alongside assignable? and the synth/check skeleton. Go's structural-and-silent satisfaction is one instance; Haskell's typeclass dictionary resolution, Rust's trait impl lookup, and TS's structural subtyping are others — all answer the same question with different machinery: "does this value-type fit this constraint-type?"

  Kit proposal:

  (constraint-satisfies? CTX VALUE-TY CONSTRAINT-TY) → bool
  

  Different consumers plug in different implementations:

  • Go: walk interface methods, lookup #method/T/NAME.
  • Haskell: typeclass instance resolution (with global instance table).
  • Rust: trait impl lookup with where-clause bound check.
  • TS: structural subtyping with property-by-property comparison.

  The judgment skeleton uses it during check when the expected type is itself an interface/constraint:

  check Γ e EXPECTED →
    if EXPECTED is a constraint type:
      let GOT = synth Γ e
      if constraint-satisfies? Γ GOT EXPECTED then :ok else mismatch
    else: use the assignable? path
  

  Source: Go-on-SX commit landing go-iface-satisfies? in lib/go/types.sx with the #method/T/NAME mangled-key storage scheme.

• 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<U>. 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.