From 3c20383851b0cd939749bc83615340313b1b1fec Mon Sep 17 00:00:00 2001 From: Yogthos Date: Sat, 13 Jun 2026 01:46:34 -0400 Subject: [PATCH] feat: Phase 0 intra-procedural collection-type inference (jolt-6sr) A forward, soft-typing-style pass (simplified HM: monovariant, never-fails, lattice top = :any) in jolt.passes, run after the inline/scalar-replace fixpoint when the optimization mode is on. It types expressions from literals and arithmetic, flows the type through let bindings, and joins at if-branches. Where a keyword-lookup subject is PROVEN to be a plain struct map it sets :hint :struct (the same channel a manual hint uses, so the back end drops the :jolt/type guard); where the type is :any it leaves the dynamic guard in place. Sound by construction: a concrete type is assigned only when proven (scalar keys with non-nil/non-false values for a struct-map), so a wrong bare get can't happen. This is the foundation; on its own it mostly overlaps Route 1 scalar-replacement (which already eliminates non-escaping let-bound maps), so its standalone win is small. Phase 1 (inter-procedural) is where escaping params get typed. Verified: conformance 335/335 x3, full jpm test; new type-infer-test pins the flow rules and the sound :any fallback (cases force the map to escape so the test isolates inference from scalar-replacement). --- jolt-core/jolt/passes.clj | 127 +++++++++++++++++++++++-- test/integration/type-infer-test.janet | 54 +++++++++++ 2 files changed, 174 insertions(+), 7 deletions(-) create mode 100644 test/integration/type-infer-test.janet diff --git a/jolt-core/jolt/passes.clj b/jolt-core/jolt/passes.clj index 76a7656..5e73c06 100644 --- a/jolt-core/jolt/passes.clj +++ b/jolt-core/jolt/passes.clj @@ -706,18 +706,131 @@ :finally (when (get node :finally) (scalar-replace (get node :finally)))) :else node))) +;; --------------------------------------------------------------------------- +;; Collection-type inference (jolt-99x), Phase 0: intra-procedural. A forward, +;; soft-typing-style pass (simplified HM: monovariant, never-fails, lattice top +;; = :any) that types expressions from literals/arithmetic and flows the type +;; through let bindings and if-joins. Where a keyword-lookup subject is PROVEN a +;; plain struct map it sets :hint :struct (the same channel a manual hint uses, +;; so the back end drops the guard); where the type is :any it leaves the +;; dynamic guard in place. Sound by construction: a concrete type is assigned +;; only when proven, so a wrong bare get is impossible. +;; +;; Lattice values: :struct-map (raw-get-safe), :phm-map, :vector, :set, :truthy +;; (a provably non-nil/non-false scalar — numbers, strings, keywords), :any (top). +(defn- join [a b] (if (= a b) a :any)) +(defn- struct-safe? [t] (= t :struct-map)) +;; a value whose type guarantees it is neither nil nor false — the back end only +;; builds a struct (vs a phm) when every value is truthy, so a map literal is a +;; struct only when all its values have a truthy type. +(defn- truthy-type? [t] + (or (= t :truthy) (= t :struct-map) (= t :phm-map) (= t :vector) (= t :set))) + +(def ^:private truthy-ret-fns + #{"+" "-" "*" "/" "inc" "dec" "mod" "rem" "quot" "min" "max" "abs" + "bit-and" "bit-or" "bit-xor" "count"}) +(def ^:private vector-ret-fns #{"vec" "vector" "mapv" "filterv" "subvec"}) + +(defn- call-ret-type [fnode] + (let [nm (cond + (and (= :var (get fnode :op)) (= "clojure.core" (get fnode :ns))) (get fnode :name) + (= :host (get fnode :op)) (get fnode :name) + :else nil)] + (cond + (nil? nm) :any + (contains? truthy-ret-fns nm) :truthy + (contains? vector-ret-fns nm) :vector + :else :any))) + +(defn- infer + "Returns [type node'] — the inferred type of node and node with struct-safe + :local references annotated :hint :struct. tenv maps in-scope local names to + inferred types." + [node tenv] + (let [op (get node :op)] + (cond + (= op :const) + [(let [v (get node :val)] (if (or (nil? v) (= false v)) :any :truthy)) node] + (= op :local) + (let [t (get tenv (get node :name))] + [(if t t :any) (if (struct-safe? t) (assoc node :hint :struct) node)]) + (= op :map) + (let [res (mapv (fn [pr] + (let [kr (infer (nth pr 0) tenv) + vr (infer (nth pr 1) tenv)] + [(nth kr 1) (nth vr 1) (nth vr 0)])) + (get node :pairs)) + t (if (and (> (count res) 0) + (every? (fn [pr] (scalar-const? (nth pr 0))) (get node :pairs)) + (every? (fn [r] (truthy-type? (nth r 2))) res)) + :struct-map :any)] + [t (assoc node :pairs (mapv (fn [r] [(nth r 0) (nth r 1)]) res))]) + (= op :vector) + [:vector (assoc node :items (mapv (fn [x] (nth (infer x tenv) 1)) (get node :items)))] + (= op :set) + [:set (assoc node :items (mapv (fn [x] (nth (infer x tenv) 1)) (get node :items)))] + (= op :if) + (let [tr (infer (get node :test) tenv) + thn (infer (get node :then) tenv) + els (infer (get node :else) tenv)] + [(join (nth thn 0) (nth els 0)) + (assoc node :test (nth tr 1) :then (nth thn 1) :else (nth els 1))]) + (= op :do) + (let [stmts (mapv (fn [s] (nth (infer s tenv) 1)) (get node :statements)) + r (infer (get node :ret) tenv)] + [(nth r 0) (assoc node :statements stmts :ret (nth r 1))]) + (= op :throw) + [:any (assoc node :expr (nth (infer (get node :expr) tenv) 1))] + (= op :invoke) + (let [fr (infer (get node :fn) tenv) + args (mapv (fn [a] (nth (infer a tenv) 1)) (get node :args))] + [(call-ret-type (get node :fn)) (assoc node :fn (nth fr 1) :args args)]) + (= op :let) + (let [res (reduce (fn [acc b] + (let [te (nth acc 0) binds (nth acc 1) + ir (infer (nth b 1) te)] + [(assoc te (nth b 0) (nth ir 0)) (conj binds [(nth b 0) (nth ir 1)])])) + [tenv []] (get node :bindings)) + br (infer (get node :body) (nth res 0))] + [(nth br 0) (assoc node :bindings (nth res 1) :body (nth br 1))]) + (= op :loop) + ;; conservative + sound: loop bindings join across recur, which we don't + ;; track in Phase 0, so they stay :any. Still descend to annotate any + ;; known-type lookups inside the body. + [:any (assoc node + :bindings (mapv (fn [b] [(nth b 0) (nth (infer (nth b 1) tenv) 1)]) (get node :bindings)) + :body (nth (infer (get node :body) tenv) 1))] + (= op :recur) + [:any (assoc node :args (mapv (fn [a] (nth (infer a tenv) 1)) (get node :args)))] + (= op :fn) + [:any (assoc node :arities (mapv (fn [a] (assoc a :body (nth (infer (get a :body) {}) 1))) + (get node :arities)))] + (= op :def) + [:any (assoc node :init (nth (infer (get node :init) tenv) 1))] + (= op :try) + [:any (assoc node + :body (nth (infer (get node :body) tenv) 1) + :catch-body (when (get node :catch-body) (nth (infer (get node :catch-body) tenv) 1)) + :finally (when (get node :finally) (nth (infer (get node :finally) tenv) 1)))] + :else [:any node]))) + +(defn- infer-top [node] (nth (infer node {}) 1)) + (defn run-passes "All passes, in order. The back end applies this to every analyzed form. When inlining is enabled for the unit (user code under direct-linking, jolt-87f), run inline + flatten + scalar-replace + const-fold to a capped fixpoint — inlining exposes map literals to lookups, scalar-replace collapses them, which - may expose more. Otherwise (core + bootstrap) just const-fold, as before." + may expose more — then a collection-type inference pass (jolt-99x) that + auto-drops the lookup guard where the type is proven. Otherwise (core + + bootstrap) just const-fold, as before." [node ctx] (if (inline-enabled? ctx) - (loop [i 0 n (const-fold node)] - (reset! dirty false) - (let [n2 (const-fold (scalar-replace (flatten-lets (inline-node n ctx))))] - (if (and @dirty (< i 8)) - (recur (inc i) n2) - n2))) + (let [opt (loop [i 0 n (const-fold node)] + (reset! dirty false) + (let [n2 (const-fold (scalar-replace (flatten-lets (inline-node n ctx))))] + (if (and @dirty (< i 8)) + (recur (inc i) n2) + n2)))] + (infer-top opt)) (const-fold node))) diff --git a/test/integration/type-infer-test.janet b/test/integration/type-infer-test.janet new file mode 100644 index 0000000..016500a --- /dev/null +++ b/test/integration/type-infer-test.janet @@ -0,0 +1,54 @@ +# Static collection-type inference, Phase 0 (jolt-6sr): intra-procedural. +# The pass infers an expression's collection type from literals/arithmetic and +# flows it through let bindings and if-joins. Where a keyword-lookup subject is +# PROVEN to be a plain struct map it auto-drops the :jolt/type guard (the +# inference output is the same ^:struct channel as a manual hint); where the +# type is unknown it stays :any and keeps the dynamic guard (sound fallback). +# +# Note: Route 1 scalar-replacement already eliminates NON-escaping let-bound +# maps outright, so these cases force the map to ESCAPE (pass it to `sink`) to +# isolate what inference adds — typing a map that survives and is then looked up. +(import ../../src/jolt/api :as api) +(import ../../src/jolt/backend :as backend) +(import ../../src/jolt/reader :as reader) + +(print "Type inference Phase 0 (jolt-6sr)...") + +(os/setenv "JOLT_DIRECT_LINK" "1") +(def ctx (api/init {:compile? true})) +(api/eval-string ctx "(ns ti)") + +(defn guards [src] + (length (string/find-all ":jolt/type" + (string/format "%p" (backend/emit-ir ctx (backend/analyze-form ctx (reader/parse-string src))))))) +(defn ev [src] (api/eval-string ctx src)) + +# --- guard auto-removal where the type is proven, no hint ------------------- +# escaping struct-map literal (scalar keys, truthy values) is proven struct +(assert (= 0 (guards "(fn [sink] (let [v {:r 1 :g 2 :b 3}] (sink v) (:r v)))")) "inferred struct-map literal -> bare lookup") +# arithmetic values are provably non-nil/non-false -> still a struct +(assert (= 0 (guards "(fn [sink a b] (let [v {:r (+ a 1) :g (* b 2) :b 7}] (sink v) (:r v)))")) "arithmetic-valued map inferred struct") +# the inferred type flows through a rebinding +(assert (= 0 (guards "(fn [sink] (let [v {:r 1 :g 2} w v] (sink w) (:r w)))")) "inferred type flows through a rebinding") +# both if-branches struct -> join is struct +(assert (= 0 (guards "(fn [sink c] (let [v (if c {:a 1} {:a 2})] (sink v) (:a v)))")) "if-join of two struct literals stays struct") + +# --- sound fallback to the guard where the type is NOT proven --------------- +# a param is unknown (Phase 1 handles params) -> guard kept, exactly as today +(assert (= 1 (guards "(fn [m] (:r m))")) "unknown param keeps the guard") +# a value that could be nil/false makes the literal maybe-phm -> :any -> guard +(assert (= 1 (guards "(fn [sink x] (let [v {:r x}] (sink v) (:r v)))")) "maybe-nil value -> not proven struct -> guard") +# join of a struct and a phm is :any -> guard +(assert (>= (guards "(fn [sink c] (let [v (if c {:a 1} (hash-map :a nil))] (sink v) (:a v)))") 1) "struct/phm join -> :any -> guard") + +# --- correctness: every shape evaluates to the same as the guarded path ----- +(def snk "(fn [_] nil)") +(assert (= 1 (ev (string "((fn [sink] (let [v {:r 1 :g 2 :b 3}] (sink v) (:r v))) " snk ")"))) "struct literal value") +(assert (= 6 (ev (string "((fn [sink a] (let [v {:r (+ a 1)}] (sink v) (:r v))) " snk " 5)"))) "arithmetic-valued struct") +(assert (= 2 (ev (string "((fn [sink] (let [v {:r 1 :g 2} w v] (sink w) (:g w))) " snk ")"))) "flowed type value") +(assert (= 1 (ev (string "((fn [sink c] (let [v (if c {:a 1} {:a 2})] (sink v) (:a v))) " snk " true)"))) "if-join value") +(assert (= nil (ev (string "((fn [sink x] (let [v {:r x}] (sink v) (:r v))) " snk " nil)"))) "maybe-nil map reads correctly (nil)") +(assert (= nil (ev (string "((fn [sink c] (let [v (if c {:a 1} (hash-map :a nil))] (sink v) (:a v))) " snk " false)"))) "phm branch reads nil correctly") +(assert (= 1 (ev (string "((fn [sink c] (let [v (if c {:a 1} (hash-map :a nil))] (sink v) (:a v))) " snk " true)"))) "struct branch reads correctly") + +(print "Type inference Phase 0 passed!")