From 81247eb6ea4c3ece22ca3dca556c65b69ed4b77e Mon Sep 17 00:00:00 2001 From: giles Date: Fri, 8 May 2026 13:05:22 +0000 Subject: [PATCH] ocaml: phase 5 HM ctor inference for option/result (+7 tests, 351 total) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ocaml-hm-ctor-env registers None/Some : 'a -> 'a option, Ok/Error : 'a -> ('a, 'b) result. :con NAME instantiates the scheme; :pcon NAME ARG-PATS walks arg patterns through the constructor's arrow type, unifying each. Pretty-printer renders 'Int option' and '(Int, 'b) result'. Examples now infer: fun x -> Some x : 'a -> 'a option match Some 5 with | None -> 0 | Some n -> n : Int fun o -> match o with | None -> 0 | Some n -> n : Int option -> Int Ok 1 : (Int, 'b) result Error "oops" : ('a, String) result User type-defs would extend the registry — pending. --- lib/ocaml/infer.sx | 73 +++++++++++++++++++++++++++++++++++++++++++- lib/ocaml/test.sh | 25 +++++++++++++++ plans/ocaml-on-sx.md | 13 +++++++- 3 files changed, 109 insertions(+), 2 deletions(-) diff --git a/lib/ocaml/infer.sx b/lib/ocaml/infer.sx index 212e80ee..081aab0d 100644 --- a/lib/ocaml/infer.sx +++ b/lib/ocaml/infer.sx @@ -22,6 +22,21 @@ (define ocaml-hm-empty-subst (fn () {})) +;; A registry of constructor types so :con / :pcon can be inferred. +;; OCaml's stdlib ctors are seeded here; user type-defs would extend +;; this in a future iteration. +(define ocaml-hm-ctor-env + (fn () + (let ((a (hm-tv "a")) (b (hm-tv "b"))) + (let ((opt-of-a (hm-con "option" (list a))) + (res-of-ab (hm-con "result" (list a b)))) + {"None" (hm-scheme (list "a") opt-of-a) + "Some" (hm-scheme (list "a") (hm-arrow a opt-of-a)) + "Ok" (hm-scheme (list "a" "b") (hm-arrow a res-of-ab)) + "Error" (hm-scheme (list "a" "b") (hm-arrow b res-of-ab)) + "true" (hm-monotype (hm-bool)) + "false" (hm-monotype (hm-bool))})))) + (define ocaml-hm-builtin-env (fn () (let ((int-int-int (hm-arrow (hm-int) (hm-arrow (hm-int) (hm-int)))) @@ -176,6 +191,42 @@ ;; Constructor patterns aren't supported here yet (need a type-def ;; registry) — :pcon falls through to a fresh tv so they don't break ;; inference of mixed clauses. +(define ocaml-infer-pcon + (fn (name arg-pats env counter) + (cond + ((has-key? ocaml-hm-ctors name) + (let ((ctor-type (hm-instantiate (get ocaml-hm-ctors name) counter)) + (env-cur env) (subst {})) + (let ((cur-type (list nil))) + (begin + (set-nth! cur-type 0 ctor-type) + (define loop + (fn (xs) + (when (not (= xs (list))) + (let ((rp (ocaml-infer-pat (first xs) env-cur counter))) + (let ((arg-tv (hm-fresh-tv counter)) + (res-tv (hm-fresh-tv counter))) + (let ((s1 (ocaml-hm-unify + (nth cur-type 0) + (hm-arrow arg-tv res-tv) + (hm-compose (get rp :subst) subst)))) + (let ((s2 (ocaml-hm-unify + (hm-apply s1 arg-tv) + (hm-apply s1 (get rp :type)) + s1))) + (begin + (set! subst s2) + (set-nth! cur-type 0 (hm-apply s2 res-tv)) + (set! env-cur (get rp :env)) + (loop (rest xs)))))))))) + (loop arg-pats) + {:type (hm-apply subst (nth cur-type 0)) + :env env-cur + :subst subst})))) + (else + (let ((tv (hm-fresh-tv counter))) + {:type tv :env env :subst {}}))))) + (define ocaml-infer-pat (fn (pat env counter) (let ((tag (nth pat 0))) @@ -241,8 +292,9 @@ {:type (get rp :type) :env (assoc (get rp :env) alias (hm-monotype (get rp :type))) :subst (get rp :subst)}))) + ((= tag "pcon") + (ocaml-infer-pcon (nth pat 1) (rest (rest pat)) env counter)) (else - ;; :pcon and others — fall through to a fresh tv (sound but loose). (let ((tv (hm-fresh-tv counter))) {:type tv :env env :subst {}})))))) @@ -302,10 +354,22 @@ {:subst subst :type (ocaml-hm-list (hm-apply subst elem-tv))})))))) +(define ocaml-hm-ctors (ocaml-hm-ctor-env)) + (set! ocaml-infer (fn (expr env counter) (let ((tag (nth expr 0))) (cond + ((= tag "con") + ;; (:con NAME) — look up constructor type, instantiate fresh. + (let ((name (nth expr 1))) + (cond + ((has-key? ocaml-hm-ctors name) + {:subst {} + :type (hm-instantiate (get ocaml-hm-ctors name) counter)}) + (else + ;; Unknown ctor — treat as a fresh polymorphic type. + {:subst {} :type (hm-fresh-tv counter)})))) ((= tag "int") {:subst {} :type (hm-int)}) ((= tag "float") {:subst {} :type (hm-int)}) ;; treat float as int for now ((= tag "string") {:subst {} :type (hm-string)}) @@ -371,5 +435,12 @@ ((= head "list") (let ((elem (ocaml-hm-format-type (nth args 0)))) (str elem " list"))) + ((= head "option") + (let ((elem (ocaml-hm-format-type (nth args 0)))) + (str elem " option"))) + ((= head "result") + (let ((a (ocaml-hm-format-type (nth args 0))) + (b (ocaml-hm-format-type (nth args 1)))) + (str "(" a ", " b ") result"))) (else head)))) (else (str t))))) diff --git a/lib/ocaml/test.sh b/lib/ocaml/test.sh index 552b33c9..b1425436 100755 --- a/lib/ocaml/test.sh +++ b/lib/ocaml/test.sh @@ -856,6 +856,22 @@ cat > "$TMPFILE" << 'EPOCHS' (epoch 1804) (eval "(ocaml-type-of \"fun lst -> match lst with | [] -> 0 | h :: _ -> h\")") +;; ── HM constructor inference (option/result) ─────────────────── +(epoch 1900) +(eval "(ocaml-type-of \"Some 5\")") +(epoch 1901) +(eval "(ocaml-type-of \"None\")") +(epoch 1902) +(eval "(ocaml-type-of \"Ok 1\")") +(epoch 1903) +(eval "(ocaml-type-of \"Error \\\"oops\\\"\")") +(epoch 1904) +(eval "(ocaml-type-of \"fun x -> Some x\")") +(epoch 1905) +(eval "(ocaml-type-of \"match Some 5 with | None -> 0 | Some n -> n\")") +(epoch 1906) +(eval "(ocaml-type-of \"fun o -> match o with | None -> 0 | Some n -> n\")") + EPOCHS OUTPUT=$(timeout 180 "$SX_SERVER" < "$TMPFILE" 2>/dev/null) @@ -1354,6 +1370,15 @@ check 1802 "match tuple" '"Int"' check 1803 "fn match int -> int" '"Int -> Int"' check 1804 "fn list -> elem" '"Int list -> Int"' +# ── HM ctor inference ────────────────────────────────────────── +check 1900 "Some 5 : Int option" '"Int option"' +check 1901 "None : 'a option" ' option' +check 1902 "Ok 1 : (Int, 'b) result" '"(Int' +check 1903 "Error 'oops'" 'String) result' +check 1904 "fun x -> Some x" ' option' +check 1905 "match Some/None -> Int" '"Int"' +check 1906 "Int option -> Int" '"Int option -> Int"' + TOTAL=$((PASS + FAIL)) if [ $FAIL -eq 0 ]; then echo "ok $PASS/$TOTAL OCaml-on-SX tests passed" diff --git a/plans/ocaml-on-sx.md b/plans/ocaml-on-sx.md index 170c85e8..c90f0701 100644 --- a/plans/ocaml-on-sx.md +++ b/plans/ocaml-on-sx.md @@ -227,7 +227,10 @@ SX CEK evaluator (both JS and OCaml hosts) pattern matching, let-rec, modules.)_ - [x] Type variables: `'a`, `'b`; unification with occur-check (kit). - [x] Let-polymorphism: generalise at let-bindings (kit `hm-generalize`). -- [ ] ADT types: `type 'a option = None | Some of 'a`. +- [~] ADT types: `option`/`result` ctors hardcoded in + `ocaml-hm-ctor-env`; `:con NAME` and `:pcon NAME …` look up the + scheme and instantiate. User type-defs would extend the registry. + Format: `Int option`, `(Int, 'b) result`. - [~] Function types `T1 -> T2` work; tuples (`'a * 'b`) and lists (`'a list`) supported. Records pending. - [ ] Type signatures: `val f : int -> int` — verify against inferred type. @@ -365,6 +368,14 @@ the "mother tongue" closure: OCaml → SX → OCaml. This means: _Newest first._ +- 2026-05-08 Phase 5 — HM constructor inference for option/result (+7 + tests, 351 total). `ocaml-hm-ctor-env` registers None/Some (`'a opt`), + Ok/Error (`('a, 'b) result`). `:con NAME` instantiates the scheme; + `:pcon NAME ARG-PATS` walks arg patterns through the constructor's + arrow type, unifying each. Pretty-printer renders `Int option` and + `(Int, 'b) result`. Examples: + `fun x -> Some x : 'a -> 'a option` + `fun o -> match o with | None -> 0 | Some n -> n : Int option -> Int` - 2026-05-08 Phase 5 — HM pattern-matching inference (+5 tests, 344 total). `ocaml-infer-pat` covers wild, var, lit, cons, list, tuple, as. `ocaml-infer-match` unifies each clause's pattern type with the