From 23afc9dde3880a3a2b8750ecfef771746cf434a0 Mon Sep 17 00:00:00 2001 From: giles Date: Fri, 8 May 2026 22:41:22 +0000 Subject: [PATCH] =?UTF-8?q?haskell:=20typecheck.sx=2010/15=E2=86=9215/15?= =?UTF-8?q?=20+=20plan=20Phases=2020-22=20(HM=20gaps,=20classes,=20integra?= =?UTF-8?q?tion)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Five "typed ok: …" tests in tests/typecheck.sx compared an unforced thunk against an integer/list. The untyped-path convention is hk-deep-force on the result; hk-run-typed follows the same shape but the tests omitted that wrap. Added hk-deep-force around hk-run-typed in those five tests. typecheck.sx now 15/15; infer.sx still 75/75. Plan adds three phases capturing the remaining type-system work: - Phase 20: Algorithm W gaps (case, do, record accessors, expression annotations). - Phase 21: type classes with qualified types ([Eq a] => …) and constraint propagation, integrated with the existing dict-passing evaluator. - Phase 22: typecheck-then-run as the default conformance path, with a ≥ 30/36 typechecking threshold before swap. Co-Authored-By: Claude Opus 4.7 (1M context) --- lib/haskell/tests/typecheck.sx | 13 ++++--- plans/haskell-completeness.md | 69 ++++++++++++++++++++++++++++++++++ 2 files changed, 77 insertions(+), 5 deletions(-) diff --git a/lib/haskell/tests/typecheck.sx b/lib/haskell/tests/typecheck.sx index 6f46e089..242e476e 100644 --- a/lib/haskell/tests/typecheck.sx +++ b/lib/haskell/tests/typecheck.sx @@ -16,15 +16,18 @@ true))) ;; ─── Valid programs pass through ───────────────────────────────────────────── -(hk-test "typed ok: simple arithmetic" (hk-run-typed "main = 1 + 2") 3) +(hk-test "typed ok: simple arithmetic" + (hk-deep-force (hk-run-typed "main = 1 + 2")) 3) -(hk-test "typed ok: boolean" (hk-run-typed "main = True") (list "True")) +(hk-test "typed ok: boolean" + (hk-deep-force (hk-run-typed "main = True")) (list "True")) -(hk-test "typed ok: let binding" (hk-run-typed "main = let x = 1 in x + 2") 3) +(hk-test "typed ok: let binding" + (hk-deep-force (hk-run-typed "main = let x = 1 in x + 2")) 3) (hk-test "typed ok: two independent fns" - (hk-run-typed "f x = x + 1\nmain = f 5") + (hk-deep-force (hk-run-typed "f x = x + 1\nmain = f 5")) 6) ;; ─── Untypeable programs are rejected ──────────────────────────────────────── @@ -76,7 +79,7 @@ (hk-test "run-typed sig ok: Int declared matches" - (hk-run-typed "main :: Int\nmain = 1 + 2") + (hk-deep-force (hk-run-typed "main :: Int\nmain = 1 + 2")) 3) {:fails hk-test-fails :pass hk-test-pass :fail hk-test-fail} \ No newline at end of file diff --git a/plans/haskell-completeness.md b/plans/haskell-completeness.md index c2ae9398..d3df426f 100644 --- a/plans/haskell-completeness.md +++ b/plans/haskell-completeness.md @@ -359,10 +359,79 @@ that to single-digit minutes. - [ ] Verify the scoreboard output is byte-identical to the old per-process driver, then keep the per-process path as `--isolated` for debugging. +### Phase 20 — Close Algorithm W gaps + +`lib/haskell/infer.sx` already implements core HM (TVar/TCon/TArr/TApp/TTuple/ +TScheme, substitution, occurs-check unification, instantiate/generalize, let- +polymorphism). 75 inference unit tests + 15 typecheck integration tests pass. +The remaining gaps that block typing real programs: + +- [ ] `case` expressions in `hk-w`. Needs to infer scrutinee type, then for + each `(:alt pat body)` infer the pattern's binding env (extending + `hk-w-pat`) and unify body types across alts. +- [ ] `do` notation: extend `hk-type-env0` with `return :: a -> IO a`, + `(>>=) :: IO a -> (a -> IO b) -> IO b`, `(>>) :: IO a -> IO b -> IO b`, + and primitive IO actions (`putStrLn :: String -> IO ()`, + `getLine :: IO String`, etc.). May need a `TApp (TCon "IO") a` shape. +- [ ] Record-accessor desugaring leaves `__rec_field` placeholder visible to + inference. Either skip generated accessor clauses during `hk-infer-prog` + or rewrite the desugar to produce a typed shape. +- [ ] Type annotations in expressions `(x :: Int)` (parser also needed; see + Phase 17). Infer should unify the inferred type with the annotation. +- [ ] Tests in `lib/haskell/tests/infer-extras.sx` (≥ 10) covering the + above shapes. + +### Phase 21 — Type classes (Eq, Ord, Num, Show) + +The evaluator already implements typeclass dispatch via dict-passing +(`__default__ClassName_method` + per-instance dicts). The type system +ignores `class` and `instance` decls. Closing this means HM with +constraints (qualified types `[ClassName var] => type`). + +- [ ] Extend the type representation: `(TQual CONSTRAINTS TYPE)` where + `CONSTRAINTS = [(class-name . type-arg), …]`. +- [ ] Generalize → `forall vars. preds => type`; instantiate → fresh-rename + vars in both preds and type. +- [ ] During inference, when a primitive operator that needs a class is + used (e.g. `+`), emit a constraint `(Num t)`; collect constraints in + the substitution-threading. +- [ ] At let-generalization, simplify constraints (defaulting for `Num` + literals → `Int`; entailment via known instances). +- [ ] `class` declarations register members with their qualified type; + `instance` declarations register a witness. +- [ ] At top-level, if any unsolvable constraint remains → type error + ("No instance for X"). +- [ ] Tests in `lib/haskell/tests/typeclasses.sx` (≥ 12 covering Eq, Ord, + Num overloading, show on instances, instance ambiguity rejection). + +### Phase 22 — Typecheck-then-run as the default + +- [ ] Replace `hk-run` with a typecheck-first variant in the conformance + driver, or run conformance twice (once typed, once untyped) and report + both pass-rates in `scoreboard.md`. +- [ ] Investigate which existing 36 programs are untypeable due to gaps + closed in Phase 20-21 vs genuinely dynamically-typed; aim for ≥ 30/36 + programs typechecking before committing to the swap. +- [ ] If swap is committed, retire `hk-run` callsites in tests in favour + of `hk-run-typed`; keep the untyped path available for parser/eval + development against in-progress features. + ## Progress log _Newest first._ +**2026-05-08** — Plan extends with Phases 20-22 (HM type system). Discovered +during planning that `lib/haskell/infer.sx` already lands core Algorithm W +(75 inference unit tests pass; let-polymorphism, sig checking, error +reporting via `hk-expr->brief`). Fixed five regressing tests in +`lib/haskell/tests/typecheck.sx` that compared an unforced thunk against +the expected value — added `hk-deep-force` around `hk-run-typed` to match +the existing untyped-path convention. typecheck.sx now 15/15. +Phase 20 captures the remaining Algorithm W gaps (case, do, record +accessors, expression annotations); Phase 21 captures type classes with +qualified types; Phase 22 captures the integration step (typecheck-then-run +across conformance). + **2026-05-08** — Phase 16 Exception handling complete (6 ops + module wiring + 14 unit tests + 2 conformance programs). `hk-bind-exceptions!` in `eval.sx` registers `throwIO`, `throw`, `evaluate`, `catch`, `try`, `handle`, and