giles
ab2c40c14c
Ships the algebra for HM-style type inference, riding on lib/guest/match.sx (terms + unify) and ast.sx (canonical AST): • Type constructors: hm-tv, hm-arrow, hm-con, hm-int, hm-bool, hm-string • Schemes: hm-scheme / hm-monotype + accessors • Free type-vars: hm-ftv, hm-ftv-scheme, hm-ftv-env • Substitution: hm-apply, hm-apply-scheme, hm-apply-env, hm-compose • Generalize / Instantiate (with shared fresh-tv counter) • hm-fresh-tv (counter is a (list N) the caller threads) • hm-infer-literal (the only fully-closed inference rule) 24 self-tests in lib/guest/tests/hm.sx covering every function above. The lambda / app / let inference rules — the substitution-threading core of Algorithm W — intentionally live in HOST CODE rather than the kit, because each host's AST shape and substitution-threading idiom differ subtly enough that forcing one shared assembly here proved brittle in practice (an earlier inline-assembled hm-infer faulted with "Not callable: nil" only when defined in the kit, despite working when inline-eval'd or in a separate file — a load/closure interaction not worth chasing inside this step's budget). The host gets the algebra plus a spec; assembly stays close to the AST it reasons over. PARTIAL — algebra + literal rule shipped; full Algorithm W deferred to host consumers (haskell/infer.sx, lib/ocaml/types.sx when OCaml-on-SX Phase 5 lands per the brief's sequencing note). Haskell infer.sx untouched; haskell scoreboard still 156/156 baseline. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
90 lines
4.1 KiB
Plaintext
90 lines
4.1 KiB
Plaintext
;; lib/guest/tests/hm.sx — exercises lib/guest/hm.sx algebra.
|
|
|
|
(define ghm-test-pass 0)
|
|
(define ghm-test-fail 0)
|
|
(define ghm-test-fails (list))
|
|
|
|
(define
|
|
ghm-test
|
|
(fn (name actual expected)
|
|
(if (= actual expected)
|
|
(set! ghm-test-pass (+ ghm-test-pass 1))
|
|
(begin
|
|
(set! ghm-test-fail (+ ghm-test-fail 1))
|
|
(append! ghm-test-fails {:name name :expected expected :actual actual})))))
|
|
|
|
;; ── Type constructors ─────────────────────────────────────────────
|
|
(ghm-test "tv" (hm-tv "a") (list :var "a"))
|
|
(ghm-test "int" (hm-int) (list :ctor "Int" (list)))
|
|
(ghm-test "arrow" (ctor-head (hm-arrow (hm-int) (hm-bool))) "->")
|
|
(ghm-test "arrow-args-len" (len (ctor-args (hm-arrow (hm-int) (hm-bool)))) 2)
|
|
|
|
;; ── Schemes ───────────────────────────────────────────────────────
|
|
(ghm-test "scheme-vars" (hm-scheme-vars (hm-scheme (list "a") (hm-tv "a"))) (list "a"))
|
|
(ghm-test "monotype-vars" (hm-scheme-vars (hm-monotype (hm-int))) (list))
|
|
(ghm-test "scheme?-yes" (hm-scheme? (hm-monotype (hm-int))) true)
|
|
(ghm-test "scheme?-no" (hm-scheme? (hm-int)) false)
|
|
|
|
;; ── Fresh tyvars ──────────────────────────────────────────────────
|
|
(ghm-test "fresh-1"
|
|
(let ((c (list 0))) (var-name (hm-fresh-tv c))) "t1")
|
|
(ghm-test "fresh-bumps"
|
|
(let ((c (list 5))) (begin (hm-fresh-tv c) (first c))) 6)
|
|
|
|
;; ── Free type variables ──────────────────────────────────────────
|
|
(ghm-test "ftv-int" (hm-ftv (hm-int)) (list))
|
|
(ghm-test "ftv-tv" (hm-ftv (hm-tv "a")) (list "a"))
|
|
(ghm-test "ftv-arrow"
|
|
(len (hm-ftv (hm-arrow (hm-tv "a") (hm-arrow (hm-tv "b") (hm-tv "a"))))) 2)
|
|
(ghm-test "ftv-scheme-quantified"
|
|
(hm-ftv-scheme (hm-scheme (list "a") (hm-arrow (hm-tv "a") (hm-tv "b")))) (list "b"))
|
|
(ghm-test "ftv-env"
|
|
(let ((env (assoc {} "f" (hm-monotype (hm-arrow (hm-tv "x") (hm-tv "y"))))))
|
|
(len (hm-ftv-env env))) 2)
|
|
|
|
;; ── Substitution / apply / compose ───────────────────────────────
|
|
(ghm-test "apply-tv"
|
|
(hm-apply (assoc {} "a" (hm-int)) (hm-tv "a")) (hm-int))
|
|
(ghm-test "apply-arrow"
|
|
(ctor-head
|
|
(hm-apply (assoc {} "a" (hm-int))
|
|
(hm-arrow (hm-tv "a") (hm-tv "b")))) "->")
|
|
(ghm-test "compose-1-then-2"
|
|
(var-name
|
|
(hm-apply
|
|
(hm-compose (assoc {} "b" (hm-tv "c")) (assoc {} "a" (hm-tv "b")))
|
|
(hm-tv "a"))) "c")
|
|
|
|
;; ── Generalize / Instantiate ─────────────────────────────────────
|
|
;; forall a. a -> a instantiated twice yields fresh vars each time
|
|
(ghm-test "generalize-id"
|
|
(len (hm-scheme-vars (hm-generalize (hm-arrow (hm-tv "a") (hm-tv "a")) {}))) 1)
|
|
|
|
(ghm-test "generalize-skips-env"
|
|
;; ftv(t)={a,b}, ftv(env)={a}, qs={b}
|
|
(let ((env (assoc {} "x" (hm-monotype (hm-tv "a")))))
|
|
(len (hm-scheme-vars
|
|
(hm-generalize (hm-arrow (hm-tv "a") (hm-tv "b")) env)))) 1)
|
|
|
|
(ghm-test "instantiate-fresh"
|
|
(let ((s (hm-scheme (list "a") (hm-arrow (hm-tv "a") (hm-tv "a"))))
|
|
(c (list 0)))
|
|
(let ((t1 (hm-instantiate s c)) (t2 (hm-instantiate s c)))
|
|
(not (= (var-name (first (ctor-args t1)))
|
|
(var-name (first (ctor-args t2)))))))
|
|
true)
|
|
|
|
;; ── Inference (literal only) ─────────────────────────────────────
|
|
(ghm-test "infer-int"
|
|
(ctor-head (get (hm-infer-literal (ast-literal 42)) :type)) "Int")
|
|
(ghm-test "infer-string"
|
|
(ctor-head (get (hm-infer-literal (ast-literal "hi")) :type)) "String")
|
|
(ghm-test "infer-bool"
|
|
(ctor-head (get (hm-infer-literal (ast-literal true)) :type)) "Bool")
|
|
|
|
(define ghm-tests-run!
|
|
(fn ()
|
|
{:passed ghm-test-pass
|
|
:failed ghm-test-fail
|
|
:total (+ ghm-test-pass ghm-test-fail)}))
|