From 2606b83920c45378b37cbff5d97c9f7c44b842dc Mon Sep 17 00:00:00 2001 From: giles Date: Tue, 5 May 2026 22:32:18 +0000 Subject: [PATCH] =?UTF-8?q?haskell:=20reject=20untypeable=20programs=20?= =?UTF-8?q?=E2=80=94=20hk-typecheck=20+=20hk-run-typed=20(+9=20tests,=2046?= =?UTF-8?q?4/464)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Sonnet 4.6 --- lib/haskell/eval.sx | 22 ++++++++++ lib/haskell/infer.sx | 76 ++++++++++++++++++---------------- lib/haskell/test.sh | 4 +- lib/haskell/tests/typecheck.sx | 44 ++++++++++++++++++++ plans/haskell-on-sx.md | 13 +++++- 5 files changed, 121 insertions(+), 38 deletions(-) create mode 100644 lib/haskell/tests/typecheck.sx diff --git a/lib/haskell/eval.sx b/lib/haskell/eval.sx index 46eb364b..82b2936b 100644 --- a/lib/haskell/eval.sx +++ b/lib/haskell/eval.sx @@ -790,3 +790,25 @@ negate x = 0 - x (fn (src) (hk-deep-force (hk-eval (hk-core-expr src) (hk-dict-copy hk-env0))))) + +(define + hk-typecheck + (fn + (prog) + (let + ((results (hk-infer-prog prog (hk-type-env0)))) + (let + ((errors (filter (fn (r) (= (first r) "err")) results))) + (when (not (empty? errors)) (raise (nth (first errors) 1))))))) + +(define + hk-run-typed + (fn + (src) + (let + ((prog (hk-core src))) + (begin + (hk-typecheck prog) + (let + ((env (hk-eval-program prog))) + (cond ((has-key? env "main") (get env "main")) (:else env))))))) diff --git a/lib/haskell/infer.sx b/lib/haskell/infer.sx index a2634e31..992c264b 100644 --- a/lib/haskell/infer.sx +++ b/lib/haskell/infer.sx @@ -525,33 +525,37 @@ hk-infer-decl (fn (env decl) - (let ((tag (first decl))) + (let + ((tag (first decl))) (cond ((= tag "fun-clause") - (let ((name (nth decl 1)) - (pats (nth decl 2)) - (body (nth decl 3))) - (let ((rhs (if (empty? pats) body (list "lambda" pats body)))) - (guard - (e (#t (list "err" (str "in '" name "': " e)))) - (begin - (hk-reset-fresh) - (let ((r (hk-w env rhs))) - (list "ok" name - (hk-type->str (hk-subst-apply (first r) (nth r 1)))))))))) + (let + ((name (nth decl 1)) (pats (nth decl 2)) (body (nth decl 3))) + (let + ((rhs (if (empty? pats) body (list "lambda" pats body)))) + (guard + (e (#t (list "err" (str "in '" name "': " e)))) + (begin + (hk-reset-fresh) + (let + ((r (hk-w env rhs))) + (let + ((final-type (hk-subst-apply (first r) (nth r 1)))) + (list "ok" name (hk-type->str final-type) final-type)))))))) ((or (= tag "bind") (= tag "pat-bind")) - (let ((pat (nth decl 1)) - (body (nth decl 2))) - (let ((label (if (and (list? pat) (= (first pat) "p-var")) - (nth pat 1) - ""))) - (guard - (e (#t (list "err" (str "in '" label "': " e)))) - (begin - (hk-reset-fresh) - (let ((r (hk-w env body))) - (list "ok" label - (hk-type->str (hk-subst-apply (first r) (nth r 1)))))))))) + (let + ((pat (nth decl 1)) (body (nth decl 2))) + (let + ((label (if (and (list? pat) (= (first pat) "p-var")) (nth pat 1) ""))) + (guard + (e (#t (list "err" (str "in '" label "': " e)))) + (begin + (hk-reset-fresh) + (let + ((r (hk-w env body))) + (let + ((final-type (hk-subst-apply (first r) (nth r 1)))) + (list "ok" label (hk-type->str final-type) final-type)))))))) (:else nil))))) ;; hk-infer-prog : program-ast × env → list of ("ok" name type) | ("err" msg) @@ -560,18 +564,20 @@ hk-infer-prog (fn (prog env) - (let ((decls (cond - ((and (list? prog) (= (first prog) "program")) - (nth prog 1)) - ((and (list? prog) (= (first prog) "module")) - (nth prog 3)) - (:else (list)))) - (results (list))) + (let + ((decls (cond ((and (list? prog) (= (first prog) "program")) (nth prog 1)) ((and (list? prog) (= (first prog) "module")) (nth prog 3)) (:else (list)))) + (results (list))) (for-each - (fn (d) - (let ((r (hk-infer-decl env d))) - (when (not (nil? r)) - (append! results r)))) + (fn + (d) + (let + ((r (hk-infer-decl env d))) + (when + (not (nil? r)) + (append! results r) + (when + (= (first r) "ok") + (dict-set! env (nth r 1) (nth r 3)))))) decls) results))) diff --git a/lib/haskell/test.sh b/lib/haskell/test.sh index e129acf0..320335a4 100755 --- a/lib/haskell/test.sh +++ b/lib/haskell/test.sh @@ -42,9 +42,9 @@ FAILED_FILES=() for FILE in "${FILES[@]}"; do [ -f "$FILE" ] || { echo "skip $FILE (not found)"; continue; } - # Load infer.sx only for infer test files (it adds ~6s overhead). + # Load infer.sx only for infer/typecheck test files (it adds ~6s overhead). INFER_LOAD="" - case "$FILE" in *infer*) INFER_LOAD='(load "lib/haskell/infer.sx")' ;; esac + case "$FILE" in *infer*|*typecheck*) INFER_LOAD='(load "lib/haskell/infer.sx")' ;; esac TMPFILE=$(mktemp) cat > "$TMPFILE" <= (index-of s sub) 0))) + +;; Helper: expect a type error containing `sub` +(define + hk-tc-err + (fn + (label src sub) + (hk-test + label + (guard + (e (#t (hk-str-has? e sub))) + (begin (hk-run-typed src) false)) + true))) + +;; ─── Valid programs pass through ───────────────────────────────────────────── +(hk-test "typed ok: simple arithmetic" (hk-run-typed "main = 1 + 2") 3) + +(hk-test "typed ok: boolean" (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: two independent fns" + (hk-run-typed "f x = x + 1\nmain = f 5") + 6) + +;; ─── Untypeable programs are rejected ──────────────────────────────────────── +;; Adding Int and Bool is a unification failure. +(hk-tc-err "reject: Int + Bool mentions Int" "main = 1 + True" "Int") +(hk-tc-err "reject: Int + Bool mentions Bool" "main = 1 + True" "Bool") + +;; Condition of if must be Bool. +(hk-tc-err "reject: if non-bool condition" "main = if 1 then 2 else 3" "Bool") + +;; Unbound variable. +(hk-tc-err "reject: unbound variable" "main = unknownVar + 1" "unknownVar") + +;; Function body type error: applying non-function. +(hk-tc-err "reject: apply non-function" "f x = 1 x" "Int") + +{:fails hk-test-fails :pass hk-test-pass :fail hk-test-fail} \ No newline at end of file diff --git a/plans/haskell-on-sx.md b/plans/haskell-on-sx.md index 598e62d9..4a012398 100644 --- a/plans/haskell-on-sx.md +++ b/plans/haskell-on-sx.md @@ -93,7 +93,7 @@ Key mappings: ### Phase 4 — Hindley-Milner inference - [x] Algorithm W: unification + type schemes + generalisation + instantiation - [x] Report type errors with meaningful positions -- [ ] Reject untypeable programs that phase 3 was accepting +- [x] Reject untypeable programs that phase 3 was accepting - [ ] Type-sig checking: user writes `f :: Int -> Int`; verify - [ ] Let-polymorphism - [ ] Unit tests: inference for 50+ expressions @@ -114,6 +114,17 @@ Key mappings: _Newest first._ +- **2026-05-05** — Phase 4 reject untypeable programs. `hk-typecheck` runs + `hk-infer-prog` on a program AST and raises the first type error found. + `hk-run-typed` is a drop-in for `hk-run` that gates evaluation on a + successful type check. `hk-infer-decl` now returns a 4th element (raw type + value); `hk-infer-prog` propagates inferred types into the running type env + so multi-function programs (`f x = x+1\ng y = f y+2`) infer correctly. + test.sh extended to load infer.sx for `*typecheck*` files. + 9 new tests in `tests/typecheck.sx`: 4 valid programs pass through, 5 + invalid programs are rejected (Int+Bool, non-Bool if condition, unbound var, + apply non-function). 464/464 green. + - **2026-05-05** — Phase 4 type error reporting. `hk-expr->brief` converts any AST node to a short human-readable string for error messages (handles var/con/int/float/ str/char/bool/app/op/if/let/lambda/tuple/list/loc). `loc` nodes in `hk-w` delegate