giles ab2c40c14c GUEST: step 8 — lib/guest/hm.sx Hindley-Milner foundations ...

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>

2026-05-07 19:45:10 +00:00

5.6 KiB

Raw Blame History

View Raw