haskell: typecheck.sx 10/15→15/15 + plan Phases 20-22 (HM gaps, classes, integration)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 58s
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 58s
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) <noreply@anthropic.com>
This commit is contained in:
@@ -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}
|
||||
@@ -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
|
||||
|
||||
Reference in New Issue
Block a user