ocaml-type-of-program now handles :def-mut (sequential generalize) and
:def-rec-mut (pre-bind tvs, infer rhs, unify, generalize all, infer
body — same algorithm as the inline let-rec-mut version).
Mutual top-level recursion now type-checks:
let rec even n = ... and odd n = ...;; even 10 : Bool
let rec map f xs = ... and length lst = ...;; map :
('a -> 'b) -> 'a list -> 'b list
ocaml-infer-let-mut: each rhs inferred in parent env, generalized
sequentially before adding to body env.
ocaml-infer-let-rec-mut: pre-bind all names with fresh tvs; infer
each rhs against the joint env, unify each with its tv, then
generalize all and infer body.
Mutual recursion now type-checks:
let rec even n = if n = 0 then true else odd (n - 1)
and odd n = if n = 0 then false else even (n - 1)
in even : Int -> Bool
ocaml-hm-parse-type-src recognises primitive type names (int/bool/
string/float/unit), tyvars 'a, and simple parametric T list / T option.
Replaces the previous int-by-default placeholder in
ocaml-hm-register-type-def!.
So 'type tag = TStr of string | TInt of int' correctly registers
TStr : string -> tag and TInt : int -> tag. Pattern-match on tag
gives proper field types in the body. Multi-arg / function types
still fall back to a fresh tv.
ocaml-hm-ctors is now a mutable list cell; user type-defs register
their constructors via ocaml-hm-register-type-def!. New
ocaml-type-of-program processes top-level decls in order:
- type-def: register ctors with the scheme inferred from PARAMS+CTORS
- def/def-rec: generalize and bind in the type env
- exception-def: no-op for typing
- expr: return inferred type
Examples:
type color = Red | Green | Blue;; Red : color
type shape = Circle of int | Square of int;;
let area s = match s with
| Circle r -> r * r
| Square s -> s * s;;
area : shape -> Int
Caveat: ctor arg types parsed as raw source strings; registry defaults
to int for any single-arg ctor. Proper type-source parsing pending.
ocaml-infer-let-rec pre-binds the function name to a fresh tv before
inferring rhs (which may recursively call the name), unifies the
inferred rhs type with the tv, generalizes, then infers body.
Builtin env types :: : 'a -> 'a list -> 'a list and @ : 'a list ->
'a list -> 'a list — needed because :op compiles to (:app (:app (:var
OP) L) R) and previously these var lookups failed.
Examples now infer:
let rec fact n = if ... in fact : Int -> Int
let rec len lst = ... in len : 'a list -> Int
let rec map f xs = ... in map : ('a -> 'b) -> 'a list -> 'b list
1 :: [2; 3] : Int list
let rec sum lst = ... in sum [1;2;3] : Int
Scoreboard refreshed: 358/358 across 14 suites.
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.
ocaml-infer-pat covers :pwild, :pvar, :plit, :pcons, :plist, :ptuple,
:pas. Returns {:type T :env ENV2 :subst S} where ENV2 has the pattern's
bound names threaded through.
ocaml-infer-match unifies each clause's pattern type with the scrutinee,
runs the body in the env extended with pattern bindings, and unifies
all body types via a fresh result tv.
Examples:
fun lst -> match lst with | [] -> 0 | h :: _ -> h : Int list -> Int
match (1, 2) with | (a, b) -> a + b : Int
Constructor patterns (:pcon) fall through to a fresh tv for now —
proper handling needs a ctor type registry from 'type' declarations.
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
OCaml-on-SX is the deferred second consumer for lib/guest/hm.sx step 8.
lib/ocaml/infer.sx assembles Algorithm W on top of the shipped algebra:
- Var: lookup + hm-instantiate.
- Fun: fresh-tv per param, auto-curried via recursion.
- App: unify against hm-arrow, fresh-tv for result.
- Let: generalize rhs over (ftv(t) - ftv(env)) — let-polymorphism.
- If: unify cond with Bool, both branches with each other.
- Op (+, =, <, etc.): builtin signatures (int*int->int monomorphic,
=/<> polymorphic 'a->'a->bool).
Tests pass for: literals, fun x -> x : 'a -> 'a, let id ... id 5/id true,
fun f x -> f (f x) : ('a -> 'a) -> 'a -> 'a (twice).
Pending: tuples, lists, pattern matching, let-rec, modules in HM.
