ocaml: phase 5 HM tuple + list types (+7 tests, 326 total)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 29s

Tuple type (hm-con "*" TYPES); list type (hm-con "list" (TYPE)).
ocaml-infer-tuple threads substitution through each item left-to-right.
ocaml-infer-list unifies all items with a fresh 'a (giving 'a list for
empty []).

Pretty-printer renders 'Int * Int' for tuples and 'Int list' for lists,
matching standard OCaml notation.

Examples:
  fun x y -> (x, y) : 'a -> 'b -> 'a * 'b
  fun x -> [x; x] : 'a -> 'a list
  []                : 'a list
This commit is contained in:
2026-05-08 12:54:15 +00:00
parent a0abdcf520
commit 6d7197182e
3 changed files with 92 additions and 1 deletions

View File

@@ -145,6 +145,56 @@
{:subst sf
:type (hm-apply sf te)}))))))))))))
;; Tuple type: (hm-con "*" (list T1 T2 ...)).
(define ocaml-hm-tuple
(fn (types) (hm-con "*" types)))
;; List type: (hm-con "list" (list ELEM)).
(define ocaml-hm-list
(fn (elem) (hm-con "list" (list elem))))
(define ocaml-infer-tuple
(fn (items env counter)
(let ((subst {}) (types (list)))
(begin
(define loop
(fn (xs env-cur)
(when (not (= xs (list)))
(let ((r (ocaml-infer (first xs) env-cur counter)))
(let ((s (get r :subst)) (t (get r :type)))
(begin
(set! subst (hm-compose s subst))
(append! types t)
(loop (rest xs) (hm-apply-env s env-cur))))))))
(loop items env)
{:subst subst
:type (ocaml-hm-tuple
(map (fn (t) (hm-apply subst t)) types))}))))
(define ocaml-infer-list
(fn (items env counter)
(cond
((= (len items) 0)
{:subst {} :type (ocaml-hm-list (hm-fresh-tv counter))})
(else
(let ((subst {}) (elem-tv (hm-fresh-tv counter)))
(begin
(define loop
(fn (xs env-cur)
(when (not (= xs (list)))
(let ((r (ocaml-infer (first xs) env-cur counter)))
(let ((s (get r :subst)) (t (get r :type)))
(let ((s2 (ocaml-hm-unify
(hm-apply s elem-tv)
t
(hm-compose s subst))))
(begin
(set! subst s2)
(loop (rest xs) (hm-apply-env s2 env-cur)))))))))
(loop items env)
{:subst subst
:type (ocaml-hm-list (hm-apply subst elem-tv))}))))))
(set! ocaml-infer
(fn (expr env counter)
(let ((tag (nth expr 0)))
@@ -162,6 +212,8 @@
(nth expr 3) (nth expr 4) env counter))
((= tag "if") (ocaml-infer-if (nth expr 1) (nth expr 2)
(nth expr 3) env counter))
((= tag "tuple") (ocaml-infer-tuple (rest expr) env counter))
((= tag "list") (ocaml-infer-list (rest expr) env counter))
((= tag "neg")
(let ((r (ocaml-infer (nth expr 1) env counter)))
(let ((s (get r :subst)) (t (get r :type)))
@@ -205,5 +257,11 @@
(str "(" (ocaml-hm-format-type a) ")"))
(else (ocaml-hm-format-type a)))
" -> " (ocaml-hm-format-type b))))
((= head "*")
(let ((parts (map ocaml-hm-format-type args)))
(join " * " parts)))
((= head "list")
(let ((elem (ocaml-hm-format-type (nth args 0))))
(str elem " list")))
(else head))))
(else (str t)))))

View File

@@ -798,6 +798,22 @@ cat > "$TMPFILE" << 'EPOCHS'
(epoch 1422)
(eval "(ocaml-run \"Result.map_error (fun e -> e + 1) (Error 5)\")")
;; ── HM extensions: tuples + lists ──────────────────────────────
(epoch 1500)
(eval "(ocaml-type-of \"(1, 2)\")")
(epoch 1501)
(eval "(ocaml-type-of \"(1, true, \\\"hi\\\")\")")
(epoch 1502)
(eval "(ocaml-type-of \"[1; 2; 3]\")")
(epoch 1503)
(eval "(ocaml-type-of \"[]\")")
(epoch 1504)
(eval "(ocaml-type-of \"fun x -> [x; x]\")")
(epoch 1505)
(eval "(ocaml-type-of \"fun x y -> (x, y)\")")
(epoch 1506)
(eval "(ocaml-type-of \"[true; false]\")")
EPOCHS
OUTPUT=$(timeout 180 "$SX_SERVER" < "$TMPFILE" 2>/dev/null)
@@ -1263,6 +1279,15 @@ check 1420 "Result.get_ok" '42'
check 1421 "Result.to_option Ok" '("Some" 1)'
check 1422 "Result.map_error" '("Error" 6)'
# ── HM tuples + lists ───────────────────────────────────────────
check 1500 "type tuple Int*Int" '"Int * Int"'
check 1501 "type 3-tuple" '"Int * Bool * String"'
check 1502 "type Int list" '"Int list"'
check 1503 "type [] poly" ' list'
check 1504 "type fn -> list" 'list"'
check 1505 "type fn -> tuple" ' * '
check 1506 "type Bool list" '"Bool list"'
TOTAL=$((PASS + FAIL))
if [ $FAIL -eq 0 ]; then
echo "ok $PASS/$TOTAL OCaml-on-SX tests passed"

View File

@@ -228,7 +228,8 @@ SX CEK evaluator (both JS and OCaml hosts)
- [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`.
- [~] Function types `T1 -> T2` work; tuples/records pending.
- [~] 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.
- [ ] Module type checking: seal against `sig` (Phase 4 stubs become real checks).
- [ ] Error reporting: position-tagged errors with expected vs actual types.
@@ -361,6 +362,13 @@ the "mother tongue" closure: OCaml → SX → OCaml. This means:
_Newest first._
- 2026-05-08 Phase 5 — HM extensions for tuples and lists (+7 tests,
326 total). Tuple type `(hm-con "*" TYPES)`, list type `(hm-con
"list" (TYPE))`. `ocaml-infer-tuple` threads substitution through
each item; `ocaml-infer-list` unifies all elements with a fresh
`'a` (giving `'a list` for `[]`). Pretty-printer renders `Int * Int`
and `Int list` like real OCaml. `fun x y -> (x, y) : 'a -> 'b -> 'a
* 'b`. `fun x -> [x; x] : 'a -> 'a list`.
- 2026-05-08 Phase 6 — expanded stdlib slice (+15 tests, 319 total).
List: concat/flatten, init, find/find_opt, partition, mapi/iteri,
assoc/assoc_opt. Option: iter, fold, to_list. Result: get_ok,