go: types.sx — interface satisfaction (structural method-set check) + 7 tests [shapes-static-types-bidirectional]
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 23s
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 23s
Phase 3 cont. The headline Go-distinguishing typing feature: interfaces
are satisfied *structurally and silently* — no `implements` declaration,
no nominal subtyping. Any type whose method set contains all the
interface's methods (with matching signatures) satisfies it.
Method declarations now type-check via go-check-method-decl:
* Receiver type extracted (T or *T → "T") via go-extract-recv-ty-name.
* Method signature (:ty-func PARAMS RESULTS) bound under a mangled
key "#method/RECV-NAME/METHOD-NAME" in ctx.
* Body checked with receiver + params extended into the body ctx.
go-iface-satisfies? CTX TY-NAME IFACE-TYPE walks the interface's
:method elements; for each, looks up #method/TY-NAME/METHOD-NAME and
compares (PARAMS, RESULTS) tuples. Embedded interfaces (:embed
elements) skipped in v0 — recursive interface resolution later.
Tests:
* method-decl binds under #method/Point/String
* pointer-receiver method also keys the base type
* Point with String() satisfies interface { String() string }
* empty type does NOT satisfy Stringer
* arity-mismatch method fails satisfaction
* multi-method satisfaction works
* partial method-set fails
types 72/72, total 377/377. Phase 3 sub-deliverable list is now
substantially complete; only AST-path error context remains as a UX
sharpener.
Sister-plan static-types-bidirectional diary updated with the
**constraint-satisfies? pluggable predicate** kit-API proposal —
third pluggable point after synth/check + assignable?. Go interfaces,
Haskell typeclasses, Rust traits, and TS structural subtyping all
answer "does this value-type fit this constraint-type?" with
different machinery; the kit's check uses constraint-satisfies? when
EXPECTED is itself a constraint type.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This commit is contained in:
@@ -1,11 +1,11 @@
|
||||
{
|
||||
"language": "go",
|
||||
"total_pass": 370,
|
||||
"total": 370,
|
||||
"total_pass": 377,
|
||||
"total": 377,
|
||||
"suites": [
|
||||
{"name":"lex","pass":129,"total":129,"status":"ok"},
|
||||
{"name":"parse","pass":176,"total":176,"status":"ok"},
|
||||
{"name":"types","pass":65,"total":65,"status":"ok"},
|
||||
{"name":"types","pass":72,"total":72,"status":"ok"},
|
||||
{"name":"eval","pass":0,"total":0,"status":"pending"},
|
||||
{"name":"runtime","pass":0,"total":0,"status":"pending"},
|
||||
{"name":"stdlib","pass":0,"total":0,"status":"pending"},
|
||||
|
||||
@@ -1,12 +1,12 @@
|
||||
# Go-on-SX Scoreboard
|
||||
|
||||
**Total: 370 / 370 tests passing**
|
||||
**Total: 377 / 377 tests passing**
|
||||
|
||||
| | Suite | Pass | Total |
|
||||
|---|---|---|---|
|
||||
| ✅ | lex | 129 | 129 |
|
||||
| ✅ | parse | 176 | 176 |
|
||||
| ✅ | types | 65 | 65 |
|
||||
| ✅ | types | 72 | 72 |
|
||||
| ⬜ | eval | 0 | 0 |
|
||||
| ⬜ | runtime | 0 | 0 |
|
||||
| ⬜ | stdlib | 0 | 0 |
|
||||
|
||||
@@ -476,6 +476,93 @@
|
||||
"x")
|
||||
(list :ty-slice (list :ty-name "int")))
|
||||
|
||||
(go-types-test
|
||||
"method: decl binds method-key"
|
||||
(go-ctx-lookup
|
||||
(go-check-decl
|
||||
go-ctx-empty
|
||||
(go-parse "func (p Point) String() string { return \"p\" }"))
|
||||
"#method/Point/String")
|
||||
(list :ty-func (list) (list (list :ty-name "string"))))
|
||||
|
||||
(go-types-test
|
||||
"method: pointer receiver also keyed by base type"
|
||||
(go-ctx-lookup
|
||||
(go-check-decl
|
||||
go-ctx-empty
|
||||
(go-parse "func (p *Point) String() string { return \"p\" }"))
|
||||
"#method/Point/String")
|
||||
(list :ty-func (list) (list (list :ty-name "string"))))
|
||||
|
||||
(go-types-test
|
||||
"iface: Point satisfies Stringer (structural)"
|
||||
(let
|
||||
((ctx (go-check-decl go-ctx-empty (go-parse "func (p Point) String() string { return \"p\" }"))))
|
||||
(go-iface-satisfies?
|
||||
ctx
|
||||
"Point"
|
||||
(list
|
||||
:ty-interface (list
|
||||
(list :method "String" (list) (list (list :ty-name "string")))))))
|
||||
true)
|
||||
|
||||
(go-types-test
|
||||
"iface: empty type does NOT satisfy Stringer"
|
||||
(go-iface-satisfies?
|
||||
go-ctx-empty
|
||||
"Empty"
|
||||
(list
|
||||
:ty-interface (list (list :method "String" (list) (list (list :ty-name "string"))))))
|
||||
false)
|
||||
|
||||
(go-types-test
|
||||
"iface: type with wrong-arity method fails"
|
||||
(let
|
||||
((ctx (go-check-decl go-ctx-empty (go-parse "func (p Point) String(x int) string { return \"p\" }"))))
|
||||
(go-iface-satisfies?
|
||||
ctx
|
||||
"Point"
|
||||
(list
|
||||
:ty-interface (list
|
||||
(list :method "String" (list) (list (list :ty-name "string")))))))
|
||||
false)
|
||||
|
||||
(go-types-test
|
||||
"iface: multi-method satisfaction (signature-only methods)"
|
||||
(let
|
||||
((ctx
|
||||
(go-check-decl
|
||||
(go-check-decl go-ctx-empty
|
||||
(go-parse "func (r Reader) Read(b []byte) int"))
|
||||
(go-parse "func (r Reader) Close() bool"))))
|
||||
(go-iface-satisfies?
|
||||
ctx
|
||||
"Reader"
|
||||
(list
|
||||
:ty-interface (list
|
||||
(list :method "Read"
|
||||
(list (list :ty-slice (list :ty-name "byte")))
|
||||
(list (list :ty-name "int")))
|
||||
(list :method "Close" (list)
|
||||
(list (list :ty-name "bool")))))))
|
||||
true)
|
||||
|
||||
(go-types-test
|
||||
"iface: partial method set fails (missing one method)"
|
||||
(let
|
||||
((ctx (go-check-decl go-ctx-empty (go-parse "func (r Reader) Read(b []byte) int { return 0 }"))))
|
||||
(go-iface-satisfies?
|
||||
ctx
|
||||
"Reader"
|
||||
(list
|
||||
:ty-interface (list
|
||||
(list
|
||||
:method "Read"
|
||||
(list (list :ty-slice (list :ty-name "byte")))
|
||||
(list (list :ty-name "int")))
|
||||
(list :method "Close" (list) (list (list :ty-name "error")))))))
|
||||
false)
|
||||
|
||||
(define
|
||||
go-types-test-summary
|
||||
(str "types " go-types-test-pass "/" go-types-test-count))
|
||||
|
||||
@@ -531,8 +531,103 @@
|
||||
(go-ctx-extend ctx name ty))
|
||||
(and (list? decl) (= (first decl) :func-decl))
|
||||
(go-check-func-decl ctx decl)
|
||||
(and (list? decl) (= (first decl) :method-decl))
|
||||
(go-check-method-decl ctx decl)
|
||||
:else ctx)))
|
||||
|
||||
;; ── method declarations and interface satisfaction ──────────────
|
||||
;; Methods are recorded in CTX under a mangled key
|
||||
;; "#method/RECV-TYPE-NAME/METHOD-NAME"
|
||||
;; bound to the method's :ty-func signature. Interface satisfaction is
|
||||
;; a structural lookup over these keys (Go spec § Interface types:
|
||||
;; "anything with the matching method set satisfies the interface").
|
||||
|
||||
(define
|
||||
go-method-key
|
||||
(fn (recv-ty-name method-name)
|
||||
(str "#method/" recv-ty-name "/" method-name)))
|
||||
|
||||
(define
|
||||
go-extract-recv-ty-name
|
||||
;; Receiver type is T or *T; return the named type's name string.
|
||||
(fn (recv-ty)
|
||||
(cond
|
||||
(and (list? recv-ty) (= (first recv-ty) :ty-name))
|
||||
(nth recv-ty 1)
|
||||
(and (list? recv-ty) (= (first recv-ty) :ty-ptr))
|
||||
(go-extract-recv-ty-name (nth recv-ty 1))
|
||||
:else nil)))
|
||||
|
||||
(define
|
||||
go-check-method-decl
|
||||
;; (list :method-decl RECV NAME PARAMS RESULTS BODY)
|
||||
;; Binds the method under the mangled key, then checks body with
|
||||
;; receiver + params extended.
|
||||
(fn (ctx decl)
|
||||
(let ((recv (nth decl 1)) (name (nth decl 2))
|
||||
(params (nth decl 3)) (results (nth decl 4))
|
||||
(body (nth decl 5)))
|
||||
(let ((recv-ty (nth recv 2)))
|
||||
(let ((recv-name (go-extract-recv-ty-name recv-ty)))
|
||||
(let ((sig (list :ty-func
|
||||
(go-decl-params-to-ty-list params) results)))
|
||||
(let ((ctx2
|
||||
(cond
|
||||
(= recv-name nil) ctx
|
||||
:else
|
||||
(go-ctx-extend ctx
|
||||
(go-method-key recv-name name) sig))))
|
||||
(cond
|
||||
(= body nil) ctx2
|
||||
(and (list? body) (= (first body) :block))
|
||||
(let ((body-ctx
|
||||
(go-extend-with-params
|
||||
(go-ctx-extend-field ctx2 recv) params)))
|
||||
(let ((err
|
||||
(go-check-block body-ctx
|
||||
(nth body 1) results)))
|
||||
(cond
|
||||
(go-type-error? err) err
|
||||
:else ctx2)))
|
||||
:else ctx2))))))))
|
||||
|
||||
(define
|
||||
go-iface-elems-satisfied?
|
||||
;; Each :method element in ELEMS must have a matching method in CTX
|
||||
;; under #method/TY-NAME/M-NAME. :embed elements are skipped in v0
|
||||
;; (they'd need recursive interface resolution).
|
||||
(fn (ctx ty-name elems)
|
||||
(cond
|
||||
(= (len elems) 0) true
|
||||
:else
|
||||
(let ((e (first elems)))
|
||||
(cond
|
||||
(= (first e) :method)
|
||||
(let ((m-name (nth e 1)) (m-params (nth e 2))
|
||||
(m-results (nth e 3)))
|
||||
(let ((found (go-ctx-lookup ctx
|
||||
(go-method-key ty-name m-name))))
|
||||
(cond
|
||||
(= found nil) false
|
||||
(and (= (nth found 1) m-params)
|
||||
(= (nth found 2) m-results))
|
||||
(go-iface-elems-satisfied? ctx ty-name (rest elems))
|
||||
:else false)))
|
||||
(= (first e) :embed)
|
||||
(go-iface-elems-satisfied? ctx ty-name (rest elems))
|
||||
:else
|
||||
(go-iface-elems-satisfied? ctx ty-name (rest elems)))))))
|
||||
|
||||
(define
|
||||
go-iface-satisfies?
|
||||
;; Does the type named TY-NAME satisfy the interface IFACE-TYPE
|
||||
;; under context CTX? Structural method-set match per Go spec.
|
||||
(fn (ctx ty-name iface-type)
|
||||
(cond
|
||||
(not (and (list? iface-type) (= (first iface-type) :ty-interface)))
|
||||
false
|
||||
:else (go-iface-elems-satisfied? ctx ty-name (nth iface-type 1)))))
|
||||
|
||||
;; ── function-decl checking ──────────────────────────────────────
|
||||
|
||||
(define
|
||||
|
||||
@@ -250,13 +250,17 @@ Progress-log line → push `origin/loops/go`.
|
||||
index-keyed shorthand). Nested composite literals work
|
||||
(`[][]int{[]int{1,2}, []int{3,4}}`). Named-type composite
|
||||
literals (`Point{...}`) need type-decl resolution; deferred.
|
||||
- [ ] Interface satisfaction (structural match against method sets).
|
||||
- [x] Interface satisfaction (structural match against method sets).
|
||||
Method decls bind under `#method/TYPE/NAME` keys (works for both
|
||||
value and pointer receivers). `go-iface-satisfies?` walks an
|
||||
interface's `:method` elements and looks each up; partial sets
|
||||
and arity-mismatches fail. Embedded interfaces deferred.
|
||||
- [ ] Short variable declaration `:=` (synth RHS into LHS bindings).
|
||||
- Defer: generics (Phase 7), full conversion rules, type assertions,
|
||||
type switches.
|
||||
- **Acceptance:** types/ suite at 60+ tests. **Bar crossed: 65/65.**
|
||||
Remaining sub-items (interface satisfaction, error reporting carrying
|
||||
AST paths) refine but don't gate Phase 4. Chisel note
|
||||
- **Acceptance:** types/ suite at 60+ tests. **Bar crossed: 72/72.**
|
||||
Remaining sub-item (error reporting carrying AST paths) sharpens UX
|
||||
but doesn't gate Phase 4. Chisel note
|
||||
`shapes-static-types-bidirectional` — sister-plan design diary is the
|
||||
cross-language record.
|
||||
|
||||
@@ -557,6 +561,20 @@ Minimal repro: see `lib/go/lex.sx#gl-oct-digit?` and `#gl-match-op`.
|
||||
|
||||
_Newest first. Append one dated entry per commit._
|
||||
|
||||
- 2026-05-27 — Phase 3 cont.: **interface satisfaction** — the headline
|
||||
Go-distinguishing typing feature this loop set out to validate.
|
||||
Method decls record under `#method/TYPE-NAME/METHOD-NAME` keys in
|
||||
ctx (value-receiver and pointer-receiver both key the base type).
|
||||
`go-iface-satisfies? CTX TY-NAME IFACE-TYPE` walks the interface's
|
||||
`:method` elements and verifies each one is present with a matching
|
||||
(PARAMS, RESULTS) signature. Embedded interfaces in iface elements
|
||||
are silently skipped in v0 (recursive interface resolution comes
|
||||
later). Partial method sets and arity mismatches correctly return
|
||||
false. types 72/72, total 377/377. `[shapes-static-types-
|
||||
bidirectional]` — sister-plan diary updated with the structural-
|
||||
satisfaction primitive the kit should ship.
|
||||
|
||||
Sister-plan diary update follows.
|
||||
- 2026-05-27 — Phase 3 cont.: composite-literal element checking.
|
||||
`go-synth-composite` dispatches on the literal's type expression:
|
||||
`:ty-slice` and `:ty-array` check each element assignable to the
|
||||
|
||||
@@ -282,6 +282,40 @@ The kits compose; design accordingly.
|
||||
|
||||
_Newest first. Append one dated entry per milestone landed._
|
||||
|
||||
- 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
|
||||
|
||||
Reference in New Issue
Block a user