giles
6c3b7d1cf9
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 24s
First slice of Phase 3 (bidirectional type checker).
lib/go/types.sx defines:
* go-ctx-empty / go-ctx-extend / go-ctx-lookup — context as a value.
* go-ctx-extend-field — consumes the (:field NAMES TYPE) shape from
the parser, binding every name to the shared type. This is the
cross-deliverable validation of the :field binding-group
observation made during Phase 2 func decls: parser produces it,
type checker consumes it, same shape end-to-end.
* go-predeclared — true / false / nil baked in. Full list expanded
on demand.
* go-synth — currently handles variable lookup; literals / calls /
binops follow in subsequent iterations.
* go-check — v0 defers to synth + structural type equality. Untyped-
constant flow and assignment-compatibility relations land later.
* Type errors carry first-class tags (:unbound, :mismatch,
:unsupported-synth) so consumers and tooling can dispatch.
Conformance.sh wired with new types suite. Scoreboard cleanup: drop
the "pending" types row since the suite is now real.
types 12/12, total 317/317. Phase 3 underway.
Sister-plan static-types-bidirectional diary updated with the
synth/check shape: judgment skeleton, error tag structure, and the
proposal that `check` should accept a `subtype?` predicate parameter
so each consumer (Go untyped-constants, TS variance, Rust lifetimes)
plugs in its own variance discipline without rewriting the judgment.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
126 lines
3.9 KiB
Plaintext
126 lines
3.9 KiB
Plaintext
;; lib/go/types.sx — Go bidirectional type checker.
|
|
;;
|
|
;; Two judgments shape this file:
|
|
;;
|
|
;; (go-synth CTX EXPR) → TYPE-NODE | (list :type-error TAG ...)
|
|
;; Given a context and an expression, produce a type.
|
|
;;
|
|
;; (go-check CTX EXPR EXPECTED) → :ok | (list :type-error TAG ...)
|
|
;; Given a context, expression, and expected type, verify compatibility.
|
|
;;
|
|
;; The two judgments are mutually recursive. Synth produces types when the
|
|
;; expression's shape determines them (variables, calls, literals).
|
|
;; Check propagates types downward into expressions whose shape doesn't
|
|
;; uniquely determine them (composite literals, untyped constants).
|
|
;;
|
|
;; Type representations reuse the parser's :ty-* AST nodes from
|
|
;; lib/go/parse.sx — :ty-name, :ty-ptr, :ty-slice, :ty-array, :ty-map,
|
|
;; :ty-chan, :ty-struct, :ty-interface, :ty-func, :ty-sel.
|
|
;;
|
|
;; Context: an association list of (NAME TYPE) bindings. Per-block scope
|
|
;; via a fresh extension on entry.
|
|
;;
|
|
;; **Independent implementation.** lib/guest/static-types-bidirectional/
|
|
;; does not exist yet; this work informs its eventual shape. Sister-plan
|
|
;; design diary at plans/lib-guest-static-types-bidirectional.md tracks
|
|
;; the chiselling insights as Phase 3 progresses.
|
|
|
|
;; ── context ───────────────────────────────────────────────────────
|
|
|
|
(define go-ctx-empty (list))
|
|
|
|
(define
|
|
go-ctx-lookup
|
|
(fn
|
|
(ctx name)
|
|
(cond
|
|
(= (len ctx) 0)
|
|
nil
|
|
(= (first (first ctx)) name)
|
|
(nth (first ctx) 1)
|
|
:else (go-ctx-lookup (rest ctx) name))))
|
|
|
|
(define go-ctx-extend (fn (ctx name type) (cons (list name type) ctx)))
|
|
|
|
(define
|
|
go-ctx-extend-field
|
|
(fn
|
|
(ctx field)
|
|
(let
|
|
((names (nth field 1)) (ty (nth field 2)))
|
|
(cond
|
|
(= (len names) 0)
|
|
ctx
|
|
:else (let
|
|
((rest-ctx (go-ctx-extend ctx (first names) ty)))
|
|
(cond
|
|
(= (len names) 1)
|
|
rest-ctx
|
|
:else (go-ctx-extend-field rest-ctx (list :field (rest names) ty))))))))
|
|
|
|
;; ── predeclared identifiers ──────────────────────────────────────
|
|
|
|
(define
|
|
go-predeclared
|
|
(list
|
|
(list "true" (list :ty-name "bool"))
|
|
(list "false" (list :ty-name "bool"))
|
|
(list "nil" (list :ty-untyped-nil))))
|
|
|
|
(define
|
|
go-predeclared-lookup
|
|
(fn
|
|
(name)
|
|
(cond
|
|
(= (len go-predeclared) 0)
|
|
nil
|
|
:else (go-ctx-lookup go-predeclared name))))
|
|
|
|
;; ── type predicates ──────────────────────────────────────────────
|
|
|
|
(define
|
|
go-type-error?
|
|
(fn
|
|
(x)
|
|
(and
|
|
(list? x)
|
|
(not (= (len x) 0))
|
|
(= (first x) :type-error))))
|
|
|
|
(define go-type-equal? (fn (a b) (= a b)))
|
|
|
|
;; ── synth ────────────────────────────────────────────────────────
|
|
|
|
(define
|
|
go-synth
|
|
(fn
|
|
(ctx expr)
|
|
(cond
|
|
(and (list? expr) (= (first expr) :var))
|
|
(let
|
|
((name (nth expr 1)))
|
|
(let
|
|
((pre (go-predeclared-lookup name)))
|
|
(cond
|
|
(not (= pre nil))
|
|
pre
|
|
:else (let
|
|
((t (go-ctx-lookup ctx name)))
|
|
(cond (= t nil) (list :type-error :unbound name) :else t)))))
|
|
:else (list :type-error :unsupported-synth expr))))
|
|
|
|
;; ── check ────────────────────────────────────────────────────────
|
|
|
|
(define
|
|
go-check
|
|
(fn
|
|
(ctx expr expected)
|
|
(let
|
|
((got (go-synth ctx expr)))
|
|
(cond
|
|
(go-type-error? got)
|
|
got
|
|
(go-type-equal? got expected)
|
|
:ok :else
|
|
(list :type-error :mismatch expected got)))))
|