From c4be5d8a0e30b52d0cb2163837e92218039809e9 Mon Sep 17 00:00:00 2001 From: Yogthos Date: Fri, 12 Jun 2026 17:45:18 -0400 Subject: [PATCH 01/20] perf: hint-driven keyword-lookup guard elimination (^:struct) A constant-keyword lookup (:k m) currently emits a guarded form, (if (get m :jolt/type) (core-get m k) (get m k)), to tell a plain struct (raw get is correct) from a phm/sorted/transient (needs core-get). On a struct that guard is a second get, so the lookup costs ~36ns where a bare get is ~20ns. Profiling the ray tracer (jolt-dad) showed keyword lookups are ~50% of a render and the guard is the only avoidable part, but dropping it needs to know statically that the subject is a plain struct. Type hints are exactly that information, and jolt already parses them and otherwise ignores them. This wires one through: a local hinted ^:struct asserts a plain struct/record map, so a (:k local) lookup on it skips the guard and emits a bare get. The hint rides on the binding symbol into the analyzer, which records it per-local and attaches it to :local IR nodes; the back end reads it on the lookup subject. It also propagates through inlining: when the inliner let-binds a non-trivial arg to a fresh local, it carries the called fn's param hint onto that local, so lookups inside the spliced body keep the bare path. This is a programmer assertion, like a Clojure type hint (an inaccurate hint just makes the raw get return the wrong value, the same contract as a wrong ^String), so it stays opt-in and off by default. On the ray tracer (with inlining on) this is 13.3s to 10.9s, 1.22x, taking it to 7.8x JVM from 9.4x after the inline pass. The unhinted path emits identical code (the fast arm is just factored out), so nothing changes without hints. Verified: a seeded full render produces an identical checksum hinted vs unhinted; conformance 335/335 in all three modes and the full jpm test pass; new test/integration/struct-hint-test.janet pins the guard removal, the inline propagation, and that an accurate hint is correctness-preserving. --- jolt-core/jolt/analyzer.clj | 33 ++++++++++++++----- jolt-core/jolt/passes.clj | 10 +++++- src/jolt/backend.janet | 15 ++++++--- test/integration/struct-hint-test.janet | 44 +++++++++++++++++++++++++ 4 files changed, 89 insertions(+), 13 deletions(-) create mode 100644 test/integration/struct-hint-test.janet diff --git a/jolt-core/jolt/analyzer.clj b/jolt-core/jolt/analyzer.clj index 8840292..7d2a91c 100644 --- a/jolt-core/jolt/analyzer.clj +++ b/jolt-core/jolt/analyzer.clj @@ -39,11 +39,21 @@ (swap! gensym-counter inc) (str "_r$" prefix n))) -(defn- empty-env [] {:locals #{}}) +(defn- empty-env [] {:locals #{} :hints {}}) (defn- local? [env nm] (contains? (:locals env) nm)) (defn- add-locals [env names] (update env :locals #(reduce conj % names))) (defn- with-recur [env name] (assoc env :recur name)) +;; Type hints (jolt-dad). The reader keeps ^hint metadata on the binding symbol; +;; we recognize ^:struct, which asserts the value is a plain struct/record map so +;; a constant-keyword lookup can skip the :jolt/type guard and emit a bare get. +;; Other hints parse and are ignored, as before. +(defn- hint-of [sym] + (let [m (form-sym-meta sym)] + (when (and m (get m :struct)) :struct))) +(defn- add-hint [env nm h] + (if h (assoc env :hints (assoc (:hints env) nm h)) env)) + (defn- analyze-seq [ctx forms env] (let [v (mapv #(analyze ctx % env) forms) n (count v)] @@ -59,20 +69,25 @@ (when-not (form-sym? bsym) (uncompilable "destructuring binding")) (let [nm (form-sym-name bsym) init (analyze ctx (nth bvec (inc i)) env)] - (recur (+ i 2) (add-locals env [nm]) (conj pairs [nm init])))) + (recur (+ i 2) (add-hint (add-locals env [nm]) nm (hint-of bsym)) + (conj pairs [nm init])))) [pairs env]))) (defn- parse-params [pvec] - (loop [i 0 fixed [] rest-name nil] + ;; :hints is a vector of [name hint] pairs (vector, not a map, so the caller + ;; folds it with a plain reduce — no reduce-over-map in the kernel subset). + (loop [i 0 fixed [] rest-name nil hints []] (if (< i (count pvec)) (let [p (nth pvec i)] (when-not (form-sym? p) (uncompilable "destructuring fn param")) (if (= "&" (form-sym-name p)) (let [r (nth pvec (inc i))] (when-not (form-sym? r) (uncompilable "destructuring fn rest")) - (recur (+ i 2) fixed (form-sym-name r))) - (recur (inc i) (conj fixed (form-sym-name p)) rest-name))) - {:fixed fixed :rest rest-name}))) + (recur (+ i 2) fixed (form-sym-name r) hints)) + (let [nm (form-sym-name p) h (hint-of p)] + (recur (inc i) (conj fixed nm) rest-name + (if h (conj hints [nm h]) hints))))) + {:fixed fixed :rest rest-name :hints hints}))) (defn- analyze-arity [ctx pvec body env fn-name] (let [pp (parse-params (vec (form-vec-items pvec))) @@ -88,7 +103,8 @@ ;; keeps recur targets unique per compilation unit. rname (gen-name (str (compile-ns ctx) "/" (or fn-name "fn") "--")) names (cond-> (vec fixed) rst (conj rst) fn-name (conj fn-name)) - env* (-> (add-locals env names) (with-recur rname)) + env0 (-> (add-locals env names) (with-recur rname)) + env* (reduce (fn [e pr] (add-hint e (nth pr 0) (nth pr 1))) env0 (:hints pp)) arity {:params fixed :recur-name rname :body (analyze-seq ctx body env*)}] ;; :rest only when variadic — an absent :rest reads back nil, same as before, @@ -190,7 +206,8 @@ (defn- analyze-symbol [ctx form env] (let [nm (form-sym-name form) ns (form-sym-ns form)] (cond - (and (nil? ns) (local? env nm)) (local nm) + (and (nil? ns) (local? env nm)) + (let [h (get (:hints env) nm)] (if h (assoc (local nm) :hint h) (local nm))) ns (let [r (resolve-global ctx form)] (if (= :var (:kind r)) (var-ref (:ns r) (:name r)) diff --git a/jolt-core/jolt/passes.clj b/jolt-core/jolt/passes.clj index 1173088..76a7656 100644 --- a/jolt-core/jolt/passes.clj +++ b/jolt-core/jolt/passes.clj @@ -178,7 +178,15 @@ (let [op (get node :op)] (cond (= op :local) (let [r (get env (get node :name))] - (if r r node)) + ;; carry the param's ^:struct hint onto a let-bound fresh + ;; local, so lookups inside the inlined body keep the bare + ;; (no-guard) path (jolt-dad). The param hint asserts the + ;; arg is a struct; inlining doesn't change that contract. + (if r + (if (and (= :local (get r :op)) (get node :hint) (not (get r :hint))) + (assoc r :hint (get node :hint)) + r) + node)) (= op :if) (assoc node :test (subst (get node :test) env) :then (subst (get node :then) env) diff --git a/src/jolt/backend.janet b/src/jolt/backend.janet index ab2bd62..a2b9aae 100644 --- a/src/jolt/backend.janet +++ b/src/jolt/backend.janet @@ -331,6 +331,13 @@ (>= 2 (length args) 1)) (let [k (fnode :val) m-expr (in args 0) + # ^:struct hint (jolt-dad): the subject IR local asserts a plain + # struct/record map, so skip the :jolt/type guard entirely and emit a + # bare get (~20ns vs ~36ns guarded). Programmer-asserted, like a + # Clojure type hint — a lie just makes the raw get return the wrong + # thing, same contract as ^String. Only for a :local subject. + subj (norm-node (in (vview (node :args)) 0)) + hinted (and (= :local (subj :op)) (= :struct (subj :hint))) # when the subject is already a janet symbol (a local), read it # directly — the guard + lookup both reference it, and locals are # immutable reads, so no rebinding let is needed (saves a binding @@ -338,13 +345,13 @@ m (if (symbol? m-expr) m-expr (jsym)) wrap (fn [body] (if (symbol? m-expr) body ['let [m m-expr] body]))] (if (= 1 (length args)) - (wrap ['if ['get m :jolt/type] (tuple core-get m k) ['get m k]]) + (let [fast ['get m k]] + (wrap (if hinted fast ['if ['get m :jolt/type] (tuple core-get m k) fast]))) (let [d-expr (in args 1) d (if (symbol? d-expr) d-expr (jsym)) v (jsym) - body ['if ['get m :jolt/type] - (tuple core-get m k d) - ['let [v ['get m k]] ['if ['nil? v] d v]]] + fast ['let [v ['get m k]] ['if ['nil? v] d v]] + body (if hinted fast ['if ['get m :jolt/type] (tuple core-get m k d) fast]) body (if (symbol? d-expr) body ['let [d d-expr] body])] (wrap body)))) (direct-call? ctx fnode) (tuple (emit ctx fnode) ;args) diff --git a/test/integration/struct-hint-test.janet b/test/integration/struct-hint-test.janet new file mode 100644 index 0000000..bf433ce --- /dev/null +++ b/test/integration/struct-hint-test.janet @@ -0,0 +1,44 @@ +# ^:struct type hint (jolt-dad). A constant-keyword lookup on a local hinted +# ^:struct skips the :jolt/type guard and emits a bare get (~20ns vs ~36ns), +# the way Clojure type hints let the compiler specialize. The hint is a +# programmer assertion (a lie just makes the raw get return the wrong thing, +# same contract as ^String); these tests pin that an ACCURATE hint is +# correctness-preserving, that it drops the guard, and that it survives inlining. +(import ../../src/jolt/api :as api) +(import ../../src/jolt/backend :as backend) +(import ../../src/jolt/reader :as reader) + +(print "Struct hint (jolt-dad)...") + +(os/setenv "JOLT_DIRECT_LINK" "1") # inline on, so hint-through-inline is exercised +(def ctx (api/init {:compile? true})) +(api/eval-string ctx "(ns sh)") +(each s ["(defn v3 [r g b] {:r r :g g :b b})" + "(defn dot [^:struct l ^:struct r] (+ (+ (* (:r l) (:r r)) (* (:g l) (:g r))) (* (:b l) (:b r))))" + "(defn sub [^:struct l ^:struct r] {:r (- (:r l) (:r r)) :g (- (:g l) (:g r)) :b (- (:b l) (:b r))})" + "(defn lensq [^:struct v] (dot v v))"] + (api/eval-string ctx s)) + +(defn guards [src] + (def code (string/format "%p" (backend/emit-ir ctx (backend/analyze-form ctx (reader/parse-string src))))) + (length (string/find-all ":jolt/type" code))) + +# the guard is dropped for hinted subjects, kept for unhinted ones +(assert (= 1 (guards "(fn [v] (:r v))")) "unhinted (:r v) keeps the guard") +(assert (= 0 (guards "(fn [^:struct v] (:r v))")) "hinted (:r v) drops the guard") +(assert (= 0 (guards "(fn [^:struct v] (+ (+ (:r v) (:g v)) (:b v)))")) "all three hinted lookups bare") +(assert (= 0 (guards "(fn [^:struct v] (lensq v))")) "hint survives through an inlined call") + +# accurate hints are correctness-preserving (value identical to the guarded path) +(assert (= 32 (api/eval-string ctx "(dot (v3 1 2 3) (v3 4 5 6))")) "hinted dot value") +(assert (= 14 (api/eval-string ctx "(lensq (v3 1 2 3))")) "hinted lensq (inline-flow) value") +(assert (= 7 (api/eval-string ctx "(:r (sub (v3 9 8 7) (v3 2 0 0)))")) "hinted sub field") +# a hinted value flowing through an inlined call still reads correctly +(api/eval-string ctx "(defn hit [^:struct ray ^:struct c] (lensq (sub (:origin ray) c)))") +(assert (= 48 (api/eval-string ctx "(hit {:origin (v3 5 5 5) :direction (v3 0 0 0)} (v3 1 1 1))")) + "hinted value through nested inline reads correctly") + +# a missing key on a hinted struct still reads nil (struct miss), like a guarded get +(assert (= nil (api/eval-string ctx "((fn [^:struct m] (:absent m)) (v3 1 2 3))")) "hinted struct miss -> nil") + +(print "Struct hint passed!") From 5f59c02b694a829ae8f5b9bb3a7417ebe08611fd Mon Sep 17 00:00:00 2001 From: Yogthos Date: Fri, 12 Jun 2026 20:20:25 -0400 Subject: [PATCH 02/20] feat: expand type-hint lookup specialization (^Record, get-form, checked mode, docs) Builds on the ^:struct keyword-lookup hint: - ^TypeName for records. A tag naming a defrecord/deftype now resolves to the struct fast path: record instances are tables tagged :jolt/deftype (not :jolt/type), so a raw keyword get is correct for them. A new host contract fn record-type? detects a record by its ->Name constructor; a non-record tag (^String, ^long, ...) is ignored, as before. - (get m :k) and (get m :k default) now get the same inlined keyword lookup as (:k m): the representation guard fast path when unhinted, and the bare get when the subject is ^:struct/^Record. A variable/number/string key still falls through to core-get. The two call shapes share one emitter (emit-kw-lookup). - JOLT_CHECK_HINTS=1 turns a violated hint into a clear runtime error (naming the local and key) by keeping the guard and throwing on the tagged arm. It is off by default with zero cost to normal builds (a hinted lookup still emits a bare get), and is part of the image-cache fingerprint. This is the answer to "a lying hint is silent": opt into checking during development. - Docs: RFC 0004 records the design, soundness contract, and measurements; the reader spec gains S12b (hints are semantically transparent; jolt recognizes ^:struct and ^Record as lookup-optimization assertions). There is no Clojure keyword equivalent for "plain map / fast keyword access" (Clojure hints are class names), so ^:struct stays a jolt-specific flag, analogous to ^:dynamic. Verified: conformance 335/335 in all three modes and the full jpm test pass; a seeded ray-tracer render is byte-identical hinted vs unhinted; the struct-hint test covers record hints, the get-form, inline propagation, and the checked-mode error. Full render with hints holds at 13.3s -> 10.9s (1.22x). --- docs/rfc/0004-type-hints.md | 128 ++++++++++++++++++++++++ docs/spec/02-reader.md | 10 ++ jolt-core/jolt/analyzer.clj | 29 ++++-- src/jolt/api.janet | 5 +- src/jolt/backend.janet | 84 +++++++++++----- src/jolt/host_iface.janet | 15 ++- test/integration/struct-hint-test.janet | 59 ++++++++--- 7 files changed, 276 insertions(+), 54 deletions(-) create mode 100644 docs/rfc/0004-type-hints.md diff --git a/docs/rfc/0004-type-hints.md b/docs/rfc/0004-type-hints.md new file mode 100644 index 0000000..4c84837 --- /dev/null +++ b/docs/rfc/0004-type-hints.md @@ -0,0 +1,128 @@ +# RFC 0004: Type hints and keyword-lookup specialization + +Status: accepted (design note) + +This note describes how Jolt treats Clojure type hints, and the one place it +uses them: a `^:struct` or `^Record` hint on a local lets a constant-keyword +lookup skip its runtime representation guard. It records the rationale, the +soundness contract, the checked mode for catching inaccurate hints, and the +measured effect, so later work does not relitigate it. + +## Background: why the lookup carries a guard + +A Jolt map value has several runtime representations (see RFC on collections and +`src/jolt/core.janet`): a Janet struct for a small all-scalar-key literal map, a +persistent hash map (a table tagged `:jolt/type :jolt/phm`) when a key is a +collection or a value is nil, plus sorted maps, transients, and record/deftype +instances. A record instance is a Janet table tagged `:jolt/deftype` but, like a +struct, it carries no `:jolt/type`, so a raw Janet `(get inst :field)` reads its +fields directly. + +A constant-keyword lookup `(:k m)` compiles to a guarded form: + +```janet +(if (get m :jolt/type) (core-get m k) (get m k)) +``` + +The guard is one opcode. A non-nil `:jolt/type` routes phm/sorted/transient/ +lazy-seq values to `core-get`'s full semantics; everything else (structs, +records, nil, scalars) takes the bare Janet `get`, which matches `core-get` for +keyword keys. The guard is correct and cheap, but on a struct it is a second +`get`: profiling the ray tracer (a naive all-maps program) found keyword lookups +are about half of a render, and the guard is the only avoidable part of each +one. A bare get is roughly 20ns where the guarded form is roughly 36ns. + +Dropping the guard is only safe when the subject is known to be a plain +struct/record rather than a tagged collection. Jolt does not infer that +inter-procedurally (it would be unsound across a dynamic language's call +boundaries). A type hint supplies the same fact soundly, as a programmer +assertion. + +## What the hints mean + +Two hints on a local resolve to the "plain struct/record" assertion, which we +call the `:struct` hint internally: + +- `^:struct` — the value is a plain struct or record map. There is no Clojure + keyword with this meaning (Clojure's type hints are class names), so this is a + Jolt-specific metadata flag, analogous to `^:dynamic`. +- `^Name` where `Name` is a `defrecord`/`deftype`. Both forms define a `->Name` + positional constructor, so the analyzer treats a tag whose `->Name` resolves + as a record type. Record instances are raw-get-safe, so the lookup drops the + guard. A `^String`, `^long`, or any other non-record tag is not a record and + is ignored, exactly as before. + +Every other hint parses and is inert, matching Clojure (S12b in the reader +spec). A hint never changes a program's result; it only permits an +optimization. + +## How it flows + +The reader already keeps `^hint` metadata on the binding symbol and is otherwise +transparent (`reader.janet`, `meta-form->map`). The change threads that fact to +the lookup site: + +1. The analyzer (`jolt-core/jolt/analyzer.clj`) records a `:struct` hint per + local in its env when a param or `let` binding carries `^:struct` or a + record-type tag, and attaches `:hint :struct` to that local's `:local` IR + node. Resolving a record-type tag uses a new host contract function + `record-type?` (`src/jolt/host_iface.janet`), which checks for the `->Name` + constructor. +2. The back end (`emit-kw-lookup` in `src/jolt/backend.janet`) emits the bare get + when the lookup subject is a `:local` carrying the hint, and the guarded form + otherwise. The unhinted path is byte-identical to before. +3. The inline pass (`jolt-core/jolt/passes.clj`) propagates the hint: when it + binds a non-trivial call argument to a fresh local, it carries the called + function's parameter hint onto that local, so lookups inside the spliced body + keep the bare path. Without this, inlining a hinted function would erase the + benefit, because the hinted parameter is replaced by an unhinted temporary. + +The same machinery covers both `(:k m)` and `(get m :k [default])` when the key +is a constant keyword. A `get` with a variable, numeric, or string key falls +through to `core-get` unchanged. + +## Soundness and the checked mode + +An accurate hint is correctness-preserving by construction: for a struct or +record the bare get equals the guarded result. An inaccurate hint (asserting +`^:struct` for a value that is actually a phm) makes the raw get return the wrong +thing. This is the same contract as a wrong Clojure `^String`, except that a +wrong Jolt hint fails silently rather than throwing. + +To make a lie visible without taxing the fast path, `JOLT_CHECK_HINTS=1` keeps +the guard but throws on the tagged arm with a message naming the local and key: + +``` +type hint violated on `m`: (:a m) — value carries :jolt/type +(a phm/sorted/transient/lazy-seq), not the plain struct/record the +^:struct/^Record hint asserts +``` + +This is a development aid, off by default, with zero cost to normal builds (the +flag is read when the lookup is compiled, and the bare get is emitted when it is +off). The flag is part of the image-cache fingerprint. + +## Coverage + +Type hints parse in every position Clojure accepts them and are inert except for +the optimization above. This matches Clojure's "parse and otherwise do nothing" +model, with the difference that Clojure additionally uses hints to avoid +reflection and select primitive arithmetic, which do not apply to a Janet host. + +## Measured effect + +On the ray tracer (`~/src/examples/ray-tracer`, all values are `{:r :g :b}`-style +maps), with inlining on and the hot parameters hinted, a render goes from 13.3s +to 10.9s, about 1.22x, taking it to roughly 7.8x the JVM from 9.4x after the +inline pass. A seeded render produces an identical pixel checksum hinted and +unhinted, confirming the hints are correctness-preserving on the full pipeline. + +## Status and non-goals + +Implemented. Not pursued: inter-procedural shape inference (unsound in a dynamic +language without a guard, which costs as much as the one being removed) and a +shape-based "hidden class" representation (profiling showed allocation is about +1% of the workload, so a cheaper allocation would not help, and an escaping-map +lookup through a runtime shape check costs about the same as the guard it would +replace). The hint is the sound, opt-in lever on the part of the cost that can +move. diff --git a/docs/spec/02-reader.md b/docs/spec/02-reader.md index 67e4500..7d9962b 100644 --- a/docs/spec/02-reader.md +++ b/docs/spec/02-reader.md @@ -83,6 +83,16 @@ checks → UNVERIFIED (rows to add). - S12a. `^:kw form` ≡ `^{:kw true} form`; `^Sym form` ≡ `^{:tag Sym} form`; `^"str"` ≡ `^{:tag "str"} form`. Multiple `^` stack, rightmost innermost, merged left-over-right. +- S12b. Type hints are semantically transparent: a hint MUST NOT change a + program's result. Hints parse in every position they do in Clojure (params, + `let` bindings, `def` names, return position, arbitrary forms) and are + otherwise inert. As a non-normative optimization, jolt recognizes two hints + on a local as an assertion that a constant-keyword lookup may skip its + runtime representation guard: `^:struct` (a plain struct/record map) and + `^Name` where `Name` is a `defrecord`/`deftype`. The assertion is the + programmer's (an inaccurate hint yields a wrong lookup, like a wrong Clojure + `^String`); `JOLT_CHECK_HINTS=1` turns a violated hint into an error at no + cost to unchecked builds. See RFC 0004. - S13a. `#'ns/sym` MUST denote the same var as `(var ns/sym)`: `(= (var clojure.core/str) #'clojure.core/str)` is true. diff --git a/jolt-core/jolt/analyzer.clj b/jolt-core/jolt/analyzer.clj index 7d2a91c..2ce9f44 100644 --- a/jolt-core/jolt/analyzer.clj +++ b/jolt-core/jolt/analyzer.clj @@ -22,7 +22,8 @@ form-literal? form-elements form-vec-items form-map-pairs form-set-items form-special? compile-ns form-macro? form-expand-1 resolve-global - form-sym-meta host-intern! form-syntax-quote-lower]])) + form-sym-meta host-intern! form-syntax-quote-lower + record-type?]])) (declare analyze) @@ -44,13 +45,19 @@ (defn- add-locals [env names] (update env :locals #(reduce conj % names))) (defn- with-recur [env name] (assoc env :recur name)) -;; Type hints (jolt-dad). The reader keeps ^hint metadata on the binding symbol; -;; we recognize ^:struct, which asserts the value is a plain struct/record map so -;; a constant-keyword lookup can skip the :jolt/type guard and emit a bare get. -;; Other hints parse and are ignored, as before. -(defn- hint-of [sym] +;; Type hints (jolt-94n). The reader keeps ^hint metadata on the binding symbol. +;; Two hints resolve to the :struct fast path (a constant-keyword lookup skips +;; the :jolt/type guard and emits a bare get): ^:struct (a plain struct/record +;; map) and ^TypeName where TypeName is a defrecord/deftype (its instances are +;; tagged :jolt/deftype, not :jolt/type, so a raw get is correct). Every other +;; hint (^String, ^long, ...) parses and is ignored, as before. +(defn- hint-of [ctx sym] (let [m (form-sym-meta sym)] - (when (and m (get m :struct)) :struct))) + (cond + (nil? m) nil + (get m :struct) :struct + :else (let [t (get m :tag)] + (when (and t (record-type? ctx t)) :struct))))) (defn- add-hint [env nm h] (if h (assoc env :hints (assoc (:hints env) nm h)) env)) @@ -69,11 +76,11 @@ (when-not (form-sym? bsym) (uncompilable "destructuring binding")) (let [nm (form-sym-name bsym) init (analyze ctx (nth bvec (inc i)) env)] - (recur (+ i 2) (add-hint (add-locals env [nm]) nm (hint-of bsym)) + (recur (+ i 2) (add-hint (add-locals env [nm]) nm (hint-of ctx bsym)) (conj pairs [nm init])))) [pairs env]))) -(defn- parse-params [pvec] +(defn- parse-params [ctx pvec] ;; :hints is a vector of [name hint] pairs (vector, not a map, so the caller ;; folds it with a plain reduce — no reduce-over-map in the kernel subset). (loop [i 0 fixed [] rest-name nil hints []] @@ -84,13 +91,13 @@ (let [r (nth pvec (inc i))] (when-not (form-sym? r) (uncompilable "destructuring fn rest")) (recur (+ i 2) fixed (form-sym-name r) hints)) - (let [nm (form-sym-name p) h (hint-of p)] + (let [nm (form-sym-name p) h (hint-of ctx p)] (recur (inc i) (conj fixed nm) rest-name (if h (conj hints [nm h]) hints))))) {:fixed fixed :rest rest-name :hints hints}))) (defn- analyze-arity [ctx pvec body env fn-name] - (let [pp (parse-params (vec (form-vec-items pvec))) + (let [pp (parse-params ctx (vec (form-vec-items pvec))) fixed (:fixed pp) rst (:rest pp) ;; Always a recur target, variadic included: the back end gives the rest diff --git a/src/jolt/api.janet b/src/jolt/api.janet index b4c9e8f..cb84cb0 100644 --- a/src/jolt/api.janet +++ b/src/jolt/api.janet @@ -296,7 +296,7 @@ # Opts land in the key via their printed form; an opt that prints unstably # (e.g. a closure in :namespaces) just degrades to a cache miss, never to a # wrong hit. Runtime knobs that shape the ctx outside opts ride along too. - (def key (string/format "%q|%q|%q|%q|%q|%q|%q|%q|%q" + (def key (string/format "%q|%q|%q|%q|%q|%q|%q|%q|%q|%q" (string janet/version "-" janet/build) opts (os/getenv "JOLT_PATH") @@ -305,7 +305,8 @@ (os/getenv "JOLT_FEATURES") (os/getenv "JOLT_INTERPRET_MACROS") (os/getenv "JOLT_DIRECT_LINK") - (os/getenv "JOLT_NO_IR_PASSES"))) + (os/getenv "JOLT_NO_IR_PASSES") + (os/getenv "JOLT_CHECK_HINTS"))) (string dir "/jolt-ctx-" (band h 0x7FFFFFFF) "-" len "-" (band (hash key) 0x7FFFFFFF) ".jimg")) (defn init-cached diff --git a/src/jolt/backend.janet b/src/jolt/backend.janet index a2b9aae..04c324f 100644 --- a/src/jolt/backend.janet +++ b/src/jolt/backend.janet @@ -304,10 +304,55 @@ (var- fp-counter 0) (defn- jsym [] (symbol "_fp$" (++ fp-counter))) +# Is fnode a reference to clojure.core/get (or a host `get`)? Used to give +# (get m :kw [d]) the same inlined keyword-lookup treatment as (:kw m [d]). +(defn- get-head? [fnode] + (case (fnode :op) + :var (and (= "clojure.core" (fnode :ns)) (= "get" (fnode :name))) + :host (= "get" (fnode :name)) + false)) + +# Shared emit for a constant-keyword map lookup — both (:kw m [d]) and +# (get m :kw [d]). subj-node is the subject's IR node (carries the type hint), +# m-expr its emitted form, k the keyword, d-expr the emitted default or nil. +# - unhinted: GUARDED — (if (get m :jolt/type) (core-get …) (bare get)). The +# guard (one opcode) routes tagged reps (phm/sorted/transient/lazy-seq) to +# core-get; a plain struct/record (no :jolt/type) takes the bare get, which +# matches core-get for keyword keys. +# - ^:struct / ^Record hinted subject: skip the guard, bare get (~20 vs ~36ns). +# - hinted + JOLT_CHECK_HINTS: keep the guard but THROW on the tagged arm, so a +# lying hint surfaces a clear error (dev aid; off by default, no perf cost). +(defn- emit-kw-lookup [subj-node m-expr k d-expr] + (def hinted (and subj-node (= :local (subj-node :op)) (= :struct (subj-node :hint)))) + (def checked (and hinted (os/getenv "JOLT_CHECK_HINTS"))) + (def m (if (symbol? m-expr) m-expr (jsym))) + (def wrap (fn [body] (if (symbol? m-expr) body ['let [m m-expr] body]))) + (def err (when checked + ['error (string "type hint violated on `" (subj-node :name) "`: (" + k " " (subj-node :name) ") — value carries :jolt/type " + "(a phm/sorted/transient/lazy-seq), not the plain " + "struct/record the ^:struct/^Record hint asserts")])) + (if (nil? d-expr) + (let [fast ['get m k]] + (wrap (cond + checked ['if ['get m :jolt/type] err fast] + hinted fast + ['if ['get m :jolt/type] (tuple core-get m k) fast]))) + (let [d (if (symbol? d-expr) d-expr (jsym)) + v (jsym) + fast ['let [v ['get m k]] ['if ['nil? v] d v]] + body (cond + checked ['if ['get m :jolt/type] err fast] + hinted fast + ['if ['get m :jolt/type] (tuple core-get m k d) fast]) + body (if (symbol? d-expr) body ['let [d d-expr] body])] + (wrap body)))) + (defn- emit-invoke [ctx node] (def fnode (norm-node (node :fn))) (def args (map |(emit ctx $) (vview (node :args)))) (def nop (native-op fnode (length args))) + (def argnodes (vview (node :args))) (cond nop (case nop '++ ['+ (in args 0) 1] @@ -326,34 +371,21 @@ # records with direct field keys, nil, janet arrays, scalars) gets janet # `get` semantics, which match core-get for keyword keys. Structs never # store nil values (nil values force the phm rep), so present-but-nil - # can't be confused with missing on the fast arm. + # can't be confused with missing on the fast arm. A ^:struct/^Record hint on + # the subject skips the guard entirely (jolt-94n; see emit-kw-lookup). (and (= :const (fnode :op)) (keyword? (fnode :val)) (>= 2 (length args) 1)) - (let [k (fnode :val) - m-expr (in args 0) - # ^:struct hint (jolt-dad): the subject IR local asserts a plain - # struct/record map, so skip the :jolt/type guard entirely and emit a - # bare get (~20ns vs ~36ns guarded). Programmer-asserted, like a - # Clojure type hint — a lie just makes the raw get return the wrong - # thing, same contract as ^String. Only for a :local subject. - subj (norm-node (in (vview (node :args)) 0)) - hinted (and (= :local (subj :op)) (= :struct (subj :hint))) - # when the subject is already a janet symbol (a local), read it - # directly — the guard + lookup both reference it, and locals are - # immutable reads, so no rebinding let is needed (saves a binding - # per lookup in exactly the hottest shape, (:k local)) - m (if (symbol? m-expr) m-expr (jsym)) - wrap (fn [body] (if (symbol? m-expr) body ['let [m m-expr] body]))] - (if (= 1 (length args)) - (let [fast ['get m k]] - (wrap (if hinted fast ['if ['get m :jolt/type] (tuple core-get m k) fast]))) - (let [d-expr (in args 1) - d (if (symbol? d-expr) d-expr (jsym)) - v (jsym) - fast ['let [v ['get m k]] ['if ['nil? v] d v]] - body (if hinted fast ['if ['get m :jolt/type] (tuple core-get m k d) fast]) - body (if (symbol? d-expr) body ['let [d d-expr] body])] - (wrap body)))) + (emit-kw-lookup (norm-node (in argnodes 0)) (in args 0) (fnode :val) + (when (= 2 (length args)) (in args 1))) + # (get m :kw) / (get m :kw default) — same inlined keyword lookup as (:kw m), + # so an explicit get with a constant keyword gets the guard fast path and the + # ^:struct/^Record hint (jolt-94n). Only when the key is a constant keyword; + # a variable/number/string key falls through to core-get below. + (and (get-head? fnode) (>= (length args) 2) (<= (length args) 3) + (let [a1 (norm-node (in argnodes 1))] (and (= :const (a1 :op)) (keyword? (a1 :val))))) + (emit-kw-lookup (norm-node (in argnodes 0)) (in args 0) + ((norm-node (in argnodes 1)) :val) + (when (= 3 (length args)) (in args 2))) (direct-call? ctx fnode) (tuple (emit ctx fnode) ;args) # Local callee (closure param, let-bound fn, defn self-name): inline the # function check so the overwhelmingly-common function case is a direct diff --git a/src/jolt/host_iface.janet b/src/jolt/host_iface.janet index 55a05d3..aed1a76 100644 --- a/src/jolt/host_iface.janet +++ b/src/jolt/host_iface.janet @@ -219,6 +219,18 @@ (not (let [m (cell :meta)] (and m (get m :redef))))) (cell :inline-ir)))) +# Is `name` (a bare type-name string, e.g. "Vec3") a defrecord/deftype? Both +# expand to define a ->Name positional constructor var (30-macros.clj), so its +# presence is the marker. Lets the analyzer resolve a ^Record type hint to the +# struct fast path: record instances are tables tagged :jolt/deftype (NOT +# :jolt/type), so a raw keyword get is correct for them (jolt-94n). +(defn h-record-type? [ctx name] + (def ctor (string "->" name)) + (def cns (ctx-find-ns ctx (h-current-ns ctx))) + (if (or (and cns (ns-find cns ctor)) + (ns-find (ctx-find-ns ctx "clojure.core") ctor)) + true false)) + (def- exports {"form-sym?" h-sym? "form-sym-name" h-sym-name "form-sym-ns" h-sym-ns "ref-put!" h-ref-put! @@ -233,7 +245,8 @@ "form-expand-1" h-expand-1 "resolve-global" h-resolve-global "form-syntax-quote-lower" h-syntax-quote-lower "host-intern!" h-intern! - "inline-enabled?" h-inline-enabled? "inline-ir" h-inline-ir}) + "inline-enabled?" h-inline-enabled? "inline-ir" h-inline-ir + "record-type?" h-record-type?}) (defn install! [ctx] (def ns (ctx-find-ns ctx "jolt.host")) diff --git a/test/integration/struct-hint-test.janet b/test/integration/struct-hint-test.janet index bf433ce..a13cf9d 100644 --- a/test/integration/struct-hint-test.janet +++ b/test/integration/struct-hint-test.janet @@ -1,18 +1,21 @@ -# ^:struct type hint (jolt-dad). A constant-keyword lookup on a local hinted -# ^:struct skips the :jolt/type guard and emits a bare get (~20ns vs ~36ns), -# the way Clojure type hints let the compiler specialize. The hint is a -# programmer assertion (a lie just makes the raw get return the wrong thing, -# same contract as ^String); these tests pin that an ACCURATE hint is -# correctness-preserving, that it drops the guard, and that it survives inlining. +# Type hints driving keyword-lookup specialization (jolt-94n). A local hinted +# ^:struct (a plain struct/record map) or ^Record (a defrecord/deftype) lets a +# constant-keyword lookup skip the :jolt/type guard and emit a bare get +# (~20ns vs ~36ns), the way Clojure type hints let the compiler specialize. +# Covers both (:k m) and (get m :k), hint propagation through inlining, the +# ^Record path, the JOLT_CHECK_HINTS dev aid, and that accurate hints preserve +# results. An inaccurate hint is a programmer error (like a wrong ^String): the +# raw get returns the wrong value, surfaced only under JOLT_CHECK_HINTS. (import ../../src/jolt/api :as api) (import ../../src/jolt/backend :as backend) (import ../../src/jolt/reader :as reader) -(print "Struct hint (jolt-dad)...") +(print "Type hints (jolt-94n)...") (os/setenv "JOLT_DIRECT_LINK" "1") # inline on, so hint-through-inline is exercised (def ctx (api/init {:compile? true})) (api/eval-string ctx "(ns sh)") +(api/eval-string ctx "(defrecord Vec3r [r g b])") (each s ["(defn v3 [r g b] {:r r :g g :b b})" "(defn dot [^:struct l ^:struct r] (+ (+ (* (:r l) (:r r)) (* (:g l) (:g r))) (* (:b l) (:b r))))" "(defn sub [^:struct l ^:struct r] {:r (- (:r l) (:r r)) :g (- (:g l) (:g r)) :b (- (:b l) (:b r))})" @@ -23,22 +26,50 @@ (def code (string/format "%p" (backend/emit-ir ctx (backend/analyze-form ctx (reader/parse-string src))))) (length (string/find-all ":jolt/type" code))) -# the guard is dropped for hinted subjects, kept for unhinted ones +# --- guard removal ---------------------------------------------------------- (assert (= 1 (guards "(fn [v] (:r v))")) "unhinted (:r v) keeps the guard") -(assert (= 0 (guards "(fn [^:struct v] (:r v))")) "hinted (:r v) drops the guard") +(assert (= 0 (guards "(fn [^:struct v] (:r v))")) "^:struct (:r v) drops the guard") +(assert (= 0 (guards "(fn [^Vec3r v] (:r v))")) "^Record (:r v) drops the guard") +(assert (= 1 (guards "(fn [^String v] (:r v))")) "^String (not a record) still guards") (assert (= 0 (guards "(fn [^:struct v] (+ (+ (:r v) (:g v)) (:b v)))")) "all three hinted lookups bare") (assert (= 0 (guards "(fn [^:struct v] (lensq v))")) "hint survives through an inlined call") +# (get m :k) gets the same treatment as (:k m) +(assert (= 1 (guards "(fn [m] (get m :k))")) "unhinted (get m :k) is guarded-inline") +(assert (= 0 (guards "(fn [^:struct m] (get m :k))")) "^:struct (get m :k) drops the guard") +(assert (= 0 (guards "(fn [^Vec3r m] (get m :k 0))")) "^Record (get m :k d) drops the guard") +# a variable (non-constant) key isn't a keyword literal, so the inline doesn't +# fire — it falls through to core-get, which still indexes correctly. +(assert (= 2 (api/eval-string ctx "((fn [m kk] (get m kk)) {:a 2} :a)")) "variable-key get via core-get") +(assert (= 10 (api/eval-string ctx "((fn [m i] (get m i)) [10 20] 0)")) "variable-key get indexes a vector") -# accurate hints are correctness-preserving (value identical to the guarded path) +# --- correctness (accurate hints preserve results) -------------------------- (assert (= 32 (api/eval-string ctx "(dot (v3 1 2 3) (v3 4 5 6))")) "hinted dot value") (assert (= 14 (api/eval-string ctx "(lensq (v3 1 2 3))")) "hinted lensq (inline-flow) value") (assert (= 7 (api/eval-string ctx "(:r (sub (v3 9 8 7) (v3 2 0 0)))")) "hinted sub field") -# a hinted value flowing through an inlined call still reads correctly (api/eval-string ctx "(defn hit [^:struct ray ^:struct c] (lensq (sub (:origin ray) c)))") (assert (= 48 (api/eval-string ctx "(hit {:origin (v3 5 5 5) :direction (v3 0 0 0)} (v3 1 1 1))")) "hinted value through nested inline reads correctly") - -# a missing key on a hinted struct still reads nil (struct miss), like a guarded get (assert (= nil (api/eval-string ctx "((fn [^:struct m] (:absent m)) (v3 1 2 3))")) "hinted struct miss -> nil") +(assert (= 9 (api/eval-string ctx "((fn [^:struct m] (get m :absent 9)) (v3 1 2 3))")) "hinted get default") +# field access on a real record instance through a ^Record hint +(api/eval-string ctx "(defn vr-x [^Vec3r v] (:r v))") +(assert (= 5 (api/eval-string ctx "(vr-x (->Vec3r 5 6 7))")) "record field via ^Record hint") +# (get m :k) on assorted reps still matches core-get semantics (unhinted path) +(assert (= 2 (api/eval-string ctx "(get {:a 2} :a)")) "get struct present") +(assert (= nil (api/eval-string ctx "(get {:a 2} :z)")) "get struct miss") +(assert (= 1 (api/eval-string ctx "(get (hash-map :a 1 :x nil) :a)")) "get phm present") +(assert (= nil (api/eval-string ctx "(get (hash-map :a 1 :x nil) :x)")) "get phm nil value") +(assert (= 7 (api/eval-string ctx "(get (sorted-map :a 7) :a)")) "get sorted present") -(print "Struct hint passed!") +# --- checked mode: a lying hint throws (separate ctx with the flag on) ------- +(os/setenv "JOLT_CHECK_HINTS" "1") +(def cctx (api/init {:compile? true})) +(api/eval-string cctx "(ns ck)") +(api/eval-string cctx "(defn rd [^:struct m] (:a m))") +(assert (= 1 (api/eval-string cctx "(rd {:a 1 :b 2})")) "checked mode: accurate hint still works") +(let [r (protect (api/eval-string cctx "(rd (hash-map :a 1 :x nil))"))] + (assert (not (r 0)) "checked mode: lying ^:struct hint throws") + (assert (string/find "type hint violated" (string (r 1))) "checked-mode error is meaningful")) +(os/setenv "JOLT_CHECK_HINTS" nil) + +(print "Type hints passed!") From 4b44bcd5fdec3b3133c881d066d7190108e8f1ec Mon Sep 17 00:00:00 2001 From: Yogthos Date: Fri, 12 Jun 2026 20:25:15 -0400 Subject: [PATCH 03/20] test: cover ^:struct on let bindings (jolt-94n) --- test/integration/struct-hint-test.janet | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/test/integration/struct-hint-test.janet b/test/integration/struct-hint-test.janet index a13cf9d..f91ffa0 100644 --- a/test/integration/struct-hint-test.janet +++ b/test/integration/struct-hint-test.janet @@ -33,6 +33,10 @@ (assert (= 1 (guards "(fn [^String v] (:r v))")) "^String (not a record) still guards") (assert (= 0 (guards "(fn [^:struct v] (+ (+ (:r v) (:g v)) (:b v)))")) "all three hinted lookups bare") (assert (= 0 (guards "(fn [^:struct v] (lensq v))")) "hint survives through an inlined call") +# hints work on let bindings too, not just params (init is a plain local here, +# so the only candidate guard is the hinted (:r v)) +(assert (= 0 (guards "(fn [^:struct s] (let [^:struct v s] (:r v)))")) "^:struct on a let binding drops the guard") +(assert (= 1 (guards "(fn [s] (let [v s] (:r v)))")) "unhinted let binding keeps the guard") # (get m :k) gets the same treatment as (:k m) (assert (= 1 (guards "(fn [m] (get m :k))")) "unhinted (get m :k) is guarded-inline") (assert (= 0 (guards "(fn [^:struct m] (get m :k))")) "^:struct (get m :k) drops the guard") From 3c20383851b0cd939749bc83615340313b1b1fec Mon Sep 17 00:00:00 2001 From: Yogthos Date: Sat, 13 Jun 2026 01:46:34 -0400 Subject: [PATCH 04/20] 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!") From ea1d9a23e1c977eefbc9ca3dc2c0d4460b297748 Mon Sep 17 00:00:00 2001 From: Yogthos Date: Sat, 13 Jun 2026 04:45:13 -0400 Subject: [PATCH 05/20] feat: Phase 1 inter-procedural collection-type inference (jolt-767) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Closed-world (optimization mode): after a unit loads, infer-unit! runs a whole-unit fixpoint over the call graph and recompiles. A fn's param types are the lub of its in-unit call-site arg types; its return type is the lub of its tail positions; iterated to a least fixpoint. Param types are RECOMPUTED FRESH each iteration (not accumulated) because :any is the lattice top — joining an early-iteration :any would poison the result permanently. Closures inherit the enclosing tenv so captured locals keep their types (their own params shadow to :any). A fn whose var escapes as a VALUE keeps :any params (its callers aren't all visible). Each fn is then re-inferred with its param types seeded and re-emitted; recompiled bodies are semantically identical, so correctness holds regardless of order. Sound under source distribution + whole-program compile (the consumer compiles all call sites together). Plumbing: the portable pass (jolt.passes) gained inter-procedural primitives — set-rtenv!, infer-body (types a body, collects its call sites), reinfer-def (seeds param types), and escape tracking. The back end stashes each single-fixed-arity defn's :def IR (:infer-ir); the evaluator triggers infer-unit! after a unit loads (via an env hook, opt mode only). Result and honest finding: the fixpoint correctly types scalar-flowing params (ray-cast/hit-all/hit-sphere all get the ray param as :struct-map, no hint), but the ray tracer does NOT speed up — its dominant lookups are on `hittable`, the element of the `hittables` vector threaded through `reduce`, which stays :any. Typing it needs collection-element types (vector) plus HOF-element awareness (knowing reduce applies the closure to elements), which is beyond inter-procedural param inference. The explicit ^:struct hint reaches it (it types the reduce closure param directly), which is why the hinted run is 1.22x. Verified: conformance 335/335 x3, full jpm test; new type-infer-phase1-test pins the fixpoint, the escape gate, the seeded re-inference, and correctness. --- jolt-core/jolt/passes.clj | 89 ++++++++++++-- src/jolt/api.janet | 4 + src/jolt/backend.janet | 109 +++++++++++++++++- src/jolt/evaluator.janet | 8 ++ test/integration/type-infer-phase1-test.janet | 54 +++++++++ 5 files changed, 251 insertions(+), 13 deletions(-) create mode 100644 test/integration/type-infer-phase1-test.janet diff --git a/jolt-core/jolt/passes.clj b/jolt-core/jolt/passes.clj index 5e73c06..eecba2d 100644 --- a/jolt-core/jolt/passes.clj +++ b/jolt-core/jolt/passes.clj @@ -731,15 +731,31 @@ "bit-and" "bit-or" "bit-xor" "count"}) (def ^:private vector-ret-fns #{"vec" "vector" "mapv" "filterv" "subvec"}) +;; Inter-procedural state (jolt-767, Phase 1). The Janet orchestrator (backend +;; infer-unit!) drives a whole-unit fixpoint: before typing a fn body it installs +;; the current return-type estimates of all unit fns here, and after typing it +;; reads back the call sites this body made (callee + inferred arg types) to +;; propagate into callee param types. Both are plain module state, like `dirty`. +(def ^:private rtenv-box (atom {})) ;; "ns/name" -> inferred return type +(def ^:private calls-box (atom [])) ;; collected [ "ns/name" [arg-types...] ] +(def ^:private escapes-box (atom #{})) ;; var-keys used as a VALUE (not a call head) + +(defn- var-key [fnode] (str (get fnode :ns) "/" (get fnode :name))) + (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)] + (let [op (get fnode :op)] (cond - (nil? nm) :any - (contains? truthy-ret-fns nm) :truthy - (contains? vector-ret-fns nm) :vector + ;; a user fn whose return type the fixpoint has estimated + (= op :var) (let [r (get @rtenv-box (var-key fnode))] + (if r r (let [nm (and (= "clojure.core" (get fnode :ns)) (get fnode :name))] + (cond (nil? nm) :any + (contains? truthy-ret-fns nm) :truthy + (contains? vector-ret-fns nm) :vector + :else :any)))) + (= op :host) (let [nm (get fnode :name)] + (cond (contains? truthy-ret-fns nm) :truthy + (contains? vector-ret-fns nm) :vector + :else :any)) :else :any))) (defn- infer @@ -781,10 +797,19 @@ [(nth r 0) (assoc node :statements stmts :ret (nth r 1))]) (= op :throw) [:any (assoc node :expr (nth (infer (get node :expr) tenv) 1))] + ;; a :var reached HERE is in value position (an arg, a let init, ...), not + ;; a call head — so the fn it names escapes and its params can't be inferred. + (= op :var) (do (swap! escapes-box conj (var-key node)) [:any node]) (= 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)]) + (let [fnode (get node :fn) + iscall-var (= :var (get fnode :op)) + ;; a :var in call-head position is a call, NOT an escape — so don't + ;; route it through infer (which would record it as escaped). + fnode' (if iscall-var fnode (nth (infer fnode tenv) 1)) + ares (mapv (fn [a] (infer a tenv)) (get node :args))] + (when iscall-var + (swap! calls-box conj [(var-key fnode) (mapv (fn [r] (nth r 0)) ares)])) + [(call-ret-type fnode) (assoc node :fn fnode' :args (mapv (fn [r] (nth r 1)) ares))]) (= op :let) (let [res (reduce (fn [acc b] (let [te (nth acc 0) binds (nth acc 1) @@ -803,8 +828,15 @@ (= 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)))] + ;; a closure inherits the enclosing tenv so CAPTURED locals keep their + ;; types (e.g. a reduce closure that calls (f captured-struct ...)); its own + ;; params/rest shadow to :any (unknown until Phase 1 types them via callers). + [:any (assoc node :arities + (mapv (fn [a] + (let [pe (reduce (fn [e p] (assoc e p :any)) tenv (get a :params)) + pe (if (get a :rest) (assoc pe (get a :rest) :any) pe)] + (assoc a :body (nth (infer (get a :body) pe) 1)))) + (get node :arities)))] (= op :def) [:any (assoc node :init (nth (infer (get node :init) tenv) 1))] (= op :try) @@ -816,6 +848,39 @@ (defn- infer-top [node] (nth (infer node {}) 1)) +;; --- Inter-procedural driver API (jolt-767) consumed by the back end -------- +(defn set-rtenv! + "Install the current return-type estimates (a map \"ns/name\" -> type) used to + type call results during the fixpoint." + [m] (reset! rtenv-box m)) + +(defn reset-escapes! [] (reset! escapes-box #{})) +(defn collected-escapes [] (vec @escapes-box)) + +(defn infer-body + "Type `body` under tenv (local-name -> type). Returns [ret-type node' calls], + where calls is the [[\"ns/name\" [arg-types...]] ...] this body invokes (for + propagating into callee param types). Also accumulates escapes (read with + collected-escapes after a full sweep)." + [body tenv] + (reset! calls-box []) + (let [r (infer body tenv)] + [(nth r 0) (nth r 1) @calls-box])) + +(defn reinfer-def + "Re-run inference on a stashed :def's fn arity bodies with param types seeded + (ptmap: param-name -> type), returning the def with annotated bodies. The back + end emits the result directly (no further passes), so the param-typed lookups + keep their specialization. Used by the inter-procedural recompile." + [def-node ptmap] + (let [fnode (get def-node :init)] + (if (= :fn (get fnode :op)) + (assoc def-node :init + (assoc fnode :arities + (mapv (fn [a] (assoc a :body (nth (infer (get a :body) ptmap) 1))) + (get fnode :arities)))) + def-node))) + (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), diff --git a/src/jolt/api.janet b/src/jolt/api.janet index cb84cb0..ed1d6b8 100644 --- a/src/jolt/api.janet +++ b/src/jolt/api.janet @@ -189,6 +189,10 @@ # — that would be circular — so it reads this hook). Without it, required # namespaces ran interpreted-only. (put (ctx :env) :toplevel-eval eval-toplevel) + # Inter-procedural type-inference hook (jolt-767): the evaluator calls this + # after a unit finishes loading (optimization mode only). Installed here to + # avoid an evaluator->backend circular import. + (put (ctx :env) :infer-unit! backend/infer-unit!) # Stateful primitives as ctx-capturing clojure.core fns (protocol-dispatch, # register-method, …) — so the protocol macros compile to plain invokes. Must # precede the overlay (its defprotocol/extend-type expansions call these). diff --git a/src/jolt/backend.janet b/src/jolt/backend.janet index 04c324f..96386a6 100644 --- a/src/jolt/backend.janet +++ b/src/jolt/backend.janet @@ -78,7 +78,10 @@ (when (= 1 (length arities)) (def ar (norm-node (in arities 0))) (unless (ar :rest) - (put cell :inline-ir {:params (ar :params) :body (ar :body)})))))) + (put cell :inline-ir {:params (ar :params) :body (ar :body)}) + # jolt-767: stash the whole (post-pass) :def IR so the inter-procedural + # pass can re-infer its body with discovered param types and re-emit it. + (put cell :infer-ir node)))))) # Var late-binding: reads go through `(var-get cell)` with the cell embedded as a # constant, so compiled code sees redefinition (Janet early-binds plain symbols) @@ -745,6 +748,110 @@ (++ n)))) n) +# Inter-procedural collection-type inference + recompile (jolt-767, Phase 1), +# closed-world / optimization mode. After a unit loads, every single-fixed-arity +# fn stashed a post-pass :def IR (:infer-ir). We: +# 1. run a whole-unit fixpoint: a fn's param types = lub of its in-unit +# call-site arg types (computed by jolt.passes/infer-body); a fn whose var +# escapes as a VALUE keeps :any params (its callers aren't all visible). +# 2. re-infer + re-emit each fn body with its param types seeded, so +# param-dependent lookups specialize (drop the :jolt/type guard). +# Recompiled bodies are semantically identical to the guarded ones, so this is +# correct regardless of recompile order; order only affects how far a direct- +# linked call propagates the faster callee. +(defn- itype-join [a b] (cond (nil? a) b (nil? b) a (= a b) a :any)) + +(defn infer-unit! + [ctx ns-name] + (def pns (ctx-find-ns ctx "jolt.passes")) + (def f-set-rtenv (and pns (ns-find pns "set-rtenv!"))) + (def f-infer-body (and pns (ns-find pns "infer-body"))) + (def f-reinfer (and pns (ns-find pns "reinfer-def"))) + (def f-reset-esc (and pns (ns-find pns "reset-escapes!"))) + (def f-get-esc (and pns (ns-find pns "collected-escapes"))) + (def ns (ctx-find-ns ctx ns-name)) + (def report @{}) + (when (and ns f-set-rtenv f-infer-body f-reinfer f-reset-esc f-get-esc) + # gather single-fixed-arity fns with a stashed :def + (def fns @[]) + (def by-key @{}) + (each nm (keys (ns :mappings)) + (def v (get (ns :mappings) nm)) + (when (and (table? v) (get v :infer-ir)) + (def d (norm-node (get v :infer-ir))) + (def init (norm-node (d :init))) + (when (= :fn (init :op)) + (def ars (vview (init :arities))) + (when (= 1 (length ars)) + (def ar (norm-node (in ars 0))) + (unless (ar :rest) + (def pv (vview (ar :params))) + (def rec @{:key (string ns-name "/" nm) :cell v :def d + :params (ar :params) :body (ar :body) + :np (length pv) :pt (array/new-filled (length pv)) :ret nil}) + (array/push fns rec) + (put by-key (rec :key) rec)))))) + (when (> (length fns) 0) + ((var-get f-reset-esc)) + # --- param/return-type fixpoint (chaotic iteration to the LEAST fixpoint) --- + # Param types are RECOMPUTED FRESH each iteration, not accumulated: :any is + # the lattice top, so a join with an early-iteration :any (a caller whose own + # params weren't typed yet) would poison the result permanently. Recomputing + # from the current state lets a param refine as its callers' types improve. + (var prev-rt @{}) + (var changed true) (var iter 0) + (while (and changed (< iter 16)) + ((var-get f-set-rtenv) prev-rt) + # type every body once under current param types; stash ret + calls + (each f fns + (def tenv @{}) + (def pv (vview (f :params))) + (for i 0 (f :np) (when (in (f :pt) i) (put tenv (in pv i) (in (f :pt) i)))) + (def res (vview ((var-get f-infer-body) (f :body) tenv))) + (put f :tret (in res 0)) + (put f :tcalls (in res 2))) + # recompute param types FRESH (start at bottom = nil) from this round's calls + (def newpt @{}) + (each f fns (put newpt (f :key) (array/new-filled (f :np)))) + (each f fns + (each c (vview (f :tcalls)) + (def cv (vview c)) + (def npa (get newpt (in cv 0))) + (when npa + (def callee (get by-key (in cv 0))) + (def ats (vview (in cv 1))) + (def lim (min (length ats) (callee :np))) + (for i 0 lim (put npa i (itype-join (in npa i) (in ats i))))))) + # commit + detect change + (set changed false) + (def nrt @{}) + (each f fns + (def np (get newpt (f :key))) + (for i 0 (f :np) (when (not= (in np i) (in (f :pt) i)) (set changed true))) + (when (not= (f :tret) (f :ret)) (set changed true)) + (put f :pt np) + (put f :ret (f :tret)) + (when (f :tret) (put nrt (f :key) (f :tret)))) + (set prev-rt nrt) + (++ iter)) + # --- escaped fns: var used as a value -> params untrustworthy -> skip --- + (def esc @{}) + (each k (vview ((var-get f-get-esc))) (put esc k true)) + # --- re-infer + re-emit each fn with concrete param types seeded --- + (each f fns + (put report (f :key) (f :pt)) + (unless (get esc (f :key)) + (def ptmap @{}) + (var concrete false) + (def pv (vview (f :params))) + (for i 0 (f :np) + (def t (in (f :pt) i)) + (when (and t (not= t :any)) (set concrete true) (put ptmap (in pv i) t))) + (when concrete + (def def2 ((var-get f-reinfer) (f :def) ptmap)) + (protect (eval (emit-ir ctx def2) (ctx-janet-env ctx)))))))) + report) + (defn ensure-macros-compiled! "Called once the overlay is fully loaded (api/load-core-overlay!): ensure the analyzer is built, then run the staged macro-recompile pass so the early diff --git a/src/jolt/evaluator.janet b/src/jolt/evaluator.janet index 096501e..694b783 100644 --- a/src/jolt/evaluator.janet +++ b/src/jolt/evaluator.janet @@ -421,6 +421,14 @@ (if path (load-ns-source ctx (slurp path) path) (load-ns-source ctx embedded (string ns-name " (stdlib)"))) + # Inter-procedural collection-type inference (jolt-767): once the whole + # unit is loaded, run the closed-world fixpoint + recompile so param- + # dependent lookups specialize. Only in optimization mode; best-effort + # (a failure here must not break loading). Hook installed by the api to + # avoid an evaluator->backend circular import. + (when (get (ctx :env) :inline?) + (when-let [iu (get (ctx :env) :infer-unit!)] + (protect (iu ctx ns-name)))) # Record load order for tooling (uberscript): a dependency finishes # loading before its requirer, so this is topological. Skip the # baked-in stdlib — it's part of the runtime, not something to bundle. diff --git a/test/integration/type-infer-phase1-test.janet b/test/integration/type-infer-phase1-test.janet new file mode 100644 index 0000000..31735f8 --- /dev/null +++ b/test/integration/type-infer-phase1-test.janet @@ -0,0 +1,54 @@ +# Inter-procedural collection-type inference, Phase 1 (jolt-767): closed-world. +# A whole-unit fixpoint propagates collection types through the call graph — a +# fn's param types become the lub of its in-unit call-site arg types — so a +# param that always receives a struct map gets typed and its lookups specialize, +# with no hint. Fns whose var escapes as a value keep :any params (their callers +# aren't all visible). Sound under source distribution + whole-program compile. +(import ../../src/jolt/api :as api) +(import ../../src/jolt/backend :as backend) +(import ../../src/jolt/types :as types) +(import ../../src/jolt/reader :as reader) + +(print "Type inference Phase 1 (jolt-767)...") + +(os/setenv "JOLT_DIRECT_LINK" "1") +(def ctx (api/init {:compile? true})) +(api/eval-string ctx "(ns p1)") +# closed-world unit. mk is small (inlined away). rd is RECURSIVE, so it survives +# inlining and is called via its var — exactly the shape (big/recursive fn with +# escaping-from-the-caller params) that inter-procedural inference targets. Its +# param v flows from mk's struct-map literal (after mk inlines into drv). +(each s ["(defn mk [a b] {:r a :g b})" + "(defn rd [v n] (if (< n 1) (:r v) (rd v (dec n))))" + "(defn drv [] (rd (mk 1 2) 3))" + # esc's var is used as a VALUE (passed to mapv) -> params must stay :any + "(defn esc [w] (:r w))" + "(defn use-esc [xs] (mapv esc xs))"] + (api/eval-string ctx s)) + +(def report (backend/infer-unit! ctx "p1")) + +# --- the fixpoint computed the right param types ----------------------------- +# rd's param v flows from mk's struct-map result (mk inlines to a struct literal +# in drv) and stays struct across the recursive self-call -> :struct-map +(assert (= :struct-map (in (get report "p1/rd") 0)) (string "rd param v: " (in (get report "p1/rd") 0))) +# esc escaped (passed to mapv) -> param stays unknown (:any / nil), NOT struct +(assert (not= :struct-map (in (get report "p1/esc") 0)) "escaping fn param not inferred struct") + +# --- the seeded re-inference drops the guard for a struct param -------------- +# (on a FRESH analysis, since infer-unit! re-stashes the already-specialized body) +(def pns (types/ctx-find-ns ctx "jolt.passes")) +(def reinfer (types/ns-find pns "reinfer-def")) +(def rd-def (backend/analyze-form ctx (reader/parse-string "(defn rdx [v n] (if (< n 1) (:r v) (rdx v (dec n))))"))) +(defn guards-seeded [ptmap] + (length (string/find-all ":jolt/type" (string/format "%p" (backend/emit-ir ctx ((types/var-get reinfer) rd-def ptmap)))))) +(assert (= 0 (guards-seeded @{"v" :struct-map})) "struct param -> bare lookup") +(assert (= 1 (guards-seeded @{})) "no param type -> guard kept") + +# --- correctness: recompiled unit still computes the same -------------------- +(assert (= 1 (api/eval-string ctx "(p1/drv)")) "drv correct after recompile") +(assert (= 7 (api/eval-string ctx "(p1/rd {:r 7 :g 8} 0)")) "rd correct on a struct") +(assert (= nil (api/eval-string ctx "(p1/rd (hash-map :r nil) 0)")) "rd correct on a phm (key present, nil)") +(assert (deep= [1 1] (api/normalize-pvecs (api/eval-string ctx "(p1/use-esc [{:r 1} {:r 1}])"))) "escaping fn still correct") + +(print "Type inference Phase 1 passed!") From 09e5af02c96ca9fa55aee8639e6ce62594f9886e Mon Sep 17 00:00:00 2001 From: Yogthos Date: Sat, 13 Jun 2026 06:53:21 -0400 Subject: [PATCH 06/20] feat: Phase 3 collection-element types + HOF awareness + ordered re-emit (jolt-d6u) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Extends the inference lattice with a parametric vector type {:vec ELEM} and threads element types through the program: - vector literals, conj/into, and range produce element-typed vectors; - reduce/map/mapv/filter/filterv seed their closure's element (and reduce's accumulator) param, so a lookup inside the closure over a vector-of-structs specializes (the HOF-element-awareness piece); - a var reference carries a VALUE type — a fn var is :truthy (non-nil, sealed root), a def var carries its inferred init type (e.g. a color table is {:vec :struct-map}); element-returning fns (rand-nth/first/nth/...) yield the collection's element type. These let the dynamically-built scene's sphere maps type as structs. The inter-procedural fixpoint now also infers non-fn def value types, and the recompile re-emits the WHOLE unit callee-first (reverse-topological) so a caller re-embeds its recompiled, now-specialized callees and a call site compiled after the pass links the whole chain. Result on the ray tracer (no hints): the chain closes — hittables infers to {:vec :struct-map}, hit-sphere's hittable param to :struct-map — and the render goes 13.1s -> 12.8s. That is only ~3%, far short of the explicit hint's 1.22x. The remaining gap is nested field access: a lookup RESULT like (:direction ray) is :any, so (:r (:direction ray)) stays guarded, and the vec3 fns (called with such values) can't be typed struct. The hint asserts the vec3 params directly and propagates through inlining; matching it needs field-shape types (ray.direction : vec3, vec3.r : number) — a structural extension (Phase 4). Sound: a seeded full render produces an identical checksum (1915337); conformance 335/335 x3 and the full jpm test pass; type-infer-phase3-test pins the element-typing + HOF mechanism. Phase 2 (vector nth/count specialization) was deprioritized — it is orthogonal to this benchmark. --- jolt-core/jolt/passes.clj | 139 ++++++++++++++++-- src/jolt/backend.janet | 119 ++++++++++----- test/integration/type-infer-phase3-test.janet | 41 ++++++ 3 files changed, 249 insertions(+), 50 deletions(-) create mode 100644 test/integration/type-infer-phase3-test.janet diff --git a/jolt-core/jolt/passes.clj b/jolt-core/jolt/passes.clj index eecba2d..037f3ab 100644 --- a/jolt-core/jolt/passes.clj +++ b/jolt-core/jolt/passes.clj @@ -716,15 +716,25 @@ ;; 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)) +;; Lattice values: :struct-map (raw-get-safe), :phm-map, :set, :truthy (a +;; provably non-nil/non-false scalar), :any (top), and a PARAMETRIC vector type +;; {:vec ELEM} (jolt-d6u, Phase 3) carrying its element type so a reduce/map +;; closure over it can type its element param. {:vec ELEM} is a small struct, so +;; it compares by value on both the Clojure and the Janet (orchestrator) side. +(defn- velem [t] (get t :vec)) +(defn- vec-type? [t] (some? (velem t))) +(defn- mk-vec [t] {:vec (if t t :any)}) +(defn- join [a b] + (cond + (= a b) a + (and (vec-type? a) (vec-type? b)) (mk-vec (join (velem a) (velem b))) + :else :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. +;; struct only when all its values have a truthy type. Collections are non-nil. (defn- truthy-type? [t] - (or (= t :truthy) (= t :struct-map) (= t :phm-map) (= t :vector) (= t :set))) + (or (= t :truthy) (= t :struct-map) (= t :phm-map) (= t :set) (vec-type? t))) (def ^:private truthy-ret-fns #{"+" "-" "*" "/" "inc" "dec" "mod" "rem" "quot" "min" "max" "abs" @@ -739,6 +749,14 @@ (def ^:private rtenv-box (atom {})) ;; "ns/name" -> inferred return type (def ^:private calls-box (atom [])) ;; collected [ "ns/name" [arg-types...] ] (def ^:private escapes-box (atom #{})) ;; var-keys used as a VALUE (not a call head) +;; jolt-d6u: a var reference's VALUE type — a fn var is :truthy (non-nil), a def +;; var carries its inferred init type (e.g. a color table -> {:vec :struct-map}). +;; The orchestrator populates this from sealed (opt-mode) cell roots + def inits. +(def ^:private vtype-box (atom {})) ;; "ns/name" -> value type + +;; fns that RETURN an element of their (first) collection arg, so a lookup on the +;; result of (rand-nth coll-of-structs) etc. types as the element. +(def ^:private elem-fns #{"rand-nth" "first" "peek" "last" "nth" "fnext" "second"}) (defn- var-key [fnode] (str (get fnode :ns) "/" (get fnode :name))) @@ -750,14 +768,44 @@ (if r r (let [nm (and (= "clojure.core" (get fnode :ns)) (get fnode :name))] (cond (nil? nm) :any (contains? truthy-ret-fns nm) :truthy - (contains? vector-ret-fns nm) :vector + (contains? vector-ret-fns nm) (mk-vec :any) :else :any)))) (= op :host) (let [nm (get fnode :name)] (cond (contains? truthy-ret-fns nm) :truthy - (contains? vector-ret-fns nm) :vector + (contains? vector-ret-fns nm) (mk-vec :any) :else :any)) :else :any))) +(declare infer) + +;; HOFs that apply their fn arg to the ELEMENTS of a collection (jolt-d6u, +;; Phase 3). :epos is which param of the fn receives an element. reduce is +;; handled separately (its arity changes the coll position, and its closure +;; also takes an accumulator). +(def ^:private hof-table + {"map" {:epos 0} "mapv" {:epos 0} "filter" {:epos 0} "filterv" {:epos 0} + "keep" {:epos 0} "remove" {:epos 0} "run!" {:epos 0} "mapcat" {:epos 0}}) + +(defn- infer-fn-seeded + "Infer a fn-literal passed to a HOF, seeding the given params to element/accum + types (seeds: param-index -> type), other params :any, captured locals from + tenv. Returns [ret-type node'] — ret is the lub of arity tail types, used to + type the HOF result (e.g. reduce's accumulator, mapv's element)." + [node seeds tenv] + (let [res (mapv (fn [a] + (let [params (get a :params) + pe (reduce (fn [e i] + (assoc e (nth params i) + (let [s (get seeds i)] (if s s :any)))) + tenv (range (count params))) + pe (if (get a :rest) (assoc pe (get a :rest) :any) pe) + br (infer (get a :body) pe)] + [(nth br 0) (assoc a :body (nth br 1))])) + (get node :arities)) + rets (mapv (fn [r] (nth r 0)) res) + ret (if (empty? rets) :any (reduce join (first rets) (rest rets)))] + [ret (assoc node :arities (mapv (fn [r] (nth r 1)) res))])) + (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 @@ -782,7 +830,10 @@ :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)))] + (let [irs (mapv (fn [x] (infer x tenv)) (get node :items)) + ets (mapv (fn [r] (nth r 0)) irs) + el (if (empty? ets) :any (reduce join (first ets) (rest ets)))] + [(mk-vec el) (assoc node :items (mapv (fn [r] (nth r 1)) irs))]) (= op :set) [:set (assoc node :items (mapv (fn [x] (nth (infer x tenv) 1)) (get node :items)))] (= op :if) @@ -799,17 +850,68 @@ [:any (assoc node :expr (nth (infer (get node :expr) tenv) 1))] ;; a :var reached HERE is in value position (an arg, a let init, ...), not ;; a call head — so the fn it names escapes and its params can't be inferred. - (= op :var) (do (swap! escapes-box conj (var-key node)) [:any node]) + ;; Its VALUE type comes from vtype-box (a fn is :truthy, a def carries its + ;; inferred type); unknown -> :any. + (= op :var) (do (swap! escapes-box conj (var-key node)) + [(let [vt (get @vtype-box (var-key node))] (if vt vt :any)) node]) (= op :invoke) (let [fnode (get node :fn) iscall-var (= :var (get fnode :op)) - ;; a :var in call-head position is a call, NOT an escape — so don't - ;; route it through infer (which would record it as escaped). - fnode' (if iscall-var fnode (nth (infer fnode tenv) 1)) - ares (mapv (fn [a] (infer a tenv)) (get node :args))] - (when iscall-var - (swap! calls-box conj [(var-key fnode) (mapv (fn [r] (nth r 0)) ares)])) - [(call-ret-type fnode) (assoc node :fn fnode' :args (mapv (fn [r] (nth r 1)) ares))]) + cn (when (and iscall-var (= "clojure.core" (get fnode :ns))) (get fnode :name)) + args (get node :args) + n (count args)] + (cond + ;; reduce over a typed vector with a fn-literal (jolt-d6u): seed the + ;; closure's accumulator (param 0) to the init type and its element + ;; (param 1) to the vector's element type, so its body — and any calls + ;; it makes — see those types. + (and (= cn "reduce") (>= n 2) (= :fn (get (nth args 0) :op))) + (let [three (>= n 3) + coll-r (infer (nth args (if three 2 1)) tenv) + init-r (when three (infer (nth args 1) tenv)) + et (let [ct (nth coll-r 0)] (if (vec-type? ct) (velem ct) :any)) + init-t (if init-r (nth init-r 0) :any) + fn-r (infer-fn-seeded (nth args 0) {0 init-t 1 et} tenv)] + [(join init-t (nth fn-r 0)) + (assoc node :args (if three + [(nth fn-r 1) (nth init-r 1) (nth coll-r 1)] + [(nth fn-r 1) (nth coll-r 1)]))]) + ;; map/mapv/filter/... over a typed vector with a fn-literal: seed the + ;; fn's element param; mapv/filterv produce a typed vector. + (and cn (get hof-table cn) (>= n 2) (= :fn (get (nth args 0) :op))) + (let [coll-r (infer (nth args 1) tenv) + et (let [ct (nth coll-r 0)] (if (vec-type? ct) (velem ct) :any)) + fn-r (infer-fn-seeded (nth args 0) {(get (get hof-table cn) :epos) et} tenv) + rt (cond (= cn "mapv") (mk-vec (nth fn-r 0)) + (= cn "filterv") (mk-vec et) + :else :any)] + [rt (assoc node :args [(nth fn-r 1) (nth coll-r 1)])]) + ;; conj/into: track the element type of a vector being grown. + (and (or (= cn "conj") (= cn "into")) (>= n 1)) + (let [ares (mapv (fn [a] (infer a tenv)) args) + base (nth (nth ares 0) 0) + rest-ts (mapv (fn [r] (nth r 0)) (rest ares)) + rt (cond + (and (= cn "conj") (vec-type? base)) + (mk-vec (reduce join (velem base) rest-ts)) + (and (= cn "into") (vec-type? base) (= 2 n) (vec-type? (nth rest-ts 0))) + (mk-vec (join (velem base) (velem (nth rest-ts 0)))) + :else (call-ret-type fnode))] + [rt (assoc node :args (mapv (fn [r] (nth r 1)) ares))]) + ;; everything else: type args, collect the call (var callee), use the + ;; declared/estimated return type. range produces a numeric vector. + :else + (let [fnode' (if iscall-var fnode (nth (infer fnode tenv) 1)) + ares (mapv (fn [a] (infer a tenv)) args)] + (when iscall-var + (swap! calls-box conj [(var-key fnode) (mapv (fn [r] (nth r 0)) ares)])) + [(cond + (= cn "range") (mk-vec :truthy) + ;; element-returning fn over a typed vector -> the element type + (and cn (contains? elem-fns cn) (> n 0)) + (let [a0 (nth (nth ares 0) 0)] (if (vec-type? a0) (velem a0) :any)) + :else (call-ret-type fnode)) + (assoc node :fn fnode' :args (mapv (fn [r] (nth r 1)) ares))]))) (= op :let) (let [res (reduce (fn [acc b] (let [te (nth acc 0) binds (nth acc 1) @@ -854,6 +956,11 @@ type call results during the fixpoint." [m] (reset! rtenv-box m)) +(defn set-vtypes! + "Install var VALUE types (a map \"ns/name\" -> type): fn vars are :truthy + (non-nil), def vars carry their inferred init type (jolt-d6u)." + [m] (reset! vtype-box m)) + (defn reset-escapes! [] (reset! escapes-box #{})) (defn collected-escapes [] (vec @escapes-box)) diff --git a/src/jolt/backend.janet b/src/jolt/backend.janet index 96386a6..13c33aa 100644 --- a/src/jolt/backend.janet +++ b/src/jolt/backend.janet @@ -72,16 +72,21 @@ (when (get (ctx :env) :inline?) (def init (norm-node (node :init))) (def meta (node :meta)) - (when (and (= :fn (init :op)) - (not (and meta (or (get meta :redef) (get meta :dynamic))))) - (def arities (vview (init :arities))) - (when (= 1 (length arities)) - (def ar (norm-node (in arities 0))) - (unless (ar :rest) - (put cell :inline-ir {:params (ar :params) :body (ar :body)}) - # jolt-767: stash the whole (post-pass) :def IR so the inter-procedural - # pass can re-infer its body with discovered param types and re-emit it. - (put cell :infer-ir node)))))) + (def redefable (and meta (or (get meta :redef) (get meta :dynamic)))) + (cond + redefable nil + (= :fn (init :op)) + (let [arities (vview (init :arities))] + (when (= 1 (length arities)) + (def ar (norm-node (in arities 0))) + (unless (ar :rest) + (put cell :inline-ir {:params (ar :params) :body (ar :body)}) + # jolt-767: stash the whole (post-pass) :def IR so the inter-procedural + # pass can re-infer its body with discovered param types and re-emit it. + (put cell :infer-ir node)))) + # a non-fn def: stash so the pass can infer its VALUE type (jolt-d6u), e.g. + # a color table used via rand-nth — its element type flows to lookups. + true (put cell :infer-ir node)))) # Var late-binding: reads go through `(var-get cell)` with the cell embedded as a # constant, so compiled code sees redefinition (Janet early-binds plain symbols) @@ -759,12 +764,21 @@ # Recompiled bodies are semantically identical to the guarded ones, so this is # correct regardless of recompile order; order only affects how far a direct- # linked call propagates the faster callee. -(defn- itype-join [a b] (cond (nil? a) b (nil? b) a (= a b) a :any)) +(defn- itype-join [a b] + (cond + (nil? a) b + (nil? b) a + (= a b) a + # compound vector types {:vec ELEM} join element-wise (jolt-d6u) + (and (struct? a) (struct? b) (in a :vec) (in b :vec)) + (struct :vec (itype-join (in a :vec) (in b :vec))) + :any)) (defn infer-unit! [ctx ns-name] (def pns (ctx-find-ns ctx "jolt.passes")) (def f-set-rtenv (and pns (ns-find pns "set-rtenv!"))) + (def f-set-vtypes (and pns (ns-find pns "set-vtypes!"))) (def f-infer-body (and pns (ns-find pns "infer-body"))) (def f-reinfer (and pns (ns-find pns "reinfer-def"))) (def f-reset-esc (and pns (ns-find pns "reset-escapes!"))) @@ -772,28 +786,34 @@ (def ns (ctx-find-ns ctx ns-name)) (def report @{}) (when (and ns f-set-rtenv f-infer-body f-reinfer f-reset-esc f-get-esc) - # gather single-fixed-arity fns with a stashed :def + # gather single-fixed-arity fns AND non-fn defs that stashed a :def IR (def fns @[]) + (def defs @[]) (def by-key @{}) + (def vtypes @{}) # var VALUE types: fns -> :truthy (non-nil), defs -> inferred (each nm (keys (ns :mappings)) (def v (get (ns :mappings) nm)) (when (and (table? v) (get v :infer-ir)) (def d (norm-node (get v :infer-ir))) (def init (norm-node (d :init))) - (when (= :fn (init :op)) - (def ars (vview (init :arities))) - (when (= 1 (length ars)) - (def ar (norm-node (in ars 0))) - (unless (ar :rest) - (def pv (vview (ar :params))) - (def rec @{:key (string ns-name "/" nm) :cell v :def d - :params (ar :params) :body (ar :body) - :np (length pv) :pt (array/new-filled (length pv)) :ret nil}) - (array/push fns rec) - (put by-key (rec :key) rec)))))) - (when (> (length fns) 0) + (def key (string ns-name "/" nm)) + (if (= :fn (init :op)) + (let [ars (vview (init :arities))] + (when (= 1 (length ars)) + (def ar (norm-node (in ars 0))) + (unless (ar :rest) + (def pv (vview (ar :params))) + (def rec @{:key key :cell v :def d :params (ar :params) :body (ar :body) + :np (length pv) :pt (array/new-filled (length pv)) :ret nil}) + (array/push fns rec) + (put by-key key rec) + # a fn value is non-nil -> :truthy (sealed root in opt mode) + (put vtypes key :truthy)))) + # non-fn def: its value type is inferred from its init (jolt-d6u) + (array/push defs @{:key key :init (d :init) :vt nil})))) + (when (or (> (length fns) 0) (> (length defs) 0)) ((var-get f-reset-esc)) - # --- param/return-type fixpoint (chaotic iteration to the LEAST fixpoint) --- + # --- param/return/value-type fixpoint (chaotic iteration to LEAST fixpoint) --- # Param types are RECOMPUTED FRESH each iteration, not accumulated: :any is # the lattice top, so a join with an early-iteration :any (a caller whose own # params weren't typed yet) would poison the result permanently. Recomputing @@ -802,7 +822,8 @@ (var changed true) (var iter 0) (while (and changed (< iter 16)) ((var-get f-set-rtenv) prev-rt) - # type every body once under current param types; stash ret + calls + ((var-get f-set-vtypes) vtypes) + # type every fn body once under current param types; stash ret + calls (each f fns (def tenv @{}) (def pv (vview (f :params))) @@ -810,6 +831,9 @@ (def res (vview ((var-get f-infer-body) (f :body) tenv))) (put f :tret (in res 0)) (put f :tcalls (in res 2))) + # infer each def's VALUE type from its init + (each dv defs + (put dv :tvt (in (vview ((var-get f-infer-body) (dv :init) @{})) 0))) # recompute param types FRESH (start at bottom = nil) from this round's calls (def newpt @{}) (each f fns (put newpt (f :key) (array/new-filled (f :np)))) @@ -832,24 +856,51 @@ (put f :pt np) (put f :ret (f :tret)) (when (f :tret) (put nrt (f :key) (f :tret)))) + (each dv defs + (when (not= (dv :tvt) (dv :vt)) (set changed true)) + (put dv :vt (dv :tvt)) + (when (dv :tvt) (put vtypes (dv :key) (dv :tvt)))) (set prev-rt nrt) (++ iter)) # --- escaped fns: var used as a value -> params untrustworthy -> skip --- (def esc @{}) (each k (vview ((var-get f-get-esc))) (put esc k true)) - # --- re-infer + re-emit each fn with concrete param types seeded --- - (each f fns + # install the FINAL return + value types so reinfer-def sees them + (def final-rt @{}) + (each f fns (when (f :ret) (put final-rt (f :key) (f :ret)))) + ((var-get f-set-rtenv) final-rt) + ((var-get f-set-vtypes) vtypes) + # --- re-emit the WHOLE unit, callees first (jolt-d6u) ------------------- + # Re-inference alone only rebinds a fn's own var, but the hot path runs + # through callee bodies INLINED / direct-linked into callers at first + # compile. Re-emitting in callee-first (reverse-topological) order makes + # each caller re-embed its now-recompiled callees, and re-infers its body + # (typing locals via return inference) — so the specialization propagates, + # and a call site compiled AFTER this pass (the -e entry) links the whole + # recompiled chain. Every fn is re-emitted, not just those with concrete + # params, so the embedding refreshes even where a fn gained no param type. + (def order @[]) + (def seen @{}) + (defn visit [k] + (unless (get seen k) + (put seen k true) + (def f (get by-key k)) + (when f + (each c (vview (f :tcalls)) (visit (in (vview c) 0))) + (array/push order f)))) + (each f fns (visit (f :key))) + (each f order (put report (f :key) (f :pt)) + (def ptmap @{}) + # escaped fn: its param types are untrustworthy (callers not all visible), + # so re-emit it WITHOUT seeding params (still re-embeds recompiled callees). (unless (get esc (f :key)) - (def ptmap @{}) - (var concrete false) (def pv (vview (f :params))) (for i 0 (f :np) (def t (in (f :pt) i)) - (when (and t (not= t :any)) (set concrete true) (put ptmap (in pv i) t))) - (when concrete - (def def2 ((var-get f-reinfer) (f :def) ptmap)) - (protect (eval (emit-ir ctx def2) (ctx-janet-env ctx)))))))) + (when (and t (not= t :any)) (put ptmap (in pv i) t)))) + (def def2 ((var-get f-reinfer) (f :def) ptmap)) + (protect (eval (emit-ir ctx def2) (ctx-janet-env ctx)))))) report) (defn ensure-macros-compiled! diff --git a/test/integration/type-infer-phase3-test.janet b/test/integration/type-infer-phase3-test.janet new file mode 100644 index 0000000..89ecfc8 --- /dev/null +++ b/test/integration/type-infer-phase3-test.janet @@ -0,0 +1,41 @@ +# Collection-element types + HOF awareness, Phase 3 (jolt-d6u). A vector carries +# its element type ({:vec ELEM}); a reduce/map/filter closure over it gets that +# element type on its element param. So a lookup inside a reduce closure over a +# vector-of-structs specializes — no hint — WHEN the element type is provable. +(import ../../src/jolt/api :as api) +(import ../../src/jolt/backend :as backend) +(import ../../src/jolt/types :as types) +(import ../../src/jolt/reader :as reader) + +(print "Type inference Phase 3 (jolt-d6u)...") + +(os/setenv "JOLT_DIRECT_LINK" "1") +(def ctx (api/init {:compile? true})) +(api/eval-string ctx "(ns p3)") +(def pns (types/ctx-find-ns ctx "jolt.passes")) +(def reinfer (types/var-get (types/ns-find pns "reinfer-def"))) +# helper: analyze a defn, reinfer with seeded param types, count guards +(defn guards [src ptmap] + (def d (backend/analyze-form ctx (reader/parse-string src))) + (length (string/find-all ":jolt/type" (string/format "%p" (backend/emit-ir ctx (reinfer d ptmap)))))) + +# a reduce closure's element param gets the vector's element type +(def red "(defn f [coll] (reduce (fn [acc h] (+ acc (:r h))) 0 coll))") +(assert (= 0 (guards red @{"coll" {:vec :struct-map}})) "reduce element typed -> bare lookup in closure") +(assert (= 1 (guards red @{"coll" {:vec :any}})) "reduce over vector of unknown -> guard kept") +(assert (= 1 (guards red @{})) "untyped coll -> guard kept") + +# mapv over a vector-of-structs types the closure element too +(def mp "(defn g [coll] (mapv (fn [h] (:r h)) coll))") +(assert (= 0 (guards mp @{"coll" {:vec :struct-map}})) "mapv element typed -> bare lookup") +(assert (= 1 (guards mp @{"coll" {:vec :any}})) "mapv over unknown element -> guard") + +# element type is DERIVED, not just seeded: a vector literal of structs, reduced +(def derived "(defn h2 [] (reduce (fn [acc x] (+ acc (:r x))) 0 [{:r 1 :g 2} {:r 3 :g 4}]))") +(assert (= 0 (guards derived @{})) "vector literal of structs -> element struct -> bare lookup") + +# correctness: the specialized closures compute the same +(assert (= 4 (api/eval-string ctx "((fn [coll] (reduce (fn [acc h] (+ acc (:r h))) 0 coll)) [{:r 1} {:r 3}])")) "reduce value") +(assert (= 4 (api/eval-string ctx "(reduce (fn [acc x] (+ acc (:r x))) 0 [{:r 1 :g 2} {:r 3 :g 4}])")) "derived value") + +(print "Type inference Phase 3 passed!") From 5f05a99010ab28046b5b4a4aeaa1cd050d2c7578 Mon Sep 17 00:00:00 2001 From: Yogthos Date: Sat, 13 Jun 2026 09:28:16 -0400 Subject: [PATCH 07/20] =?UTF-8?q?feat:=20Phase=202=20vector-op=20specializ?= =?UTF-8?q?ation=20=E2=80=94=20count/nth=20on=20inferred=20vectors=20(jolt?= =?UTF-8?q?-d6u)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The inference now tags a :local it proved to be a vector with :hint :vector, and the back end specializes (count v) -> pv-count (skipping core-count's dispatch chain) and the 3-arg (nth v i default) -> pv-nth. The 2-arg nth is deliberately NOT specialized: pv-nth returns nil out-of-bounds where Clojure nth throws. Sound, conformance 335/335 x3 and full jpm test pass; type-infer-phase2-test pins the specialization and the 2-arg exclusion. --- jolt-core/jolt/passes.clj | 6 ++++- src/jolt/backend.janet | 20 ++++++++++++++++ test/integration/type-infer-phase2-test.janet | 24 +++++++++++++++++++ 3 files changed, 49 insertions(+), 1 deletion(-) create mode 100644 test/integration/type-infer-phase2-test.janet diff --git a/jolt-core/jolt/passes.clj b/jolt-core/jolt/passes.clj index 037f3ab..54e8ab3 100644 --- a/jolt-core/jolt/passes.clj +++ b/jolt-core/jolt/passes.clj @@ -817,7 +817,11 @@ [(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)]) + [(if t t :any) + (cond + (struct-safe? t) (assoc node :hint :struct) + (vec-type? t) (assoc node :hint :vector) + :else node)]) (= op :map) (let [res (mapv (fn [pr] (let [kr (infer (nth pr 0) tenv) diff --git a/src/jolt/backend.janet b/src/jolt/backend.janet index 13c33aa..957c547 100644 --- a/src/jolt/backend.janet +++ b/src/jolt/backend.janet @@ -13,6 +13,7 @@ (use ./evaluator) (import ./reader :as r) (import ./phm :as phm) +(import ./pv :as pv) # The IR is portable data; reading its representation is a host-layer concern. # Most nodes are Janet structs (raw-readable), but a node carrying a nil-valued @@ -320,6 +321,16 @@ :host (= "get" (fnode :name)) false)) +# Is fnode a reference to clojure.core/ (or host )? +(defn- core-head? [fnode name] + (case (fnode :op) + :var (and (= "clojure.core" (fnode :ns)) (= name (fnode :name))) + :host (= name (fnode :name)) + false)) + +# Is this IR node a :local the inference proved to be a vector ({:vec ...})? +(defn- vec-hinted? [n] (and (= :local (n :op)) (= :vector (n :hint)))) + # Shared emit for a constant-keyword map lookup — both (:kw m [d]) and # (get m :kw [d]). subj-node is the subject's IR node (carries the type hint), # m-expr its emitted form, k the keyword, d-expr the emitted default or nil. @@ -394,6 +405,15 @@ (emit-kw-lookup (norm-node (in argnodes 0)) (in args 0) ((norm-node (in argnodes 1)) :val) (when (= 3 (length args)) (in args 2))) + # (count v) on an inferred vector -> pv-count, skipping core-count's dispatch + # chain (jolt-d6u, Phase 2). Sound: a {:vec ...}-typed value is a pvec. + (and (core-head? fnode "count") (= 1 (length args)) (vec-hinted? (norm-node (in argnodes 0)))) + (tuple pv/pv-count (in args 0)) + # (nth v i default) on an inferred vector -> pv-nth. Only the 3-ARG form: the + # 2-arg nth ERRORS on out-of-bounds where pv-nth returns nil, so specializing + # it would change semantics; the 3-arg default matches pv-nth exactly. + (and (core-head? fnode "nth") (= 3 (length args)) (vec-hinted? (norm-node (in argnodes 0)))) + (tuple pv/pv-nth (in args 0) (in args 1) (in args 2)) (direct-call? ctx fnode) (tuple (emit ctx fnode) ;args) # Local callee (closure param, let-bound fn, defn self-name): inline the # function check so the overwhelmingly-common function case is a direct diff --git a/test/integration/type-infer-phase2-test.janet b/test/integration/type-infer-phase2-test.janet new file mode 100644 index 0000000..94c8aeb --- /dev/null +++ b/test/integration/type-infer-phase2-test.janet @@ -0,0 +1,24 @@ +# Vector op specialization, Phase 2 (jolt-d6u): a value the inference proved to +# be a vector ({:vec ...}) gets count -> pv-count (skip core-count's dispatch) +# and 3-arg nth -> pv-nth. 2-arg nth is NOT specialized: it errors on +# out-of-bounds where pv-nth returns nil. +(import ../../src/jolt/api :as api) +(import ../../src/jolt/backend :as backend) +(import ../../src/jolt/types :as types) +(import ../../src/jolt/reader :as reader) +(print "Type inference Phase 2 (vector ops)...") +(os/setenv "JOLT_DIRECT_LINK" "1") +(def ctx (api/init {:compile? true})) +(api/eval-string ctx "(ns p2)") +(def reinfer (types/var-get (types/ns-find (types/ctx-find-ns ctx "jolt.passes") "reinfer-def"))) +(defn estr [src ptmap] + (string/format "%p" (backend/emit-ir ctx (reinfer (backend/analyze-form ctx (reader/parse-string src)) ptmap)))) +(assert (string/find "pv-count" (estr "(defn f [v] (count v))" @{"v" {:vec :any}})) "count on vector -> pv-count") +(assert (not (string/find "pv-count" (estr "(defn f [v] (count v))" @{}))) "count on unknown not specialized") +(assert (string/find "pv-nth" (estr "(defn f [v i] (nth v i 0))" @{"v" {:vec :any}})) "3-arg nth on vector -> pv-nth") +(assert (not (string/find "pv-nth" (estr "(defn f [v i] (nth v i))" @{"v" {:vec :any}}))) "2-arg nth NOT specialized") +# correctness +(assert (= 3 (api/eval-string ctx "(count [1 2 3])")) "count value") +(assert (= 2 (api/eval-string ctx "(nth [1 2 3] 1 9)")) "nth 3-arg in-bounds") +(assert (= 9 (api/eval-string ctx "(nth [1 2 3] 5 9)")) "nth 3-arg default") +(print "Type inference Phase 2 passed!") From e7473f38cf77458e155b06c9bdea73dc3b8a7c0b Mon Sep 17 00:00:00 2001 From: Yogthos Date: Sat, 13 Jun 2026 10:17:21 -0400 Subject: [PATCH 08/20] docs: RFC 0005 structural type inference + RFC 0006 success type checking 0005 proposes replacing the ad-hoc inference lattice with one recursive structural type (a struct carries its field types, a vector its element type, recursively), so a lookup returns its field's type and nested access is typed end to end. It unifies :struct tracking with field tracking, subsumes the current inference phases, and is the soft-typing (HM + a dynamic top) design: structural types + core-fn type schemes, solved by lattice join with :any as top instead of unify-or-fail. Includes the depth cap for termination and an explicit design-problems section. 0006 (follow-up, depends on 0005) reuses the inference as a loose type checker in the success-typing discipline (Dialyzer): report only PROVABLY-wrong code (a concrete type in an operation's throwing error-domain), accept everything ambiguous, never a false positive. Curated error-domain table, strictness levels (off/warn/error), clear located messages, and the soundness boundaries (closed-world, macros, unions). --- docs/rfc/0005-structural-type-inference.md | 244 +++++++++++++++++++++ docs/rfc/0006-success-type-checking.md | 215 ++++++++++++++++++ 2 files changed, 459 insertions(+) create mode 100644 docs/rfc/0005-structural-type-inference.md create mode 100644 docs/rfc/0006-success-type-checking.md diff --git a/docs/rfc/0005-structural-type-inference.md b/docs/rfc/0005-structural-type-inference.md new file mode 100644 index 0000000..872ae3a --- /dev/null +++ b/docs/rfc/0005-structural-type-inference.md @@ -0,0 +1,244 @@ +# RFC 0005 — Structural collection-type inference + +- **Status**: Draft +- **Champions**: jolt maintainers +- **Created**: 2026-06-13 + +## Summary + +Replace jolt's ad-hoc inference lattice with a single recursive **structural +type**, so that the type of a value mirrors the tree shape of the data it +describes. A struct-map carries its field types, a vector its element type, a +function its parameter and return types, recursively. A keyword lookup returns +the looked-up field's type, so nested access like `(:r (:direction ray))` is +typed end to end. This unifies the two facts the current inference tracks +inconsistently (a vector's element type, but not a map's field types), subsumes +the existing inference phases (jolt-99x Phases 0 to 3) as special cases, and +closes the remaining ray-tracer gap without a hint. The system is a +soft-typing-style inference: it never rejects a program, it assigns a concrete +type only when it can prove one, and it falls back to `:any` (and the existing +runtime guard) everywhere else. + +## Motivation + +The inference added in jolt-99x specializes a collection access (drops the +`:jolt/type` guard, emits `pv-count`, and so on) when it can prove the +collection's type. It works, it is sound, and it is fully dynamic-fallback +safe. But its type lattice grew ad hoc: + +- `:struct-map` means "a raw-get-safe map" but carries **no field types**. +- `{:vec ELEM}` carries its **element type**. + +These are the same idea applied to two kinds of child in the data tree, but +only one is tracked. The cost is concrete: in the ray tracer a lookup result +like `(:direction ray)` is typed `:any`, so `(:r (:direction ray))` keeps its +guard, and the `vec3` functions (called all day with such values) cannot be +typed, so the inference reaches only about 3% where the explicit `^:struct` +hint reaches 22%. The hint wins precisely because it asserts the field/param +shape the inference fails to derive. + +The fix is to make the type a structural tree, tagged as precisely as provable. +Then `:struct` tracking and field tracking are one mechanism, the special cases +collapse into one signature table, and nested access is typed by construction. + +## The type lattice + +A type `T` is one of: + +- A scalar tag: `:num`, `:str`, `:kw`, `:bool`, `:char`. (Optionally a coarser + `:nonnil` for "provably not nil and not false", which is what the struct-vs-phm + decision needs; see below.) +- `:nil`. +- `{:struct {field -> T}}` — a raw-get-safe map (Janet struct or record) whose + field `k` has type `(fields k)` or `:any` if absent. The degenerate + `{:struct {}}` is "a struct, fields unknown" and replaces today's + `:struct-map`. +- `{:vec T}` — a vector whose elements have type `T`. +- `{:set T}` — a set of `T`. +- `:phm` — a persistent hash map (NOT raw-get-safe; distinct from `:struct`). +- `{:fn {:params [T...] :ret T}}` — a function (optional precision; the current + flat param/return inference is the zero-arity-detail version of this). +- `:any` — the top. Anything not provably more specific. +- `:bottom` (represented as the absence of a type / `nil` internally) — the + identity for join, used to seed the fixpoint. + +Types are immutable values comparable by structural equality, exactly like the +current `{:vec ELEM}` representation, so they flow across the portable +inference and the Janet orchestrator unchanged. + +### Join (least upper bound) + +``` +join(T, T) = T +join(bottom, T) = T +join({:struct a}, {:struct b}) = {:struct {k -> join(a[k]?:any, b[k]?:any) for k in keys(a) ∪ keys(b)}} +join({:vec a}, {:vec b}) = {:vec join(a, b)} +join({:set a}, {:set b}) = {:set join(a, b)} +join(_, _) = :any ; different constructors +``` + +Two struct types join field-wise; a field present in only one side becomes +`:any` in the result (it might be absent, so a lookup of it is not provably +typed). This is the standard record lattice. + +### Termination: depth cap + +Structural types of recursive data (a tree node that contains a tree node, a +cons cell) would be infinite. To keep types finite and the inter-procedural +fixpoint terminating, structural types are **depth-capped**: beyond a small +depth `D` (proposed `D = 4`) a child type is `:any`. Construction and join both +truncate at `D`. With the cap the lattice has finite height, so the monotone +fixpoint converges. The ray tracer's shapes (vec3 inside ray inside hit-info) +are depth 2 to 3, well inside the cap. + +## Inference rules + +Inference is a forward pass producing `[type node']` for each IR node (the +existing shape), threaded with a local type environment and the +inter-procedural state from Phase 1. The rules are uniform over the structural +type: + +- **Literals.** `{:k v ...}` with constant scalar keys and struct-safe values + builds `{:struct {:k type(v) ...}}`; otherwise `:phm`. `[a b ...]` builds + `{:vec (join type(a) type(b) ...)}`. `#{...}` builds `{:set ...}`. Scalars + build their scalar tag. (The struct-vs-phm condition is the same as the back + end's: scalar keys, and every value provably non-nil and non-false.) +- **Lookup returns the field type.** `(:k m)` / `(get m :k)` where + `m : {:struct fs}` returns `(fs :k)` or `:any`. This is the single rule that + makes nesting work and that unifies field tracking with `:struct` tracking. +- **Indexing returns the element type.** `(nth v i)` / `(v i)` where + `v : {:vec T}` returns `T`. `(first v)` / `(peek v)` likewise. +- **Flow.** `let`/`loop` bind init types; `if` joins the branch types; `do` + takes the tail type. (As today.) +- **Calls use signatures.** Every call result type comes from the callee's + signature: core fns from a fixed signature table (below), user fns from the + inter-procedural fixpoint's inferred signature. + +The Phase 1 inter-procedural fixpoint, recompile, escape gate, and closed-world +assumption (RFC to follow / jolt-767) are unchanged. They now propagate +structural types instead of flat tags. + +## Core function signatures + +The current special cases (`truthy-ret-fns`, `vector-ret-fns`, `elem-fns`, +`hof-table`, and the `conj`/`range`/`reduce`/`mapv` branches) collapse into one +table of **type schemes**, possibly parametric: + +``` +inc, dec, +, -, *, /, mod, ... : (... :num) -> :num +count : (Coll) -> :num +nth : ∀T. ({:vec T}, :num) -> T (3-arg adds a default: -> join(T, default)) +get : ∀T. ({:struct fs}, :k) -> (fs :k) ; const key +first,peek : ∀T. ({:vec T}) -> T +conj : ∀T. ({:vec T}, x) -> {:vec join(T, type(x))} +assoc : ({:struct fs}, :k, v) -> {:struct (assoc fs :k type(v))} ; const key +vec, mapv : ... -> {:vec ...} +range : (...) -> {:vec :num} +rand-nth : ∀T. ({:vec T}) -> T +map, filter, mapv, filterv, reduce, ... ; see HOFs +``` + +Parametric schemes (the `∀T`) are where polymorphism actually matters, and they +give the element/field propagation for free. **Higher-order functions are just +schemes whose parameter is itself a function type**: `reduce`'s scheme says its +function argument is `(Acc, Elem) -> Acc` applied to the collection's element +type, so the closure's element parameter is typed by applying the scheme, +replacing the hand-written `hof-table`. + +## Hints as seeds + +`^:struct x` seeds `x : {:struct {}}` (a struct, fields unknown) at a unit +boundary the inference cannot see across. A future extension could allow a shape +hint `^{:r :num :g :num :b :num}` to seed field types, but once inference is +structural this is rarely needed; the hint stays the escape hatch for genuinely +dynamic boundaries, exactly as today. + +## Soundness + +Unchanged in spirit from the current system: a concrete type is assigned only +when proven (a literal genuinely has those fields; a fn provably returns that +shape), and everything unprovable is `:any`, which keeps the dynamic guard. A +wrong specialization is therefore impossible. The inter-procedural part keeps +the closed-world (optimization-mode) assumption already adopted, which is sound +under whole-program / source-distribution compilation. + +## Relationship to Hindley-Milner and soft typing + +This is HM-shaped with two deliberate departures, which is the textbook +definition of **soft typing** (Wright and Cartwright, "A Practical Soft Type +System for Scheme", 1997 — HM extended with union types and a dynamic type). + +Taken from HM: + +- The **structural type language** (records, vectors, functions as type + constructors). This is the "tree of types". +- **Constraint propagation** and **type schemes** for the core library (the + `∀T` signatures). That parametric polymorphism is exactly what HM provides, + and it is where it matters (generic collection functions like `nth`, + `reduce`, `map`). + +Changed, on purpose: + +- Replace "unify or **fail**" with "**join over a lattice whose top is `:any`**". + The inference never rejects a program; an unprovable spot becomes `:any` and + keeps the runtime guard. This is the "fall back to dynamic when in doubt" + policy made principled. +- **Monovariant** for user functions (the inter-procedural fixpoint plus + inlining cover the practical polymorphism); parametric schemes are kept only + for core functions. + +So: HM structural types and constraint propagation and core-fn schemes, solved +by lattice join with a dynamic top instead of unification-or-fail. Other AOT +inferencers for dynamic languages do the whole-program version of the same +thing (RPython's annotator, Crystal's global inference, Shed Skin), all with a +union/dynamic fallback. + +## Implementation and migration + +This is a refactor that **simplifies** the current code: it deletes the ad-hoc +tag soup and the per-op special cases and replaces them with one recursive type +plus a signature table. + +1. Define the structural type, `join`, the depth cap, and the predicates + (`struct-safe?`, `field-type`, `elem-type`) in `jolt.passes`. +2. Rewrite `infer` so each op produces/consumes structural types: literals + build shapes; `(:k m)` returns the field type; calls consult the signature + table. +3. Move the core-fn knowledge into a signature table (subsumes the existing + tables and HOF handling). +4. The back end keeps reading the use-site type to specialize (guard drop for + `{:struct}`, `pv-count`/`pv-nth` for `{:vec}`), now uniformly. +5. Keep the Phase 1 fixpoint, recompile, escape gate, and triggering as is; they + propagate structural types. + +The phases land incrementally behind the same optimization-mode gate, each +verified against conformance (three modes), the full test gate, and the +ray-tracer benchmark, exactly as the current phases were. + +## Design problems and open questions + +- **Recursion / termination.** Handled by the depth cap (`D = 4`). Open + question: is a fixed cap better than proper recursive (mu) types? A cap is + simpler and sound; mu-types are more precise but add complexity. Proposed: + start with the cap. +- **Compile-time cost.** Structural types are larger and the fixpoint does more + work. Mitigations: the depth cap bounds type size; inference runs only in + optimization mode; the fixpoint iteration count stays bounded. Needs + measurement on a large namespace (clojure.core itself) to confirm acceptable. +- **Heterogeneous data.** `[1 "a"]` joins to `{:vec :any}`; a map whose field + varies across branches joins that field to `:any`. Correct degradation, not a + problem, but worth stating. +- **Non-constant keys.** `(assoc m k v)` / `(:k m)` with a non-constant `k` + cannot track a specific field; the result degrades to `{:struct {}}` or + `:phm` as appropriate. Field tracking only applies to constant scalar keys. +- **`false`/`nil` field values.** A map literal is `{:struct ...}` only when + every value is provably non-nil and non-false (the back end stores such maps + as a phm). The `:nonnil` tag (or a per-type "provably truthy" predicate) is + what the literal rule needs; this must be carried correctly or struct + inference is unsound. +- **Function-type precision.** `{:fn ...}` is optional. The current flat + param/return inference is enough for the collection-specialization goal; + full function types matter more for the type-checker (RFC 0006) and could be + deferred. +- **Closed-world boundary.** Inherited from Phase 1: param/return inference + assumes the compiled unit is the whole program. Documented there; unchanged. diff --git a/docs/rfc/0006-success-type-checking.md b/docs/rfc/0006-success-type-checking.md new file mode 100644 index 0000000..e67da5e --- /dev/null +++ b/docs/rfc/0006-success-type-checking.md @@ -0,0 +1,215 @@ +# RFC 0006 — Compile-time detection of provably-wrong code (success typing) + +- **Status**: Draft +- **Champions**: jolt maintainers +- **Created**: 2026-06-13 +- **Depends on**: RFC 0005 (structural collection-type inference) + +## Summary + +Reuse the structural type inference of RFC 0005 as a **loose type checker**: at +compile time, flag code that is *provably* wrong, accept everything that is +merely ambiguous, and never produce a false positive. Concretely, when an +expression's inferred type is concrete and the operation applied to it would +throw at runtime for that type (for example passing a string where a function +only ever operates on numbers), report a clear compile-time error pointing at +the offending form, with the inferred type and what was expected. When the type +is `:any`, a union that includes a valid case, or beyond the inference's depth +cap, accept it silently. This is **success typing** (the discipline behind +Erlang's Dialyzer), applied to jolt for free on top of the inference we already +need for optimization. + +## Motivation + +Once the compiler tracks concrete types for many values (RFC 0005), it can see +some programs that cannot possibly be correct: `(inc "x")`, `(first 5)`, +`(count :k)`, `(/ 1 "two")`. Today these compile and fail at runtime, often far +from the cause. Reporting them at compile time, with a precise location and +message, turns a class of runtime crashes into immediate, actionable feedback, +at no extra inference cost. + +The design constraint the user set is the right one and is exactly success +typing's contract: **accept ambiguous cases, reject only provably-wrong ones.** +A checker that never lies about errors is one developers trust and that does not +get in the way of correct-but-untypeable dynamic code. + +## Principle: success typing, never a false positive + +Success typing (Lindahl and Sagonas, "Practical Type Inference Based on Success +Typings", 2006; the basis of Dialyzer) inverts the usual type-checker stance. +A normal checker accepts only what it can prove correct and rejects the rest +(false positives on dynamic code). A success typer accepts everything that +*could* be correct and rejects only what *cannot* be correct under any +execution. It is sound for **rejection**: if it reports an error, the code is +genuinely wrong. It is intentionally incomplete: it misses errors it cannot +prove. That is the correct trade for a dynamic language, and it matches the +user's "accept ambiguous, reject provably wrong". + +Mapped onto jolt: + +- The inference assigns a value a concrete type only when it can prove it + (RFC 0005). Unprovable is `:any`. +- A use site is reported **iff** the argument's inferred type is concrete and + lies entirely outside the operation's accepted domain, where the operation + *throws* on that domain (not merely returns a benign default). +- `:any`, a depth-capped child, or a union that includes an accepted type is + **never** reported. + +## What "provably wrong" means + +The checker needs, per operation it understands, an **error domain**: the set +of argument types for which the operation throws at runtime. This is narrower +than "the types it is documented to accept", because Clojure is lenient in many +places and flagging a benign case would be a false positive: + +- `(get 5 :k)` returns `nil`, it does not throw. NOT reported. +- `(:k 5)` returns `nil`. NOT reported. +- `(count 5)` throws ("count not supported on number"). Reported when the + argument is provably a non-countable scalar. +- `(first 5)` throws (not seqable). Reported for a provably non-seqable scalar. +- `(inc "x")`, `(+ 1 "x")` throw. Reported when an argument is provably a + non-number (`:str`, `:kw`, `:struct`, `:vec`, ...). +- `(nth 5 0)` throws. Reported for a provably non-indexable scalar. + +So the checker ships a curated table of the clearest throwing operations with +their error domains. It starts small (arithmetic on non-numbers, seq/`count`/ +`nth`/`first` on non-seqables) and grows conservatively. Anything not in the +table is not checked, which is safe (no false positive). + +A use site is reported only when: + +1. the argument's inferred type `T` is concrete (not `:any`, not a union that + includes an accepted type, not truncated by the depth cap), and +2. `T` is in the operation's error domain (the operation provably throws on `T`). + +## Examples + +```clojure +(inc "x") ; ERROR: inc expects a number, got a string +(let [n "x"] (inc n)) ; ERROR: same, n inferred :str +(count :foo) ; ERROR: count not supported on :kw +(first 42) ; ERROR: 42 is not seqable +(:k 5) ; accepted (returns nil, not an error) +(inc (rand-nth coll)) ; accepted if the element type is :any/unknown +(inc (if c 1 "x")) ; accepted: union {:num, :str} includes :num (ambiguous) +(defn f [n] (inc n)) ... ; if f is ALWAYS called with strings in-unit, ERROR at the call; + ; if its callers are unknown/varied, accepted +``` + +## Error reporting + +A reported error includes: + +- the source location (`file:line:col`) of the offending form; +- the operation and the parameter position; +- the inferred type of the argument, rendered readably (`:str`, + `{:struct {:r :num}}`, `{:vec :any}`); +- what the operation requires (`a number`, `a seqable`). + +Example: + +``` +type error at scene.clj:42:18 + (inc total) — `inc` requires a number, but `total` is a string +``` + +Errors are attributed to the form the user wrote. For macro-expanded code, the +checker reports at the original form's recorded position (the loader already +tracks `:error-pos`), never at synthesized internals. + +## Strictness levels + +A single env/compile flag controls behavior, defaulting to non-breaking: + +- **off** — no checking (default for now). +- **warn** — report to stderr, do not fail compilation. The recommended rollout + default once the table is trusted. +- **error** — fail compilation on a provable type error. Opt-in for CI / strict + builds. + +Because the checker only fires on provable errors, even `error` mode cannot +break a correct program: a correct program has no provable type errors to +report. (A correct-but-untypeable program is simply not reported, since its +types degrade to `:any`.) + +## Soundness of rejection (no false positives) + +The whole value of this feature is that a reported error is real. The +guarantees: + +- The inference assigns concrete types only when provable (RFC 0005). So a + concrete `T` at a use site is a genuine lower bound on what flows there in the + analyzed world. +- The error-domain table lists only operations that genuinely throw on the + listed types, verified against the runtime. +- Ambiguity is always accepted: `:any`, unions containing an accepted type, and + depth-capped children are never reported. + +Two boundaries need care and bound where the checker is allowed to fire: + +- **Closed-world / redefinition.** Inter-procedural argument types assume the + compiled unit is the whole program (inherited from RFC 0005). For the checker, + this means a reported error on a *user* function's parameter is only as sound + as that assumption. The conservative initial policy: only report against + **core-function** error domains (stable, not redefinable) and against types + derived without crossing an open boundary. Reporting against inferred user-fn + signatures is a later, opt-in escalation. +- **Macros / generated code.** Check post-expansion IR but report at the user's + source location, and suppress reports inside expansions the user did not + write (or attribute them to the macro call site). + +## Relationship to other systems + +- **Dialyzer / success typing** (Erlang): the direct model — sound for + rejection, no false positives, accepts the ambiguous. +- **Typed Clojure / core.typed**: opt-in *sound* gradual typing that rejects + what it cannot prove correct; the opposite trade (false positives on dynamic + code), which is why we do not follow it. +- **clj-kondo**: a popular Clojure linter that flags some obvious type misuses + syntactically; this RFC subsumes the type-driven subset with inference-backed + precision and no false positives. + +## Implementation + +The checker is a thin pass over the same inference results: + +1. After (or during) inference, walk the IR. At each call to an operation in + the error-domain table, look at the inferred type of each checked argument. +2. If concrete and in the error domain, record a diagnostic with location, the + inferred type, and the expected domain. +3. Emit diagnostics per the strictness level. + +It adds no new inference; it consumes RFC 0005's types and a small curated +table. It can ship after RFC 0005 lands, starting in `warn` mode with the +smallest high-confidence table (arithmetic and seq/count/nth/first), and grow. + +## Design problems and open questions + +- **Curating the error domain.** The table must list only genuinely-throwing + cases. Getting it wrong (listing a lenient op) yields false positives, which + destroys trust. Mitigation: start tiny, test each entry against the runtime, + grow slowly. Open question: derive the table from the same machinery the + runtime uses, to avoid drift? +- **Unions.** Today the inference joins to `:any` rather than forming unions + (`{:num | :str}`). Precise success typing wants unions (report only when + *every* member is in the error domain). Open question: add a small bounded + union type to RFC 0005's lattice, or keep `:any` and lose some precision (more + conservative, fewer reports, still no false positives)? Proposed: start with + `:any` (conservative), add unions if too many real errors are missed. +- **User-function signatures.** Reporting against inferred user-fn domains is + more powerful but rests on the closed-world assumption and on the inferred + signature being a true requirement. Proposed: core fns first; user fns behind + an explicit opt-in. +- **Negative/never types.** Some "provably wrong" cases are about a value being + the wrong arity or a fn vs a non-fn (calling a non-function). Worth including + the clear ones (calling a `:num` as a function) since the inference already + knows function-ness. +- **Position vs intent.** Reporting at the right source location through + inlining and macro expansion needs the position metadata to survive the + passes. The loader tracks `:error-pos`; the IR may need to carry form + positions for precise column reporting. +- **Interaction with the optimization gate.** The inference currently runs only + in optimization mode. The checker is valuable in normal builds too, so the + inference (at least its intra-procedural, sound-without-closed-world part) + may need to run for checking even when specialization is off. Open question: + decouple "run inference for checking" from "specialize from inference". From 9bc7b272451c3f237dbf216c8a85036ab6eb6c85 Mon Sep 17 00:00:00 2001 From: Yogthos Date: Sat, 13 Jun 2026 10:44:40 -0400 Subject: [PATCH 09/20] =?UTF-8?q?perf:=20structural=20type=20inference=20(?= =?UTF-8?q?RFC=200005)=20=E2=80=94=20nested=20access=20typed,=20hint-free?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Replace the ad-hoc inference lattice (a flat :struct-map tag plus {:vec ELEM}) with one recursive structural type: {:struct {field -> T}}, {:vec T}, {:set T}, scalar tags, and :any. A keyword lookup now returns its field's type, so nested access like (:r (:direction ray)) is typed end to end and drops its guard. join is field-wise and element-wise with a depth cap of 4 so the inter-procedural fixpoint still terminates. The back end honors a struct hint on any subject node, not just locals, so an inferred field type on a nested lookup specializes. The orchestrator's fixpoint joins through the portable join-types so compound types no longer collapse to :any. Ray tracer goes 12.8s to 11.0s with no hints, matching the explicit ^:struct version (10.9s). Render checksum unchanged (1915337), full gate green, conformance x3 modes pass. jolt-5uj --- jolt-core/jolt/passes.clj | 137 ++++++++++++++---- src/jolt/backend.janet | 11 +- test/integration/type-infer-phase1-test.janet | 11 +- test/integration/type-infer-phase3-test.janet | 4 +- 4 files changed, 127 insertions(+), 36 deletions(-) diff --git a/jolt-core/jolt/passes.clj b/jolt-core/jolt/passes.clj index 54e8ab3..f035353 100644 --- a/jolt-core/jolt/passes.clj +++ b/jolt-core/jolt/passes.clj @@ -716,27 +716,72 @@ ;; 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, :set, :truthy (a -;; provably non-nil/non-false scalar), :any (top), and a PARAMETRIC vector type -;; {:vec ELEM} (jolt-d6u, Phase 3) carrying its element type so a reduce/map -;; closure over it can type its element param. {:vec ELEM} is a small struct, so -;; it compares by value on both the Clojure and the Janet (orchestrator) side. +;; Recursive STRUCTURAL types (RFC 0005). A type mirrors the data tree: +;; compound: {:struct {field -> T}} (raw-get-safe map, field types) +;; {:vec T} (vector of T) +;; {:set T} (set of T) +;; scalar: :num :str :kw :truthy (all provably non-nil/non-false) +;; :phm (persistent hash map; NOT raw-get-safe) +;; :any (top), nil (bottom, identity for join). +;; Compound types are small jolt maps, so they compare by value on both the +;; Clojure and the Janet (orchestrator) side. struct/vec/set use distinct keys so +;; a type is recognised by which key it carries. +;; (get t :KEY) is nil for a keyword type and the child for a compound, so a +;; compound is detected by some? — no map?/contains? needed. (defn- velem [t] (get t :vec)) +(defn- selem [t] (get t :set)) +(defn- sfields [t] (get t :struct)) (defn- vec-type? [t] (some? (velem t))) +(defn- set-type? [t] (some? (selem t))) +(defn- struct-type? [t] (some? (sfields t))) (defn- mk-vec [t] {:vec (if t t :any)}) -(defn- join [a b] +(defn- mk-set [t] {:set (if t t :any)}) +(defn- mk-struct [fs] {:struct fs}) +(declare join-t) +(defn- merge-fields + "Per-field join of two field maps (a key in only one side joins with :any)." + [fa fb] + (let [m1 (reduce (fn [m k] (assoc m k (join-t (get fa k :any) (get fb k :any)))) {} (keys fa))] + (reduce (fn [m k] (if (get m k) m (assoc m k (join-t (get fa k :any) (get fb k :any))))) m1 (keys fb)))) +(defn- join-t [a b] (cond (= a b) a - (and (vec-type? a) (vec-type? b)) (mk-vec (join (velem a) (velem b))) + (nil? a) b + (nil? b) a + (and (struct-type? a) (struct-type? b)) (mk-struct (merge-fields (sfields a) (sfields b))) + (and (vec-type? a) (vec-type? b)) (mk-vec (join-t (velem a) (velem b))) + (and (set-type? a) (set-type? b)) (mk-set (join-t (selem a) (selem b))) :else :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. Collections are non-nil. +(defn- join [a b] (join-t a b)) +;; depth cap (RFC 0005): truncate a type below depth d to :any, so recursive data +;; can't make an infinite type and the inter-procedural fixpoint stays finite. +(def ^:private type-depth 4) +(defn- cap [t d] + (cond + (<= d 0) (if (or (struct-type? t) (vec-type? t) (set-type? t)) :any t) + (struct-type? t) (mk-struct (reduce (fn [m k] (assoc m k (cap (get (sfields t) k) (dec d)))) + {} (keys (sfields t)))) + (vec-type? t) (mk-vec (cap (velem t) (dec d))) + (set-type? t) (mk-set (cap (selem t) (dec d))) + :else t)) +;; raw-get-safe (a Janet struct / record): a struct type. The field type of key +;; k, if known, else :any. +(defn- struct-safe? [t] (struct-type? t)) +(defn- field-type [t k] (if (struct-type? t) (get (sfields t) k :any) :any)) +;; tag a node (any expression, not just a :local) so the back end can specialize +;; a lookup whose SUBJECT is that node — this is what makes nested access work: +;; (:direction ray) is tagged struct, so (:r (:direction ray)) drops its guard. +(defn- mark-hint [node h] (assoc node :hint h)) +;; a value provably neither nil nor false — the back end only builds a struct +;; (vs a phm) when every value is non-nil/non-false, so a map literal is a struct +;; only when all its values have such a type. Collections are non-nil. (defn- truthy-type? [t] - (or (= t :truthy) (= t :struct-map) (= t :phm-map) (= t :set) (vec-type? t))) + (or (= t :num) (= t :str) (= t :kw) (= t :truthy) (= t :phm) + (struct-type? t) (vec-type? t) (set-type? t))) -(def ^:private truthy-ret-fns +;; core fns whose result is a number (so it is non-nil/non-false and, for the +;; success-type checker, provably numeric). +(def ^:private num-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"}) @@ -767,11 +812,11 @@ (= op :var) (let [r (get @rtenv-box (var-key fnode))] (if r r (let [nm (and (= "clojure.core" (get fnode :ns)) (get fnode :name))] (cond (nil? nm) :any - (contains? truthy-ret-fns nm) :truthy + (contains? num-ret-fns nm) :num (contains? vector-ret-fns nm) (mk-vec :any) :else :any)))) (= op :host) (let [nm (get fnode :name)] - (cond (contains? truthy-ret-fns nm) :truthy + (cond (contains? num-ret-fns nm) :num (contains? vector-ret-fns nm) (mk-vec :any) :else :any)) :else :any))) @@ -814,7 +859,13 @@ (let [op (get node :op)] (cond (= op :const) - [(let [v (get node :val)] (if (or (nil? v) (= false v)) :any :truthy)) node] + [(let [v (get node :val)] + (cond (number? v) :num + (string? v) :str + (keyword? v) :kw + (or (nil? v) (= false v)) :any ; nil/false are not struct-eligible + :else :truthy)) ; true, char, ... -> non-nil + node] (= op :local) (let [t (get tenv (get node :name))] [(if t t :any) @@ -823,23 +874,29 @@ (vec-type? t) (assoc node :hint :vector) :else node)]) (= op :map) - (let [res (mapv (fn [pr] + (let [pairs (get node :pairs) + 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)] + [(nth kr 1) (nth vr 1) (nth vr 0) (get (nth pr 0) :val)])) + pairs) + struct? (and (> (count res) 0) + (every? (fn [pr] (scalar-const? (nth pr 0))) pairs) + (every? (fn [r] (truthy-type? (nth r 2))) res)) + t (if struct? + (cap (mk-struct (reduce (fn [m r] (assoc m (nth r 3) (nth r 2))) {} res)) type-depth) + :any)] [t (assoc node :pairs (mapv (fn [r] [(nth r 0) (nth r 1)]) res))]) (= op :vector) (let [irs (mapv (fn [x] (infer x tenv)) (get node :items)) ets (mapv (fn [r] (nth r 0)) irs) el (if (empty? ets) :any (reduce join (first ets) (rest ets)))] - [(mk-vec el) (assoc node :items (mapv (fn [r] (nth r 1)) irs))]) + [(cap (mk-vec el) type-depth) (assoc node :items (mapv (fn [r] (nth r 1)) irs))]) (= op :set) - [:set (assoc node :items (mapv (fn [x] (nth (infer x tenv) 1)) (get node :items)))] + (let [irs (mapv (fn [x] (infer x tenv)) (get node :items)) + ets (mapv (fn [r] (nth r 0)) irs) + el (if (empty? ets) :any (reduce join (first ets) (rest ets)))] + [(cap (mk-set el) type-depth) (assoc node :items (mapv (fn [r] (nth r 1)) irs))]) (= op :if) (let [tr (infer (get node :test) tenv) thn (infer (get node :then) tenv) @@ -865,6 +922,29 @@ args (get node :args) n (count args)] (cond + ;; (:k m) / (:k m default): the result is m's field type, and if m is a + ;; struct the subject is tagged so the back end drops the guard — this + ;; types nested access end to end (RFC 0005). + (and (= :const (get fnode :op)) (keyword? (get fnode :val)) (>= n 1) (<= n 2)) + (let [mr (infer (nth args 0) tenv) + mt (nth mr 0) + msub (if (struct-safe? mt) (mark-hint (nth mr 1) :struct) (nth mr 1)) + ft (field-type mt (get fnode :val)) + dr (when (= n 2) (infer (nth args 1) tenv))] + [(if dr (join ft (nth dr 0)) ft) + (assoc node :args (if dr [msub (nth dr 1)] [msub]))]) + ;; (get m :k [default]): same, when the key is a constant keyword. + (and (or (and (= :var (get fnode :op)) (= "clojure.core" (get fnode :ns)) (= "get" (get fnode :name))) + (and (= :host (get fnode :op)) (= "get" (get fnode :name)))) + (>= n 2) (= :const (get (nth args 1) :op)) (keyword? (get (nth args 1) :val))) + (let [mr (infer (nth args 0) tenv) + mt (nth mr 0) + msub (if (struct-safe? mt) (mark-hint (nth mr 1) :struct) (nth mr 1)) + kr (infer (nth args 1) tenv) + ft (field-type mt (get (nth args 1) :val)) + dr (when (= n 3) (infer (nth args 2) tenv))] + [(if dr (join ft (nth dr 0)) ft) + (assoc node :args (if dr [msub (nth kr 1) (nth dr 1)] [msub (nth kr 1)]))]) ;; reduce over a typed vector with a fn-literal (jolt-d6u): seed the ;; closure's accumulator (param 0) to the init type and its element ;; (param 1) to the vector's element type, so its body — and any calls @@ -910,7 +990,7 @@ (when iscall-var (swap! calls-box conj [(var-key fnode) (mapv (fn [r] (nth r 0)) ares)])) [(cond - (= cn "range") (mk-vec :truthy) + (= cn "range") (mk-vec :num) ;; element-returning fn over a typed vector -> the element type (and cn (contains? elem-fns cn) (> n 0)) (let [a0 (nth (nth ares 0) 0)] (if (vec-type? a0) (velem a0) :any)) @@ -965,6 +1045,11 @@ (non-nil), def vars carry their inferred init type (jolt-d6u)." [m] (reset! vtype-box m)) +(defn join-types + "Public structural join (lub), used by the orchestrator's fixpoint so param/ + return types join field-wise/element-wise instead of collapsing to :any." + [a b] (join-t a b)) + (defn reset-escapes! [] (reset! escapes-box #{})) (defn collected-escapes [] (vec @escapes-box)) diff --git a/src/jolt/backend.janet b/src/jolt/backend.janet index 957c547..f9247e7 100644 --- a/src/jolt/backend.janet +++ b/src/jolt/backend.janet @@ -342,7 +342,11 @@ # - hinted + JOLT_CHECK_HINTS: keep the guard but THROW on the tagged arm, so a # lying hint surfaces a clear error (dev aid; off by default, no perf cost). (defn- emit-kw-lookup [subj-node m-expr k d-expr] - (def hinted (and subj-node (= :local (subj-node :op)) (= :struct (subj-node :hint)))) + # the subject is a struct (raw-get-safe) when hinted so — by an explicit + # ^:struct/^Record hint on a local, OR by inference tagging ANY subject + # expression it proved to be a struct (jolt-d6u/RFC 0005), which is what lets + # nested access like (:r (:direction ray)) drop its guard. + (def hinted (and subj-node (= :struct (subj-node :hint)))) (def checked (and hinted (os/getenv "JOLT_CHECK_HINTS"))) (def m (if (symbol? m-expr) m-expr (jsym))) (def wrap (fn [body] (if (symbol? m-expr) body ['let [m m-expr] body]))) @@ -799,13 +803,14 @@ (def pns (ctx-find-ns ctx "jolt.passes")) (def f-set-rtenv (and pns (ns-find pns "set-rtenv!"))) (def f-set-vtypes (and pns (ns-find pns "set-vtypes!"))) + (def f-join (and pns (ns-find pns "join-types"))) (def f-infer-body (and pns (ns-find pns "infer-body"))) (def f-reinfer (and pns (ns-find pns "reinfer-def"))) (def f-reset-esc (and pns (ns-find pns "reset-escapes!"))) (def f-get-esc (and pns (ns-find pns "collected-escapes"))) (def ns (ctx-find-ns ctx ns-name)) (def report @{}) - (when (and ns f-set-rtenv f-infer-body f-reinfer f-reset-esc f-get-esc) + (when (and ns f-set-rtenv f-set-vtypes f-join f-infer-body f-reinfer f-reset-esc f-get-esc) # gather single-fixed-arity fns AND non-fn defs that stashed a :def IR (def fns @[]) (def defs @[]) @@ -865,7 +870,7 @@ (def callee (get by-key (in cv 0))) (def ats (vview (in cv 1))) (def lim (min (length ats) (callee :np))) - (for i 0 lim (put npa i (itype-join (in npa i) (in ats i))))))) + (for i 0 lim (put npa i ((var-get f-join) (in npa i) (in ats i))))))) # commit + detect change (set changed false) (def nrt @{}) diff --git a/test/integration/type-infer-phase1-test.janet b/test/integration/type-infer-phase1-test.janet index 31735f8..e60fbc1 100644 --- a/test/integration/type-infer-phase1-test.janet +++ b/test/integration/type-infer-phase1-test.janet @@ -29,11 +29,12 @@ (def report (backend/infer-unit! ctx "p1")) # --- the fixpoint computed the right param types ----------------------------- -# rd's param v flows from mk's struct-map result (mk inlines to a struct literal -# in drv) and stays struct across the recursive self-call -> :struct-map -(assert (= :struct-map (in (get report "p1/rd") 0)) (string "rd param v: " (in (get report "p1/rd") 0))) +# rd's param v flows from mk's struct result (mk inlines to a struct literal in +# drv) and stays struct across the recursive self-call -> a {:struct ...} type +(defn struct-type? [t] (truthy? (get t :struct))) +(assert (struct-type? (in (get report "p1/rd") 0)) (string "rd param v: " (in (get report "p1/rd") 0))) # esc escaped (passed to mapv) -> param stays unknown (:any / nil), NOT struct -(assert (not= :struct-map (in (get report "p1/esc") 0)) "escaping fn param not inferred struct") +(assert (not (struct-type? (in (get report "p1/esc") 0))) "escaping fn param not inferred struct") # --- the seeded re-inference drops the guard for a struct param -------------- # (on a FRESH analysis, since infer-unit! re-stashes the already-specialized body) @@ -42,7 +43,7 @@ (def rd-def (backend/analyze-form ctx (reader/parse-string "(defn rdx [v n] (if (< n 1) (:r v) (rdx v (dec n))))"))) (defn guards-seeded [ptmap] (length (string/find-all ":jolt/type" (string/format "%p" (backend/emit-ir ctx ((types/var-get reinfer) rd-def ptmap)))))) -(assert (= 0 (guards-seeded @{"v" :struct-map})) "struct param -> bare lookup") +(assert (= 0 (guards-seeded @{"v" {:struct {}}})) "struct param -> bare lookup") (assert (= 1 (guards-seeded @{})) "no param type -> guard kept") # --- correctness: recompiled unit still computes the same -------------------- diff --git a/test/integration/type-infer-phase3-test.janet b/test/integration/type-infer-phase3-test.janet index 89ecfc8..e9dc1c5 100644 --- a/test/integration/type-infer-phase3-test.janet +++ b/test/integration/type-infer-phase3-test.janet @@ -21,13 +21,13 @@ # a reduce closure's element param gets the vector's element type (def red "(defn f [coll] (reduce (fn [acc h] (+ acc (:r h))) 0 coll))") -(assert (= 0 (guards red @{"coll" {:vec :struct-map}})) "reduce element typed -> bare lookup in closure") +(assert (= 0 (guards red @{"coll" {:vec {:struct {}}}})) "reduce element typed -> bare lookup in closure") (assert (= 1 (guards red @{"coll" {:vec :any}})) "reduce over vector of unknown -> guard kept") (assert (= 1 (guards red @{})) "untyped coll -> guard kept") # mapv over a vector-of-structs types the closure element too (def mp "(defn g [coll] (mapv (fn [h] (:r h)) coll))") -(assert (= 0 (guards mp @{"coll" {:vec :struct-map}})) "mapv element typed -> bare lookup") +(assert (= 0 (guards mp @{"coll" {:vec {:struct {}}}})) "mapv element typed -> bare lookup") (assert (= 1 (guards mp @{"coll" {:vec :any}})) "mapv over unknown element -> guard") # element type is DERIVED, not just seeded: a vector literal of structs, reduced From 9867c33079b39516be8f057c2729f6e3a462f9ac Mon Sep 17 00:00:00 2001 From: Yogthos Date: Sat, 13 Jun 2026 11:00:58 -0400 Subject: [PATCH 10/20] =?UTF-8?q?feat:=20success-type=20checker=20(RFC=200?= =?UTF-8?q?006)=20=E2=80=94=20flag=20provably-wrong=20core=20calls?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Reuse the structural inference from RFC 0005 as a loose type checker. It reports a core-fn call only when an argument's inferred type is concrete and lies in that op's throwing error domain, and accepts everything ambiguous (:any, a union that joined to :any, :truthy). By construction it never produces a false positive: a correct program has nothing to report even in error mode. The curated error-domain table starts with the clearest throwing cases: arithmetic on a provable non-number, and count/first/rest/next/seq/nth on a provable non-seqable scalar. Lenient operations like (get 5 :k) and (:k 5), which return nil rather than throw, are deliberately not listed. Checking is decoupled from specialization: it runs whenever JOLT_TYPE_CHECK is warn or error, regardless of :inline?, reading the knob at compile time so no rebuild is needed. warn prints to stderr, error fails the form's compilation, off (the default) skips it entirely. Core init stays clean under the flag. jolt-y3b --- jolt-core/jolt/passes.clj | 126 +++++++++++++++++++++++++ src/jolt/backend.janet | 46 +++++++-- test/integration/type-check-test.janet | 57 +++++++++++ 3 files changed, 221 insertions(+), 8 deletions(-) create mode 100644 test/integration/type-check-test.janet diff --git a/jolt-core/jolt/passes.clj b/jolt-core/jolt/passes.clj index f035353..6204be4 100644 --- a/jolt-core/jolt/passes.clj +++ b/jolt-core/jolt/passes.clj @@ -794,6 +794,7 @@ (def ^:private rtenv-box (atom {})) ;; "ns/name" -> inferred return type (def ^:private calls-box (atom [])) ;; collected [ "ns/name" [arg-types...] ] (def ^:private escapes-box (atom #{})) ;; var-keys used as a VALUE (not a call head) +(def ^:private diag-box (atom [])) ;; success-type-check diagnostics (RFC 0006) ;; jolt-d6u: a var reference's VALUE type — a fn var is :truthy (non-nil), a def ;; var carries its inferred init type (e.g. a color table -> {:vec :struct-map}). ;; The orchestrator populates this from sealed (opt-mode) cell roots + def inits. @@ -1034,6 +1035,121 @@ (defn- infer-top [node] (nth (infer node {}) 1)) +;; --------------------------------------------------------------------------- +;; Success-type checking (RFC 0006). Reuse the inference above as a loose type +;; checker: flag a core-fn call ONLY when an argument's inferred type is +;; concrete AND lies in that op's error domain (the op provably throws on it). +;; Everything ambiguous — :any, :truthy (true/char/...), :nil — is accepted, so +;; there are no false positives. The table is curated to genuinely-throwing +;; cases; lenient ops ((get 5 :k) -> nil, (:k 5) -> nil) are NOT listed. + +;; concrete non-numbers: arithmetic provably throws on these. +(defn- not-number? [t] + (or (= t :str) (= t :kw) (= t :phm) + (struct-type? t) (vec-type? t) (set-type? t))) + +;; concrete non-seqable scalars: seq/count/first/nth provably throw on these. +;; (Strings and collections ARE seqable/countable; :truthy is ambiguous; :nil +;; and :any are accepted.) +(defn- not-seqable? [t] (or (= t :num) (= t :kw))) + +;; arithmetic / numeric ops: EVERY argument must be a number. +(def ^:private num-ops + #{"+" "-" "*" "/" "inc" "dec" "mod" "rem" "quot" "min" "max" "abs" + "bit-and" "bit-or" "bit-xor" "bit-not" "bit-shift-left" "bit-shift-right"}) +;; seq/count/index ops: argument 0 must be seqable/countable. +(def ^:private seq-ops #{"count" "first" "rest" "next" "seq" "nth"}) + +(defn- type-name + "Render an inferred type for an error message." + [t] + (cond (struct-type? t) "a map" + (vec-type? t) "a vector" + (set-type? t) "a set" + (= t :str) "a string" + (= t :kw) "a keyword" + (= t :num) "a number" + (= t :phm) "a map" + :else (str t))) + +(defn- check-invoke + "If node is a core-op call whose argument type is provably in the error domain, + conj a diagnostic. arg-types is the vector of inferred argument types." + [cn args arg-types] + (cond + (contains? num-ops cn) + (reduce (fn [_ i] + (let [t (nth arg-types i)] + (when (not-number? t) + (swap! diag-box conj + {:op cn :argpos i :type (type-name t) + :msg (str "`" cn "` requires a number, but argument " + (inc i) " is " (type-name t))}))) + nil) + nil (range (count args))) + (and (contains? seq-ops cn) (> (count args) 0)) + (let [t (nth arg-types 0)] + (when (not-seqable? t) + (swap! diag-box conj + {:op cn :argpos 0 :type (type-name t) + :msg (str "`" cn "` requires " + (if (= cn "count") "a countable collection" "a seqable") + ", but argument 1 is " (type-name t))}))) + :else nil)) + +(defn- check-walk + "Walk the IR, inferring argument types and recording diagnostics for + provably-wrong core-fn calls. Threads tenv through binders exactly like infer." + [node tenv] + (let [op (get node :op)] + (cond + (= op :invoke) + (let [fnode (get node :fn) + args (get node :args) + cn (when (and (= :var (get fnode :op)) (= "clojure.core" (get fnode :ns))) + (get fnode :name))] + (when cn + (check-invoke cn args (mapv (fn [a] (nth (infer a tenv) 0)) args))) + (check-walk fnode tenv) + (reduce (fn [_ a] (check-walk a tenv) nil) nil args)) + (= op :let) + (let [te (reduce (fn [e b] + (check-walk (nth b 1) e) + (assoc e (nth b 0) (nth (infer (nth b 1) e) 0))) + tenv (get node :bindings))] + (check-walk (get node :body) te)) + (= op :if) + (do (check-walk (get node :test) tenv) + (check-walk (get node :then) tenv) + (check-walk (get node :else) tenv)) + (= op :do) + (do (reduce (fn [_ s] (check-walk s tenv) nil) nil (get node :statements)) + (check-walk (get node :ret) tenv)) + (= op :fn) + (reduce (fn [_ a] + (let [pe (reduce (fn [e p] (assoc e p :any)) tenv (get a :params)) + pe (if (get a :rest) (assoc pe (get a :rest) :any) pe)] + (check-walk (get a :body) pe)) + nil) + nil (get node :arities)) + (= op :loop) + (do (reduce (fn [_ b] (check-walk (nth b 1) tenv) nil) nil (get node :bindings)) + (check-walk (get node :body) tenv)) + (= op :recur) + (reduce (fn [_ a] (check-walk a tenv) nil) nil (get node :args)) + (= op :def) (check-walk (get node :init) tenv) + (= op :throw) (check-walk (get node :expr) tenv) + (= op :vector) (reduce (fn [_ x] (check-walk x tenv) nil) nil (get node :items)) + (= op :set) (reduce (fn [_ x] (check-walk x tenv) nil) nil (get node :items)) + (= op :map) + (reduce (fn [_ pr] (check-walk (nth pr 0) tenv) (check-walk (nth pr 1) tenv) nil) + nil (get node :pairs)) + (= op :try) + (do (check-walk (get node :body) tenv) + (when (get node :catch-body) (check-walk (get node :catch-body) tenv)) + (when (get node :finally) (check-walk (get node :finally) tenv))) + :else nil))) + ;; --- Inter-procedural driver API (jolt-767) consumed by the back end -------- (defn set-rtenv! "Install the current return-type estimates (a map \"ns/name\" -> type) used to @@ -1053,6 +1169,16 @@ (defn reset-escapes! [] (reset! escapes-box #{})) (defn collected-escapes [] (vec @escapes-box)) +(defn check-form + "Success-type check a single analyzed form (RFC 0006). Returns a vector of + diagnostics [{:op :argpos :type :msg} ...] for provably-wrong core-fn calls; + empty when nothing is provably wrong. Runs independently of specialization so + it is usable in normal builds (the decoupled checking path)." + [node] + (reset! diag-box []) + (check-walk node {}) + (vec @diag-box)) + (defn infer-body "Type `body` under tenv (local-name -> type). Returns [ret-type node' calls], where calls is the [[\"ns/name\" [arg-types...]] ...] this body invokes (for diff --git a/src/jolt/backend.janet b/src/jolt/backend.janet index f9247e7..7cdf9e3 100644 --- a/src/jolt/backend.janet +++ b/src/jolt/backend.janet @@ -613,6 +613,27 @@ [ctx] (build-compiler! ctx)) +(defn type-check! + "Success-type check the analyzed IR (RFC 0006). Looks up jolt.passes/check-form + (absent during pre-passes bootstrap -> no-op), runs it protected so a checker + bug never breaks compilation, then reports each diagnostic per strictness: + `warn` prints to stderr, `error` throws (failing this form's compilation). + Because the checker only fires on PROVABLY-wrong code, a correct program has + nothing to report under either level." + [ctx ir strictness ns] + (def cf (ns-find (ctx-find-ns ctx "jolt.passes") "check-form")) + (when cf + (def r (protect ((var-get cf) ir))) + (when (r 0) + (def diags (if (pv/pvec? (r 1)) (pv/pv->array (r 1)) (r 1))) + (when (and diags (> (length diags) 0)) + (def loc (if ns (string ns) "?")) + (each d diags + (def msg (string "type error in " loc ": " (get d :msg))) + (if (= strictness "error") + (error msg) + (eprint " " msg))))))) + (defn analyze-form "Run the portable Clojure analyzer (jolt.analyzer/analyze) on a reader form, returning host-neutral IR." @@ -645,14 +666,23 @@ # Resolved lazily; absent during the pre-passes bootstrap window. (def pv (unless (= "1" (os/getenv "JOLT_NO_IR_PASSES")) (ns-find (ctx-find-ns ctx "jolt.passes") "run-passes"))) - (if pv - (let [pr (protect ((var-get pv) (r 1) ctx))] - # the pass runs interpreted; a throw inside it unwinds past the - # interpreter's ns restores — put the compile ns back either way, or - # the REST of this compilation resolves in jolt.passes - (ctx-set-current-ns ctx saved-ns) - (if (pr 0) (pr 1) (r 1))) - (r 1))) + (def result + (if pv + (let [pr (protect ((var-get pv) (r 1) ctx))] + # the pass runs interpreted; a throw inside it unwinds past the + # interpreter's ns restores — put the compile ns back either way, or + # the REST of this compilation resolves in jolt.passes + (ctx-set-current-ns ctx saved-ns) + (if (pr 0) (pr 1) (r 1))) + (r 1))) + # Success-type check (RFC 0006), decoupled from specialization: runs whenever + # JOLT_TYPE_CHECK is warn/error, regardless of :inline?. Read at runtime so it + # needs no rebuild. The analyzed IR (r 1) carries no specialization; the + # checker does its own inference. + (def tc (os/getenv "JOLT_TYPE_CHECK")) + (when (and tc (not= tc "off") (not= tc "0")) + (type-check! ctx (r 1) tc saved-ns)) + result) # The analyzer's deliberate punt signal — (uncompilable why) throws the string # "jolt/uncompilable: ". Anything else escaping the compile step is an diff --git a/test/integration/type-check-test.janet b/test/integration/type-check-test.janet new file mode 100644 index 0000000..0804c0c --- /dev/null +++ b/test/integration/type-check-test.janet @@ -0,0 +1,57 @@ +# Success-type checking (RFC 0006, jolt-y3b). The structural inference of +# RFC 0005, reused as a loose checker: flag a core-fn call ONLY when an argument +# is PROVABLY the wrong type (concrete and in the op's throwing error domain). +# Ambiguous cases (:any, unions, :truthy) are accepted — no false positives. +(import ../../src/jolt/api :as api) +(import ../../src/jolt/backend :as backend) +(import ../../src/jolt/types :as types) +(import ../../src/jolt/reader :as reader) + +(print "Success-type checking (jolt-y3b)...") + +(os/setenv "JOLT_DIRECT_LINK" "1") +(def ctx (api/init {:compile? true})) +(def pns (types/ctx-find-ns ctx "jolt.passes")) +(def check (types/var-get (types/ns-find pns "check-form"))) + +# diagnostics (a Janet tuple of diag structs) for a source form +(defn diags [src] + (api/normalize-pvecs (check (backend/analyze-form ctx (reader/parse-string src))))) +(defn nd [src] (length (diags src))) + +# --- provably wrong: REPORTED ------------------------------------------------ +(assert (= 1 (nd "(inc \"x\")")) "inc on a string") +(assert (= 1 (nd "(+ 1 \"x\")")) "+ with a string arg") +(assert (= 1 (nd "(count :foo)")) "count of a keyword") +(assert (= 1 (nd "(count 5)")) "count of a number") +(assert (= 1 (nd "(first 42)")) "first of a number") +(assert (= 1 (nd "(nth :k 0)")) "nth of a keyword") +(assert (= 1 (nd "(let [n \"x\"] (inc n))")) "inc on a let-bound string") +(assert (= 1 (nd "(inc (count :k))")) "inner count of keyword reported (inc of :num is fine)") + +# --- ambiguous / lenient: ACCEPTED (no false positive) ----------------------- +(assert (= 0 (nd "(:k 5)")) "keyword lookup on a number returns nil, not an error") +(assert (= 0 (nd "(get 5 :k)")) "get on a number returns nil, not an error") +(assert (= 0 (nd "(fn [x] (inc x))")) "inc on an unknown (:any) param accepted") +(assert (= 0 (nd "(fn [c] (inc (if c 1 \"x\")))")) "inc on a {:num | :str} branch -> :any, accepted") +(assert (= 0 (nd "(count \"ab\")")) "count of a string is fine") +(assert (= 0 (nd "(count [1 2 3])")) "count of a vector is fine") +(assert (= 0 (nd "(first [1 2 3])")) "first of a vector is fine") +(assert (= 0 (nd "(inc (count [1 2 3]))")) "count of vector + inc of :num both fine") +(assert (= 0 (nd "(inc (first [1 2 3]))")) "first of vector -> :num, inc fine") + +# --- the diagnostic carries op + type + a message ---------------------------- +(def one (in (diags "(inc \"x\")") 0)) +(assert (= "inc" (get one :op)) "diagnostic names the op") +(assert (string/find "number" (get one :msg)) "message says a number is required") + +# --- end-to-end: strictness drives compilation (decoupled from :inline?) ----- +# error mode aborts a provably-wrong form's compilation; a correct form compiles. +(os/setenv "JOLT_TYPE_CHECK" "error") +(assert (not (first (protect (api/eval-string ctx "(count :nope)")))) + "error mode aborts a provably-wrong form") +(assert (first (protect (api/eval-string ctx "(count [1 2 3])"))) + "error mode accepts a correct form") +(os/setenv "JOLT_TYPE_CHECK" "off") + +(print "Success-type checking passed!") From 1c0b3fe9bd4f1aa3754ba89cb71fbd0b294e713e Mon Sep 17 00:00:00 2001 From: Yogthos Date: Sat, 13 Jun 2026 11:01:42 -0400 Subject: [PATCH 11/20] docs: mark RFC 0005/0006 implemented, note follow-up work --- docs/rfc/0005-structural-type-inference.md | 3 ++- docs/rfc/0006-success-type-checking.md | 5 ++++- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/docs/rfc/0005-structural-type-inference.md b/docs/rfc/0005-structural-type-inference.md index 872ae3a..635e15c 100644 --- a/docs/rfc/0005-structural-type-inference.md +++ b/docs/rfc/0005-structural-type-inference.md @@ -1,6 +1,7 @@ # RFC 0005 — Structural collection-type inference -- **Status**: Draft +- **Status**: Implemented (jolt-5uj). Ray tracer 12.8s to 11.0s hint-free, + matching the explicit `^:struct` version; render checksum unchanged. - **Champions**: jolt maintainers - **Created**: 2026-06-13 diff --git a/docs/rfc/0006-success-type-checking.md b/docs/rfc/0006-success-type-checking.md index e67da5e..ee6442d 100644 --- a/docs/rfc/0006-success-type-checking.md +++ b/docs/rfc/0006-success-type-checking.md @@ -1,6 +1,9 @@ # RFC 0006 — Compile-time detection of provably-wrong code (success typing) -- **Status**: Draft +- **Status**: Implemented (jolt-y3b), first table. Core-fn error domains + (arithmetic on non-numbers, count/first/rest/next/seq/nth on non-seqable + scalars), `JOLT_TYPE_CHECK=off|warn|error`, decoupled from specialization. + Precise source locations (file:line:col) remain follow-up work. - **Champions**: jolt maintainers - **Created**: 2026-06-13 - **Depends on**: RFC 0005 (structural collection-type inference) From 9f076937af77453aac640f4fa8ff3f2c1dd1df57 Mon Sep 17 00:00:00 2001 From: Yogthos Date: Sat, 13 Jun 2026 11:39:55 -0400 Subject: [PATCH 12/20] feat: bounded union types in the RFC 0005 lattice (jolt-pz5) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The success checker (RFC 0006) used to lose differing if-branches to :any and accept the use. (inc (if c "a" :k)) typed the if as :any — sound but imprecise, since the value is provably {:str | :kw}, every member of which is in inc's error domain. Adds {:union #{T...}} to the lattice: join-t forms a scalar union of differing branches instead of collapsing to :any, capped at 4 distinct scalars (the member space is the five scalar tags, so the lattice stays finite and the inter-procedural fixpoint still terminates). The checker's not-number?/not-seqable? report a union only when EVERY member is in the error domain — any valid member accepts the call, so still no false positives. type-name renders "a string or a keyword". Unions are scalar-only and carry no :struct/:vec/:set key, so every structural predicate already treats them as opaque — specialization sees them exactly as :any and codegen is unchanged. Gate green, suite 4718, conformance 335/335, bench even. --- jolt-core/jolt/passes.clj | 62 +++++++++++++++++++++++--- test/integration/type-check-test.janet | 20 +++++++++ 2 files changed, 75 insertions(+), 7 deletions(-) diff --git a/jolt-core/jolt/passes.clj b/jolt-core/jolt/passes.clj index 6204be4..c74f035 100644 --- a/jolt-core/jolt/passes.clj +++ b/jolt-core/jolt/passes.clj @@ -737,6 +737,40 @@ (defn- mk-vec [t] {:vec (if t t :any)}) (defn- mk-set [t] {:set (if t t :any)}) (defn- mk-struct [fs] {:struct fs}) + +;; Bounded union types (RFC 0006 / jolt-pz5). A union {:union #{T...}} records +;; that a value is provably one of a small, fixed set of SCALAR types — what +;; differing if-branches used to collapse to :any. It exists so the success +;; checker can reject a use where EVERY member is in the op's error domain +;; ((inc (if c "a" :k))) while still accepting one where any member is valid +;; ((inc (if c 1 "x"))). Scalars only, capped cardinality: the member space is +;; the five scalar tags, so the lattice stays finite and the inter-procedural +;; fixpoint terminates. A union is opaque to every STRUCTURAL predicate +;; (struct-type?/vec-type?/set-type? key on :struct/:vec/:set, which a union +;; lacks), so specialization treats it exactly like :any — codegen is +;; unchanged; only the checker reads inside it. +(def ^:private union-cap 4) +(defn- scalar-t? [t] (or (= t :num) (= t :str) (= t :kw) (= t :truthy) (= t :phm))) +(defn- union-type? [t] (some? (get t :union))) +(defn- umembers [t] (get t :union)) +(defn- union-of + "Normalize a seq of member types into a lattice value: flatten nested unions, + keep only scalars (any non-scalar member collapses the whole thing to :any, + the conservative top), then return the lone member if one, {:union #{...}} + for 2..cap distinct scalars, or :any past the cap." + [ts] + (let [flat (reduce (fn [acc t] + (if (union-type? t) + (reduce conj acc (umembers t)) + (conj acc t))) + #{} ts)] + (cond + (not (every? scalar-t? flat)) :any + (= 0 (count flat)) :any + (= 1 (count flat)) (first flat) + (> (count flat) union-cap) :any + :else {:union flat}))) + (declare join-t) (defn- merge-fields "Per-field join of two field maps (a key in only one side joins with :any)." @@ -751,7 +785,11 @@ (and (struct-type? a) (struct-type? b)) (mk-struct (merge-fields (sfields a) (sfields b))) (and (vec-type? a) (vec-type? b)) (mk-vec (join-t (velem a) (velem b))) (and (set-type? a) (set-type? b)) (mk-set (join-t (selem a) (selem b))) - :else :any)) + ;; differing kinds: form a scalar union when both sides reduce to scalars + ;; (or scalar unions); anything compound on either side stays :any (jolt-pz5) + :else (let [ma (cond (union-type? a) (umembers a) (scalar-t? a) #{a} :else nil) + mb (cond (union-type? b) (umembers b) (scalar-t? b) #{b} :else nil)] + (if (and ma mb) (union-of (reduce conj ma mb)) :any)))) (defn- join [a b] (join-t a b)) ;; depth cap (RFC 0005): truncate a type below depth d to :any, so recursive data ;; can't make an infinite type and the inter-procedural fixpoint stays finite. @@ -1043,15 +1081,22 @@ ;; there are no false positives. The table is curated to genuinely-throwing ;; cases; lenient ops ((get 5 :k) -> nil, (:k 5) -> nil) are NOT listed. -;; concrete non-numbers: arithmetic provably throws on these. +;; concrete non-numbers: arithmetic provably throws on these. A union is in the +;; error domain only when EVERY member is (jolt-pz5) — if any member is an +;; accepted type the call is accepted (no false positive). (defn- not-number? [t] - (or (= t :str) (= t :kw) (= t :phm) - (struct-type? t) (vec-type? t) (set-type? t))) + (if (union-type? t) + (every? not-number? (umembers t)) + (or (= t :str) (= t :kw) (= t :phm) + (struct-type? t) (vec-type? t) (set-type? t)))) ;; concrete non-seqable scalars: seq/count/first/nth provably throw on these. ;; (Strings and collections ARE seqable/countable; :truthy is ambiguous; :nil -;; and :any are accepted.) -(defn- not-seqable? [t] (or (= t :num) (= t :kw))) +;; and :any are accepted.) A union throws only when every member does. +(defn- not-seqable? [t] + (if (union-type? t) + (every? not-seqable? (umembers t)) + (or (= t :num) (= t :kw)))) ;; arithmetic / numeric ops: EVERY argument must be a number. (def ^:private num-ops @@ -1063,7 +1108,10 @@ (defn- type-name "Render an inferred type for an error message." [t] - (cond (struct-type? t) "a map" + (cond (union-type? t) + (reduce (fn [s m] (if (= s "") (type-name m) (str s " or " (type-name m)))) + "" (umembers t)) + (struct-type? t) "a map" (vec-type? t) "a vector" (set-type? t) "a set" (= t :str) "a string" diff --git a/test/integration/type-check-test.janet b/test/integration/type-check-test.janet index 0804c0c..b77f340 100644 --- a/test/integration/type-check-test.janet +++ b/test/integration/type-check-test.janet @@ -40,6 +40,26 @@ (assert (= 0 (nd "(inc (count [1 2 3]))")) "count of vector + inc of :num both fine") (assert (= 0 (nd "(inc (first [1 2 3]))")) "first of vector -> :num, inc fine") +# --- bounded unions (jolt-pz5): report only when EVERY member is in the error +# domain; accept when any member is valid. Differing branches used to collapse +# to :any (accepted); now they form {:union #{...}} and are checked per-member. +(assert (= 1 (nd "(fn [c] (inc (if c \"a\" :k)))")) + "inc of {:str | :kw} — every member non-number — reported") +(assert (= 0 (nd "(fn [c] (inc (if c 1 \"x\")))")) + "inc of {:num | :str} — :num is fine — still accepted") +(assert (= 1 (nd "(fn [c] (count (if c :k 5)))")) + "count of {:kw | :num} — both non-seqable — reported") +(assert (= 0 (nd "(fn [c] (count (if c :k \"ab\")))")) + "count of {:kw | :str} — :str is seqable — accepted") +(assert (= 1 (nd "(fn [c] (inc (if c \"a\" (if c :k :j))))")) + "inc of nested all-non-number union reported") +(assert (= 0 (nd "(fn [c] (inc (if c \"a\" (if c :k 1))))")) + "inc of union with a buried :num member accepted") +# a union is opaque to structural specialization — it keeps the dynamic guard, +# exactly like :any, so a keyword lookup over it is never mis-specialized. +(assert (= 0 (nd "(fn [c] (:r (if c {:r 1} {:g 2})))")) + "keyword lookup over a struct union is accepted (no false positive)") + # --- the diagnostic carries op + type + a message ---------------------------- (def one (in (diags "(inc \"x\")") 0)) (assert (= "inc" (get one :op)) "diagnostic names the op") From 824b30defda90eca5ba1c50092b1156502086538 Mon Sep 17 00:00:00 2001 From: Yogthos Date: Sat, 13 Jun 2026 11:56:21 -0400 Subject: [PATCH 13/20] feat: report provably-wrong calls to user functions, opt-in (jolt-zo1) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The success checker fired only against core-fn error domains (stable, not redefinable). This adds reporting of a call that passes a provably-wrong type to a USER fn whose body requires otherwise — e.g. a fn that only does arithmetic on a param, called with a string. As check-walk sees defs it registers each non-redefinable single-fixed-arity user fn's {:params :body} in module state (user-sig-box, accumulating across forms like rtenv-box — a def must precede its call). At a call site (strict mode only) the body is re-checked with ONE parameter bound to its concrete argument type, others :any; if that produces a diagnostic the all-:any body did not, the argument alone is provably wrong and the call is reported. Monotonic — binding a concrete type can only add error-domain hits — so still no false positives. A cycle guard (checking-box) terminates mutual recursion. Gated behind JOLT_TYPE_CHECK_USER (orthogonal to the warn/error level) because it rests on the closed-world assumption, weaker than the core-fn case. check-form gains a strict? arity; the default path is unchanged and user-fn code runs only when the checker is enabled. ^:redef/^:dynamic and multi/variadic fns are not registered (their body is no stable requirement). Gate green, suite 4718, conformance 335/335. --- jolt-core/jolt/passes.clj | 116 ++++++++++++++++++++++--- src/jolt/backend.janet | 10 ++- test/integration/type-check-test.janet | 25 ++++++ 3 files changed, 138 insertions(+), 13 deletions(-) diff --git a/jolt-core/jolt/passes.clj b/jolt-core/jolt/passes.clj index c74f035..63e221b 100644 --- a/jolt-core/jolt/passes.clj +++ b/jolt-core/jolt/passes.clj @@ -838,6 +838,17 @@ ;; The orchestrator populates this from sealed (opt-mode) cell roots + def inits. (def ^:private vtype-box (atom {})) ;; "ns/name" -> value type +;; User-function error domains (jolt-zo1), opt-in. As the checker walks defs it +;; registers each non-redefinable single-fixed-arity user fn's {:params :body} +;; here, keyed "ns/name". At a later call site (strict mode only) the body is +;; re-checked with ONE parameter bound to its concrete argument type — if that +;; alone produces a diagnostic the all-:any body did not, that argument is +;; provably wrong and the CALL is reported. Module state, like rtenv-box: a def +;; must precede its call (the same closed-world ordering RFC 0005 assumes). +(def ^:private user-sig-box (atom {})) ;; "ns/name" -> {:params [..] :body ir} +(def ^:private checking-box (atom #{})) ;; keys mid-recheck — cycle guard +(def ^:private strict-box (atom false)) ;; report against user-fn domains? + ;; fns that RETURN an element of their (first) collection arg, so a lookup on the ;; result of (rand-nth coll-of-structs) etc. types as the element. (def ^:private elem-fns #{"rand-nth" "first" "peek" "last" "nth" "fnext" "second"}) @@ -1145,6 +1156,75 @@ ", but argument 1 is " (type-name t))}))) :else nil)) +(declare check-walk) + +;; --- user-function error domains (jolt-zo1), opt-in -------------------------- +(defn- all-any-env + "tenv binding every param name to :any (the all-ambiguous baseline)." + [params] + (reduce (fn [e p] (assoc e p :any)) {} params)) + +(defn- isolated-diag-count + "Count of diagnostics check-walk produces for body under tenv, with the shared + diag-box saved and restored so this probe never leaks into the real report." + [body tenv] + (let [saved @diag-box] + (reset! diag-box []) + (check-walk body tenv) + (let [n (count @diag-box)] + (reset! diag-box saved) + n))) + +(defn- register-user-fn! + "Record a (def name (fn [params] body)) — single fixed arity, not redefinable — + for later user-fn call checking. Redefinable/dynamic and multi/variadic fns are + skipped (their body is not a stable requirement)." + [node] + (let [init (get node :init) + m (get node :meta) + redefable (and m (or (get m :redef) (get m :dynamic)))] + (when (and (not redefable) (= :fn (get init :op))) + (let [arities (get init :arities)] + (when (= 1 (count arities)) + (let [ar (first arities)] + (when (not (get ar :rest)) + (swap! user-sig-box assoc + (str (get node :ns) "/" (get node :name)) + {:name (get node :name) + :params (get ar :params) :body (get ar :body)})))))))) + +(defn- check-user-call + "Strict mode: report a call whose concrete argument type provably makes the + callee body throw. For each concrete arg, re-check the body with ONLY that + parameter bound to its arg type (others :any); a diagnostic the all-:any body + did not already have means the argument alone is provably wrong. Monotonic — + binding a concrete type can only ADD error-domain hits — so no false positive. + Cycle-guarded so mutually recursive fns terminate." + [key sig arg-types] + (when (not (contains? @checking-box key)) + (let [prev @checking-box] + (reset! checking-box (conj prev key)) + (let [params (:params sig) + body (:body sig) + base (isolated-diag-count body (all-any-env params)) + npar (count params) + nargs (count arg-types) + np (if (< npar nargs) npar nargs)] + (reduce + (fn [_ i] + (let [at (nth arg-types i)] + (when (and (not= at :any) (not= at :truthy)) + (let [pe (assoc (all-any-env params) (nth params i) at)] + (when (> (isolated-diag-count body pe) base) + (swap! diag-box conj + {:op :user-call :argpos i :type (type-name at) + :msg (str "argument " (inc i) " to `" (:name sig) + "` is " (type-name at) + ", which its body provably rejects")}))))) + nil) + nil (range np))) + (reset! checking-box prev)))) + (defn- check-walk "Walk the IR, inferring argument types and recording diagnostics for provably-wrong core-fn calls. Threads tenv through binders exactly like infer." @@ -1155,9 +1235,14 @@ (let [fnode (get node :fn) args (get node :args) cn (when (and (= :var (get fnode :op)) (= "clojure.core" (get fnode :ns))) - (get fnode :name))] - (when cn - (check-invoke cn args (mapv (fn [a] (nth (infer a tenv) 0)) args))) + (get fnode :name)) + ukey (when (= :var (get fnode :op)) + (str (get fnode :ns) "/" (get fnode :name))) + usig (when (and @strict-box ukey) (get @user-sig-box ukey))] + (when (or cn usig) + (let [ats (mapv (fn [a] (nth (infer a tenv) 0)) args)] + (when cn (check-invoke cn args ats)) + (when usig (check-user-call ukey usig ats)))) (check-walk fnode tenv) (reduce (fn [_ a] (check-walk a tenv) nil) nil args)) (= op :let) @@ -1185,7 +1270,7 @@ (check-walk (get node :body) tenv)) (= op :recur) (reduce (fn [_ a] (check-walk a tenv) nil) nil (get node :args)) - (= op :def) (check-walk (get node :init) tenv) + (= op :def) (do (register-user-fn! node) (check-walk (get node :init) tenv)) (= op :throw) (check-walk (get node :expr) tenv) (= op :vector) (reduce (fn [_ x] (check-walk x tenv) nil) nil (get node :items)) (= op :set) (reduce (fn [_ x] (check-walk x tenv) nil) nil (get node :items)) @@ -1219,13 +1304,22 @@ (defn check-form "Success-type check a single analyzed form (RFC 0006). Returns a vector of - diagnostics [{:op :argpos :type :msg} ...] for provably-wrong core-fn calls; - empty when nothing is provably wrong. Runs independently of specialization so - it is usable in normal builds (the decoupled checking path)." - [node] - (reset! diag-box []) - (check-walk node {}) - (vec @diag-box)) + diagnostics [{:op :argpos :type :msg} ...] for provably-wrong calls; empty + when nothing is provably wrong. Runs independently of specialization so it is + usable in normal builds (the decoupled checking path). + + With strict? true, also reports calls to registered user functions whose + concrete argument types provably make the body throw (jolt-zo1, opt-in, + closed-world). user-sig-box accumulates registered defs across forms, so a + def must precede its call — the same ordering RFC 0005 already assumes." + ([node] (check-form node false)) + ([node strict?] + (reset! strict-box (if strict? true false)) + (reset! checking-box #{}) + (reset! diag-box []) + (check-walk node {}) + (reset! strict-box false) + (vec @diag-box))) (defn infer-body "Type `body` under tenv (local-name -> type). Returns [ret-type node' calls], diff --git a/src/jolt/backend.janet b/src/jolt/backend.janet index 7cdf9e3..678fe05 100644 --- a/src/jolt/backend.janet +++ b/src/jolt/backend.janet @@ -619,11 +619,17 @@ bug never breaks compilation, then reports each diagnostic per strictness: `warn` prints to stderr, `error` throws (failing this form's compilation). Because the checker only fires on PROVABLY-wrong code, a correct program has - nothing to report under either level." + nothing to report under either level. + + JOLT_TYPE_CHECK_USER (an orthogonal opt-in knob, jolt-zo1) additionally + reports calls to user functions whose concrete argument types provably make + the body throw — sound only under the closed-world assumption, hence opt-in." [ctx ir strictness ns] (def cf (ns-find (ctx-find-ns ctx "jolt.passes") "check-form")) (when cf - (def r (protect ((var-get cf) ir))) + (def uenv (os/getenv "JOLT_TYPE_CHECK_USER")) + (def strict? (and uenv (not= uenv "0") (not= uenv "off"))) + (def r (protect ((var-get cf) ir strict?))) (when (r 0) (def diags (if (pv/pvec? (r 1)) (pv/pv->array (r 1)) (r 1))) (when (and diags (> (length diags) 0)) diff --git a/test/integration/type-check-test.janet b/test/integration/type-check-test.janet index b77f340..8c7e25f 100644 --- a/test/integration/type-check-test.janet +++ b/test/integration/type-check-test.janet @@ -18,6 +18,10 @@ (defn diags [src] (api/normalize-pvecs (check (backend/analyze-form ctx (reader/parse-string src))))) (defn nd [src] (length (diags src))) +# strict mode (jolt-zo1): also report provably-wrong calls to user fns +(defn nds [src] + (length (api/normalize-pvecs + (check (backend/analyze-form ctx (reader/parse-string src)) true)))) # --- provably wrong: REPORTED ------------------------------------------------ (assert (= 1 (nd "(inc \"x\")")) "inc on a string") @@ -60,6 +64,27 @@ (assert (= 0 (nd "(fn [c] (:r (if c {:r 1} {:g 2})))")) "keyword lookup over a struct union is accepted (no false positive)") +# --- user-function error domains (jolt-zo1), opt-in strict mode -------------- +# A call passing a provably-wrong type to a user fn whose body requires +# otherwise is reported ONLY in strict mode; the default level never fires on +# user fns (closed-world soundness boundary). +(assert (= 0 (nd "(do (defn ufa [x] (+ x 1)) (ufa \"s\"))")) + "user-fn wrong call NOT reported at the default level") +(assert (= 1 (nds "(do (defn ufa [x] (+ x 1)) (ufa \"s\"))")) + "strict: arithmetic fn called with a string is reported") +(assert (= 0 (nds "(do (defn ufb [x] (+ x 1)) (ufb 5))")) + "strict: same fn called with a number is accepted") +(assert (= 0 (nds "(do (defn ufc [x] (:k x)) (ufc \"s\"))")) + "strict: a body that uses the param leniently is not reported") +# cross-form: a def registered by an earlier check is visible to a later call +(nds "(defn ufd [x] (count x))") +(assert (= 1 (nds "(ufd 42)")) + "strict: cross-form call to a seq-only fn with a number is reported") +(assert (= 0 (nds "(do (defn ^:redef ufe [x] (+ x 1)) (ufe \"s\"))")) + "strict: a ^:redef fn is not a stable requirement, not reported") +(assert (= 1 (nds "(do (defn ufrec [x] (ufrec (+ x 1))) (ufrec \"s\"))")) + "strict: self-recursion terminates (cycle guard) and the (+ x 1) on a string is reported once") + # --- the diagnostic carries op + type + a message ---------------------------- (def one (in (diags "(inc \"x\")") 0)) (assert (= "inc" (get one :op)) "diagnostic names the op") From f2d65addc8d8600df9f092e054c3aff62d28c2f8 Mon Sep 17 00:00:00 2001 From: Yogthos Date: Sat, 13 Jun 2026 12:18:53 -0400 Subject: [PATCH 14/20] feat: precise file:line:col source locations for type errors (jolt-fqy) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit RFC 0006 error reporting wanted file:line:col but IR nodes carried no position, so diagnostics read only "type error in : ". Now: type error /tmp/scene.clj:5:5: `inc` requires a number, but argument 1 is a string The reader records each LIST form's absolute start offset in a table keyed by form identity (lists are fresh arrays, never interned), gated behind a flag the loaders enable only when JOLT_TYPE_CHECK is on — zero cost off. Keying by identity makes positions survive macroexpansion exactly when the user's own sub-form is spliced through, and absent for macro-synthesized structure: a `(inc :k)` written inside `(when c ...)` reports at its own line, never at the expansion's generated if/do. The analyzer stamps the offset onto :invoke nodes (form-position host contract fn); the checker carries it into each diagnostic as :pos; the loaders stash the file's source + path on the env (save/restored across nested requires); backend/type-check! converts offset -> line:col via the reader's line-col and renders the RFC format. Falls back to the ns when no position is available (synthetic forms), so it is never worse than before. Gate green, conformance 335/335, suite 4718, runtime bench even (positions are compile-time only; off by default). --- jolt-core/jolt/analyzer.clj | 11 +++++-- jolt-core/jolt/passes.clj | 20 ++++++------ src/jolt/api.janet | 5 +++ src/jolt/backend.janet | 15 +++++++-- src/jolt/evaluator.janet | 14 ++++++++- src/jolt/host_iface.janet | 6 +++- src/jolt/loader.janet | 4 +++ src/jolt/reader.janet | 42 +++++++++++++++++++++++++- test/integration/type-check-test.janet | 6 ++++ 9 files changed, 106 insertions(+), 17 deletions(-) diff --git a/jolt-core/jolt/analyzer.clj b/jolt-core/jolt/analyzer.clj index 2ce9f44..f56ee38 100644 --- a/jolt-core/jolt/analyzer.clj +++ b/jolt-core/jolt/analyzer.clj @@ -23,7 +23,7 @@ form-map-pairs form-set-items form-special? compile-ns form-macro? form-expand-1 resolve-global form-sym-meta host-intern! form-syntax-quote-lower - record-type?]])) + record-type? form-position]])) (declare analyze) @@ -250,8 +250,13 @@ (and (form-sym? head) (not shadowed) (form-macro? ctx head)) (analyze ctx (form-expand-1 ctx form) env) :else - (invoke (analyze ctx head env) - (mapv #(analyze ctx % env) (rest items)))))))) + ;; stamp the list form's source offset onto the :invoke (jolt-fqy) + ;; so the success checker can report file:line:col. nil when the + ;; reader did not record it (synthetic/macro-built forms). + (let [n (invoke (analyze ctx head env) + (mapv #(analyze ctx % env) (rest items))) + p (form-position form)] + (if p (assoc n :pos p) n))))))) (defn analyze ([ctx form] (analyze ctx form (empty-env))) diff --git a/jolt-core/jolt/passes.clj b/jolt-core/jolt/passes.clj index 63e221b..4306599 100644 --- a/jolt-core/jolt/passes.clj +++ b/jolt-core/jolt/passes.clj @@ -1133,15 +1133,16 @@ (defn- check-invoke "If node is a core-op call whose argument type is provably in the error domain, - conj a diagnostic. arg-types is the vector of inferred argument types." - [cn args arg-types] + conj a diagnostic. arg-types is the vector of inferred argument types; pos is + the call form's source offset (jolt-fqy), carried into each diagnostic." + [cn args arg-types pos] (cond (contains? num-ops cn) (reduce (fn [_ i] (let [t (nth arg-types i)] (when (not-number? t) (swap! diag-box conj - {:op cn :argpos i :type (type-name t) + {:op cn :argpos i :type (type-name t) :pos pos :msg (str "`" cn "` requires a number, but argument " (inc i) " is " (type-name t))}))) nil) @@ -1150,7 +1151,7 @@ (let [t (nth arg-types 0)] (when (not-seqable? t) (swap! diag-box conj - {:op cn :argpos 0 :type (type-name t) + {:op cn :argpos 0 :type (type-name t) :pos pos :msg (str "`" cn "` requires " (if (= cn "count") "a countable collection" "a seqable") ", but argument 1 is " (type-name t))}))) @@ -1200,7 +1201,7 @@ did not already have means the argument alone is provably wrong. Monotonic — binding a concrete type can only ADD error-domain hits — so no false positive. Cycle-guarded so mutually recursive fns terminate." - [key sig arg-types] + [key sig arg-types pos] (when (not (contains? @checking-box key)) (let [prev @checking-box] (reset! checking-box (conj prev key)) @@ -1217,7 +1218,7 @@ (let [pe (assoc (all-any-env params) (nth params i) at)] (when (> (isolated-diag-count body pe) base) (swap! diag-box conj - {:op :user-call :argpos i :type (type-name at) + {:op :user-call :argpos i :type (type-name at) :pos pos :msg (str "argument " (inc i) " to `" (:name sig) "` is " (type-name at) ", which its body provably rejects")}))))) @@ -1240,9 +1241,10 @@ (str (get fnode :ns) "/" (get fnode :name))) usig (when (and @strict-box ukey) (get @user-sig-box ukey))] (when (or cn usig) - (let [ats (mapv (fn [a] (nth (infer a tenv) 0)) args)] - (when cn (check-invoke cn args ats)) - (when usig (check-user-call ukey usig ats)))) + (let [ats (mapv (fn [a] (nth (infer a tenv) 0)) args) + pos (get node :pos)] + (when cn (check-invoke cn args ats pos)) + (when usig (check-user-call ukey usig ats pos)))) (check-walk fnode tenv) (reduce (fn [_ a] (check-walk a tenv) nil) nil args)) (= op :let) diff --git a/src/jolt/api.janet b/src/jolt/api.janet index ed1d6b8..c657829 100644 --- a/src/jolt/api.janet +++ b/src/jolt/api.janet @@ -369,5 +369,10 @@ Returns the result of the last form evaluated." [ctx s &opt file] (default file "") + # record form positions so the checker can report file:line:col (jolt-fqy) + (when (checker-enabled?) + (track-positions! true) + (put (ctx :env) :tc-source s) + (put (ctx :env) :tc-file file)) (eval-forms-positioned ctx (parse-all-positioned s file) file)) diff --git a/src/jolt/backend.janet b/src/jolt/backend.janet index 678fe05..5181eb5 100644 --- a/src/jolt/backend.janet +++ b/src/jolt/backend.janet @@ -633,9 +633,20 @@ (when (r 0) (def diags (if (pv/pvec? (r 1)) (pv/pv->array (r 1)) (r 1))) (when (and diags (> (length diags) 0)) - (def loc (if ns (string ns) "?")) + # source + file for offset -> line:col (jolt-fqy). The loader stashes the + # current file's source + path on the env when checking is on. + (def src (get (ctx :env) :tc-source)) + (def file (or (get (ctx :env) :tc-file) (and ns (string ns)))) (each d diags - (def msg (string "type error in " loc ": " (get d :msg))) + (def off (get d :pos)) + # precise: file:line:col of the offending form when its offset and the + # source are both available; else the ns (no worse than before) + (def loc + (if (and off src) + (let [lc (r/line-col src off)] + (string (or file "?") ":" (in lc 0) ":" (in lc 1))) + (string "in " (if ns (string ns) "?")))) + (def msg (string "type error " loc ": " (get d :msg))) (if (= strictness "error") (error msg) (eprint " " msg))))))) diff --git a/src/jolt/evaluator.janet b/src/jolt/evaluator.janet index 694b783..72cc465 100644 --- a/src/jolt/evaluator.janet +++ b/src/jolt/evaluator.janet @@ -375,6 +375,18 @@ [ctx src &opt file] (default file "") (def toplevel (get (ctx :env) :toplevel-eval)) + # a require runs nested inside an outer file's eval; save/restore the outer + # checker source so its later forms still convert offsets correctly (jolt-fqy) + (def checking (checker-enabled?)) + (def saved-src (and checking (get (ctx :env) :tc-source))) + (def saved-file (and checking (get (ctx :env) :tc-file))) + (when checking + (track-positions! true) + (put (ctx :env) :tc-source src) + (put (ctx :env) :tc-file file)) + (defer (when checking + (put (ctx :env) :tc-source saved-src) + (put (ctx :env) :tc-file saved-file)) (each [f line] (parse-all-positioned src file) (try (if toplevel (toplevel ctx f) (eval-form ctx @{} f)) @@ -388,7 +400,7 @@ (when (nil? (get env :error-loading)) (put env :error-loading @[])) (def chain (get env :error-loading)) (when (not= (last chain) file) (array/push chain file)) - (propagate err fib))))) + (propagate err fib)))))) (defn- maybe-require-ns "If namespace ns-name isn't populated yet, load its source — from a file on the diff --git a/src/jolt/host_iface.janet b/src/jolt/host_iface.janet index aed1a76..2bcf20e 100644 --- a/src/jolt/host_iface.janet +++ b/src/jolt/host_iface.janet @@ -194,6 +194,10 @@ # with it would recurse forever. (defn h-ref-get [tab key] (get tab key)) +# Absolute source offset of a list FORM (jolt-fqy), or nil. The analyzer stamps +# it onto :invoke nodes so the success checker can report file:line:col. +(defn h-form-position [form] (rdr/form-pos form)) + # --------------------------------------------------------------------------- # Inline registry (jolt-87f, Route 1 AOT escape analysis). The inline pass # (jolt.passes) is portable Clojure and can't read Janet var cells, so it asks @@ -246,7 +250,7 @@ "form-syntax-quote-lower" h-syntax-quote-lower "host-intern!" h-intern! "inline-enabled?" h-inline-enabled? "inline-ir" h-inline-ir - "record-type?" h-record-type?}) + "record-type?" h-record-type? "form-position" h-form-position}) (defn install! [ctx] (def ns (ctx-find-ns ctx "jolt.host")) diff --git a/src/jolt/loader.janet b/src/jolt/loader.janet index 70a76b6..d7e2028 100644 --- a/src/jolt/loader.janet +++ b/src/jolt/loader.janet @@ -112,6 +112,10 @@ (load-ns ctx filepath) → namespace symbol string" [ctx filepath] (def source (slurp filepath)) + (when (checker-enabled?) + (track-positions! true) + (put (ctx :env) :tc-source source) + (put (ctx :env) :tc-file filepath)) (def pairs (parse-all-positioned source filepath)) (var ns-name nil) (each [form _] pairs diff --git a/src/jolt/reader.janet b/src/jolt/reader.janet index 7b01ec9..a6220f7 100644 --- a/src/jolt/reader.janet +++ b/src/jolt/reader.janet @@ -14,6 +14,41 @@ # Forward declaration for mutual recursion (var read-form nil) +# Source-position tracking for the success checker (jolt-fqy). When enabled, the +# reader records each LIST form's absolute start offset (lists are the forms that +# become :invoke nodes — what the checker reports on). Off by default: a flag +# check per list is the only cost when the checker isn't running. Keyed by form +# IDENTITY (lists are fresh arrays, never interned), so a position survives +# macroexpansion exactly when the user's own sub-form is spliced through, and is +# absent for macro-synthesized structure — which is what we want (fall back to +# the call site). Not cleared between parses: nested parses (a require mid-load) +# would otherwise drop an outer file's positions; the table is bounded by forms +# compiled this process and only populated when the checker is on. +(def form-pos-table @{}) +(var track-positions false) +(var pos-base 0) # absolute offset of the slice read-form currently sees + +(defn track-positions! + "Enable/disable list-form position recording (jolt-fqy)." + [on] (set track-positions on)) + +(defn set-pos-base! + "Tell the reader the absolute offset of the slice it is about to read, so + recorded list positions are absolute (parse-all-positioned reads a shrinking + remainder)." + [b] (set pos-base b)) + +(defn form-pos + "Absolute start offset recorded for a list form, or nil." + [form] (get form-pos-table form)) + +(defn checker-enabled? + "True when JOLT_TYPE_CHECK selects a non-off level — the loaders use this to + decide whether to record form positions for the checker (jolt-fqy)." + [] + (def tc (os/getenv "JOLT_TYPE_CHECK")) + (if (and tc (not= tc "off") (not= tc "0")) true false)) + (def whitespace-chars " \t\n\r,") (defn whitespace? [c] @@ -624,7 +659,9 @@ # list (= c 40) - (read-list s pos) + (let [r (read-list s pos)] + (when track-positions (put form-pos-table (in r 0) (+ pos-base pos))) + r) # unmatched closing delimiters (= c 41) @@ -726,6 +763,9 @@ (or (= c (chr " ")) (= c (chr "\t")) (= c (chr "\r")) (= c (chr ","))) (++ i) (= c (chr ";")) (while (and (< i n) (not= (in s i) (chr "\n"))) (++ i)) (set scanning false))) + # list-form positions recorded during this parse-next are relative to s; + # tell the reader the slice base so they land absolute (jolt-fqy) + (when track-positions (set-pos-base! (- (length source) (length s)))) (def [form rest*] (try (parse-next s) ([err fib] diff --git a/test/integration/type-check-test.janet b/test/integration/type-check-test.janet index 8c7e25f..28b5088 100644 --- a/test/integration/type-check-test.janet +++ b/test/integration/type-check-test.janet @@ -10,6 +10,7 @@ (print "Success-type checking (jolt-y3b)...") (os/setenv "JOLT_DIRECT_LINK" "1") +(reader/track-positions! true) # record form positions (jolt-fqy) (def ctx (api/init {:compile? true})) (def pns (types/ctx-find-ns ctx "jolt.passes")) (def check (types/var-get (types/ns-find pns "check-form"))) @@ -89,6 +90,11 @@ (def one (in (diags "(inc \"x\")") 0)) (assert (= "inc" (get one :op)) "diagnostic names the op") (assert (string/find "number" (get one :msg)) "message says a number is required") +# --- the diagnostic carries the offending form's source offset (jolt-fqy) ----- +(assert (= 0 (get one :pos)) "diagnostic carries :pos (offset 0 for a single form)") +(def nested (in (diags "(do 1 2 (inc :k))") 0)) +(assert (= 8 (get nested :pos)) + "the inner (inc :k) form is positioned at its own offset, not the do's") # --- end-to-end: strictness drives compilation (decoupled from :inline?) ----- # error mode aborts a provably-wrong form's compilation; a correct form compiles. From 37949ac6025bf4d46170df4461c16bf384c17570 Mon Sep 17 00:00:00 2001 From: Yogthos Date: Sat, 13 Jun 2026 12:26:56 -0400 Subject: [PATCH 15/20] fix: unary arithmetic type-error message no longer crashes the reporter MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit rewrite-message assumed janet's BINARY arithmetic dispatch error shape ("could not find method :+ for 1 or :r+ for "a""). Unary inc/dec/- on a non-number produce "could not find method :+ for "x"" — no "or :r" clause — so orpos was nil and the reporter itself threw "could not find method :+ for nil", burying the real error. Handle the unary form. Found auditing the RFC 0006 checker's default (checker-off) path. Regression row in cli-test. --- src/jolt/main.janet | 20 +++++++++++++------- test/integration/cli-test.janet | 6 ++++++ 2 files changed, 19 insertions(+), 7 deletions(-) diff --git a/src/jolt/main.janet b/src/jolt/main.janet index af7527c..602bdff 100644 --- a/src/jolt/main.janet +++ b/src/jolt/main.janet @@ -259,18 +259,24 @@ [msg] (def msg (string msg)) (cond - # janet polymorphic arithmetic: could not find method :+ for 1 or :r+ for "a" + # janet polymorphic arithmetic. Binary: "could not find method :+ for 1 or + # :r+ for "a"". Unary (inc/dec/-): "could not find method :+ for "x"" — no + # "or :r" clause, so orpos is nil; handle both without crashing the reporter. (string/has-prefix? "could not find method :" msg) (let [rest* (string/slice msg (length "could not find method :")) sp (string/find " " rest*) op (string/slice rest* 0 sp) tail (string/slice rest* (+ sp (length " for "))) - orpos (string/find " or :r" tail) - a (string/slice tail 0 orpos) - forpos (string/find " for " tail (+ orpos 1)) - b (string/slice tail (+ forpos 5))] - (string "Cannot " (get op-words op op) " " a " and " b - " — " op " expects numbers")) + orpos (string/find " or :r" tail)] + (if (nil? orpos) + # unary form: one operand + (string "Cannot " (get op-words op op) " " tail + " — " op " expects numbers") + (let [a (string/slice tail 0 orpos) + forpos (string/find " for " tail (+ orpos 1)) + b (string/slice tail (+ forpos 5))] + (string "Cannot " (get op-words op op) " " a " and " b + " — " op " expects numbers")))) # janet fixed-arity: called with 2 arguments, expected 1 (and (string/has-prefix? " called with " msg)) (let [nm-end (string/find ">" msg) diff --git a/test/integration/cli-test.janet b/test/integration/cli-test.janet index eef40aa..8b490f6 100644 --- a/test/integration/cli-test.janet +++ b/test/integration/cli-test.janet @@ -45,6 +45,12 @@ (check "arith error message rewritten" (run-err "-e" `(+ 1 "a")`) (has `Cannot add 1 and "a"`)) +# unary arithmetic (inc/dec) on a non-number: the host error has no "or :r" +# clause, which used to crash the rewriter itself — handle it (jolt audit) +(check "unary arith error does not crash the rewriter" + (run-err "-e" `(inc "x")`) + (fn [s] (and (string/find "expects numbers" s) + (nil? (string/find "could not find method" s))))) (check "arity error names the fn" (run-err "-e" "(defn afn [x] x) (afn 1 2)") (has "Wrong number of args (2) passed to: user/afn")) From 69af83da895e73b67a27ba4a7b032c1a8ec4633c Mon Sep 17 00:00:00 2001 From: Yogthos Date: Sat, 13 Jun 2026 13:02:17 -0400 Subject: [PATCH 16/20] refactor: fold success checking into the inference walk MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The checker ran a separate check-walk that re-inferred each argument's subtree AND recursed into it — quadratic in expression nesting. Fold the diagnostic emission into `infer` itself (gated by a checking? flag, off during the optimization fixpoint): one O(n) walk that both types and checks. Removes check-walk entirely; check-form now drives infer. This is a cleanup and removes the deep-nesting blowup, but it does NOT make warn-by-default cheap: on a real 360-line file the checker still adds ~2.6x compile time (277ms -> 720ms). That cost is the structural inference pass itself, which checking inherently requires — not redundancy. A cheap default-on path would need either piggybacking on the inference direct-link already runs, or a lighter scalar-only checker inference. Gate green, type-check tests pass. --- jolt-core/jolt/passes.clj | 96 ++++++++++++--------------------------- 1 file changed, 30 insertions(+), 66 deletions(-) diff --git a/jolt-core/jolt/passes.clj b/jolt-core/jolt/passes.clj index 4306599..dd21a17 100644 --- a/jolt-core/jolt/passes.clj +++ b/jolt-core/jolt/passes.clj @@ -848,11 +848,20 @@ (def ^:private user-sig-box (atom {})) ;; "ns/name" -> {:params [..] :body ir} (def ^:private checking-box (atom #{})) ;; keys mid-recheck — cycle guard (def ^:private strict-box (atom false)) ;; report against user-fn domains? +;; When true, `infer` emits success-type diagnostics as it types (jolt audit). +;; The checker IS the inference walk now — one O(n) pass that both types and +;; checks, instead of a separate check-walk that re-inferred every subtree +;; (quadratic in nesting). Off during the optimization fixpoint so it doesn't +;; emit intermediate diagnostics; on only inside check-form. +(def ^:private checking? (atom false)) ;; fns that RETURN an element of their (first) collection arg, so a lookup on the ;; result of (rand-nth coll-of-structs) etc. types as the element. (def ^:private elem-fns #{"rand-nth" "first" "peek" "last" "nth" "fnext" "second"}) +;; the checker's emission points, defined after infer but referenced from it +(declare check-invoke check-user-call register-user-fn!) + (defn- var-key [fnode] (str (get fnode :ns) "/" (get fnode :name))) (defn- call-ret-type [fnode] @@ -1039,6 +1048,15 @@ ares (mapv (fn [a] (infer a tenv)) args)] (when iscall-var (swap! calls-box conj [(var-key fnode) (mapv (fn [r] (nth r 0)) ares)])) + ;; success-type check at this call, reusing the arg types just + ;; computed (jolt audit): core error domains always, user-fn domains + ;; in strict mode. The arg subtrees are inferred exactly once. + (when @checking? + (let [ats (mapv (fn [r] (nth r 0)) ares) pos (get node :pos)] + (when cn (check-invoke cn args ats pos)) + (when (and @strict-box iscall-var) + (let [k (var-key fnode) usig (get @user-sig-box k)] + (when usig (check-user-call k usig ats pos)))))) [(cond (= cn "range") (mk-vec :num) ;; element-returning fn over a typed vector -> the element type @@ -1074,7 +1092,8 @@ (assoc a :body (nth (infer (get a :body) pe) 1)))) (get node :arities)))] (= op :def) - [:any (assoc node :init (nth (infer (get node :init) tenv) 1))] + (do (when @checking? (register-user-fn! node)) + [:any (assoc node :init (nth (infer (get node :init) tenv) 1))]) (= op :try) [:any (assoc node :body (nth (infer (get node :body) tenv) 1) @@ -1157,8 +1176,6 @@ ", but argument 1 is " (type-name t))}))) :else nil)) -(declare check-walk) - ;; --- user-function error domains (jolt-zo1), opt-in -------------------------- (defn- all-any-env "tenv binding every param name to :any (the all-ambiguous baseline)." @@ -1166,12 +1183,13 @@ (reduce (fn [e p] (assoc e p :any)) {} params)) (defn- isolated-diag-count - "Count of diagnostics check-walk produces for body under tenv, with the shared - diag-box saved and restored so this probe never leaks into the real report." + "Count of diagnostics typing body under tenv produces, with the shared + diag-box saved and restored so this probe never leaks into the real report. + Runs the same checking inference as check-form (checking? is already on)." [body tenv] (let [saved @diag-box] (reset! diag-box []) - (check-walk body tenv) + (infer body tenv) (let [n (count @diag-box)] (reset! diag-box saved) n))) @@ -1226,65 +1244,6 @@ nil (range np))) (reset! checking-box prev)))) -(defn- check-walk - "Walk the IR, inferring argument types and recording diagnostics for - provably-wrong core-fn calls. Threads tenv through binders exactly like infer." - [node tenv] - (let [op (get node :op)] - (cond - (= op :invoke) - (let [fnode (get node :fn) - args (get node :args) - cn (when (and (= :var (get fnode :op)) (= "clojure.core" (get fnode :ns))) - (get fnode :name)) - ukey (when (= :var (get fnode :op)) - (str (get fnode :ns) "/" (get fnode :name))) - usig (when (and @strict-box ukey) (get @user-sig-box ukey))] - (when (or cn usig) - (let [ats (mapv (fn [a] (nth (infer a tenv) 0)) args) - pos (get node :pos)] - (when cn (check-invoke cn args ats pos)) - (when usig (check-user-call ukey usig ats pos)))) - (check-walk fnode tenv) - (reduce (fn [_ a] (check-walk a tenv) nil) nil args)) - (= op :let) - (let [te (reduce (fn [e b] - (check-walk (nth b 1) e) - (assoc e (nth b 0) (nth (infer (nth b 1) e) 0))) - tenv (get node :bindings))] - (check-walk (get node :body) te)) - (= op :if) - (do (check-walk (get node :test) tenv) - (check-walk (get node :then) tenv) - (check-walk (get node :else) tenv)) - (= op :do) - (do (reduce (fn [_ s] (check-walk s tenv) nil) nil (get node :statements)) - (check-walk (get node :ret) tenv)) - (= op :fn) - (reduce (fn [_ a] - (let [pe (reduce (fn [e p] (assoc e p :any)) tenv (get a :params)) - pe (if (get a :rest) (assoc pe (get a :rest) :any) pe)] - (check-walk (get a :body) pe)) - nil) - nil (get node :arities)) - (= op :loop) - (do (reduce (fn [_ b] (check-walk (nth b 1) tenv) nil) nil (get node :bindings)) - (check-walk (get node :body) tenv)) - (= op :recur) - (reduce (fn [_ a] (check-walk a tenv) nil) nil (get node :args)) - (= op :def) (do (register-user-fn! node) (check-walk (get node :init) tenv)) - (= op :throw) (check-walk (get node :expr) tenv) - (= op :vector) (reduce (fn [_ x] (check-walk x tenv) nil) nil (get node :items)) - (= op :set) (reduce (fn [_ x] (check-walk x tenv) nil) nil (get node :items)) - (= op :map) - (reduce (fn [_ pr] (check-walk (nth pr 0) tenv) (check-walk (nth pr 1) tenv) nil) - nil (get node :pairs)) - (= op :try) - (do (check-walk (get node :body) tenv) - (when (get node :catch-body) (check-walk (get node :catch-body) tenv)) - (when (get node :finally) (check-walk (get node :finally) tenv))) - :else nil))) - ;; --- Inter-procedural driver API (jolt-767) consumed by the back end -------- (defn set-rtenv! "Install the current return-type estimates (a map \"ns/name\" -> type) used to @@ -1319,7 +1278,12 @@ (reset! strict-box (if strict? true false)) (reset! checking-box #{}) (reset! diag-box []) - (check-walk node {}) + ;; the check IS the inference: one walk that types and emits diagnostics + ;; (jolt audit). checking? gates emission so the optimization fixpoint, which + ;; also calls infer, stays silent. + (reset! checking? true) + (infer node {}) + (reset! checking? false) (reset! strict-box false) (vec @diag-box))) From 088232b7780719ef7705cf6ab043ae8756a34f59 Mon Sep 17 00:00:00 2001 From: Yogthos Date: Sat, 13 Jun 2026 13:46:16 -0400 Subject: [PATCH 17/20] feat: success checker on by default in direct-link builds, free (jolt audit) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Checking inherently needs an inference pass (~2.6x compile as a standalone pass). But direct-link builds ALREADY run one inference pass for specialization (run-passes' infer-top), so checking can ride along: set a check-mode flag, turn checking? on during that existing pass, and collect the diagnostics after — ~2% overhead measured on the ray tracer, vs 2.6x for the separate pass. So the checker now defaults to `warn` in direct-link builds (where it's nearly free) and stays OFF in plain REPL/dev builds (no inference to ride, no forced cost — opt in with JOLT_TYPE_CHECK there). JOLT_TYPE_CHECK still overrides in both directions (off to disable, error to escalate). It checks the POST-optimization IR, which matches what the optimized program actually evaluates — scalar-replace only drops provably-pure code, an accepted opt-mode divergence, so no real error is hidden. The loaders enable position tracking whenever checking will run (env-selected or direct-link). type-check! (the standalone pass) stays for plain builds; both paths share report-diags!. cli-test pins: plain build silent, direct-link warns by default, JOLT_TYPE_CHECK=off disables. Gate green, suite 4718, runtime bench even. --- jolt-core/jolt/passes.clj | 27 ++++++++++- src/jolt/api.janet | 6 ++- src/jolt/backend.janet | 84 +++++++++++++++++++++------------ src/jolt/evaluator.janet | 2 +- src/jolt/loader.janet | 2 +- test/integration/cli-test.janet | 25 ++++++++++ 6 files changed, 111 insertions(+), 35 deletions(-) diff --git a/jolt-core/jolt/passes.clj b/jolt-core/jolt/passes.clj index dd21a17..7b69114 100644 --- a/jolt-core/jolt/passes.clj +++ b/jolt-core/jolt/passes.clj @@ -1311,6 +1311,21 @@ (get fnode :arities)))) def-node))) +;; Piggyback checking (jolt audit). In direct-link mode infer-top already runs +;; one inference pass for specialization; turning checking? on during it makes +;; the success checker nearly free there (no extra traversal — just the +;; per-call error-domain predicates). The back end sets the mode before +;; run-passes and reads take-diags! after. It checks the POST-optimization IR, +;; which matches what the optimized program actually evaluates (scalar-replace +;; only drops provably-pure code, an accepted opt-mode divergence). +(def ^:private check-mode-box (atom {:on false :strict false})) +(defn set-check-mode! + "Enable/disable checking during the next run-passes inference (direct-link)." + [on strict?] (reset! check-mode-box {:on (if on true false) :strict (if strict? true false)})) +(defn take-diags! + "Diagnostics accumulated by the last checking run-passes; clears the buffer." + [] (let [d (vec @diag-box)] (reset! diag-box []) d)) + (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), @@ -1327,5 +1342,15 @@ (if (and @dirty (< i 8)) (recur (inc i) n2) n2)))] - (infer-top opt)) + ;; specialization inference, optionally also emitting success diagnostics + (if (get @check-mode-box :on) + (do (reset! diag-box []) + (reset! checking-box #{}) + (reset! strict-box (get @check-mode-box :strict)) + (reset! checking? true) + (let [r (infer-top opt)] + (reset! checking? false) + (reset! strict-box false) + r)) + (infer-top opt))) (const-fold node))) diff --git a/src/jolt/api.janet b/src/jolt/api.janet index c657829..e935f3a 100644 --- a/src/jolt/api.janet +++ b/src/jolt/api.janet @@ -369,8 +369,10 @@ Returns the result of the last form evaluated." [ctx s &opt file] (default file "") - # record form positions so the checker can report file:line:col (jolt-fqy) - (when (checker-enabled?) + # record form positions so the checker can report file:line:col (jolt-fqy). + # The checker is on when JOLT_TYPE_CHECK selects it, OR by default in + # direct-link builds (where it piggybacks on inference for free). + (when (or (checker-enabled?) (get (ctx :env) :inline?)) (track-positions! true) (put (ctx :env) :tc-source s) (put (ctx :env) :tc-file file)) diff --git a/src/jolt/backend.janet b/src/jolt/backend.janet index 5181eb5..91de6d8 100644 --- a/src/jolt/backend.janet +++ b/src/jolt/backend.janet @@ -613,13 +613,32 @@ [ctx] (build-compiler! ctx)) -(defn type-check! - "Success-type check the analyzed IR (RFC 0006). Looks up jolt.passes/check-form - (absent during pre-passes bootstrap -> no-op), runs it protected so a checker - bug never breaks compilation, then reports each diagnostic per strictness: +(defn- report-diags! + "Render and emit success-type diagnostics (RFC 0006) at the given strictness: `warn` prints to stderr, `error` throws (failing this form's compilation). - Because the checker only fires on PROVABLY-wrong code, a correct program has - nothing to report under either level. + file:line:col when the diagnostic carries an offset and the source is on the + env (jolt-fqy); else the ns." + [ctx diags strictness ns] + (def src (get (ctx :env) :tc-source)) + (def file (or (get (ctx :env) :tc-file) (and ns (string ns)))) + (each d diags + (def off (get d :pos)) + (def loc + (if (and off src) + (let [lc (r/line-col src off)] + (string (or file "?") ":" (in lc 0) ":" (in lc 1))) + (string "in " (if ns (string ns) "?")))) + (def msg (string "type error " loc ": " (get d :msg))) + (if (= strictness "error") + (error msg) + (eprint " " msg)))) + +(defn type-check! + "Decoupled success-type check (RFC 0006): run jolt.passes/check-form as its OWN + inference pass over `ir` and report. Used in NON-direct-link builds, where the + optimization inference doesn't run — so checking costs a separate pass. (In + direct-link builds checking piggybacks on run-passes' inference instead, near + free; see analyze-form.) Protected so a checker bug never breaks compilation. JOLT_TYPE_CHECK_USER (an orthogonal opt-in knob, jolt-zo1) additionally reports calls to user functions whose concrete argument types provably make @@ -633,23 +652,7 @@ (when (r 0) (def diags (if (pv/pvec? (r 1)) (pv/pv->array (r 1)) (r 1))) (when (and diags (> (length diags) 0)) - # source + file for offset -> line:col (jolt-fqy). The loader stashes the - # current file's source + path on the env when checking is on. - (def src (get (ctx :env) :tc-source)) - (def file (or (get (ctx :env) :tc-file) (and ns (string ns)))) - (each d diags - (def off (get d :pos)) - # precise: file:line:col of the offending form when its offset and the - # source are both available; else the ns (no worse than before) - (def loc - (if (and off src) - (let [lc (r/line-col src off)] - (string (or file "?") ":" (in lc 0) ":" (in lc 1))) - (string "in " (if ns (string ns) "?")))) - (def msg (string "type error " loc ": " (get d :msg))) - (if (= strictness "error") - (error msg) - (eprint " " msg))))))) + (report-diags! ctx diags strictness ns))))) (defn analyze-form "Run the portable Clojure analyzer (jolt.analyzer/analyze) on a reader form, @@ -683,6 +686,21 @@ # Resolved lazily; absent during the pre-passes bootstrap window. (def pv (unless (= "1" (os/getenv "JOLT_NO_IR_PASSES")) (ns-find (ctx-find-ns ctx "jolt.passes") "run-passes"))) + # Success-type checking level (RFC 0006). JOLT_TYPE_CHECK wins when set; + # otherwise it defaults to `warn` in direct-link builds — where the + # optimization inference already runs, so checking piggybacks on it for nearly + # free — and stays OFF for plain REPL/dev builds (no inference -> no free ride; + # opt in with JOLT_TYPE_CHECK there). (jolt audit) + (def tc (os/getenv "JOLT_TYPE_CHECK")) + (def tc-off (or (= tc "off") (= tc "0"))) + (def direct-link? (if (get (ctx :env) :inline?) true false)) + (def level (cond tc-off nil tc tc direct-link? "warn" true nil)) + (def uenv (os/getenv "JOLT_TYPE_CHECK_USER")) + (def strict? (and uenv (not= uenv "0") (not= uenv "off") true)) + # piggyback: check DURING run-passes' inference (direct-link, the cheap path) + (def piggyback? (and level direct-link? pv true)) + (def scm (and piggyback? (ns-find (ctx-find-ns ctx "jolt.passes") "set-check-mode!"))) + (when scm ((var-get scm) true strict?)) (def result (if pv (let [pr (protect ((var-get pv) (r 1) ctx))] @@ -692,13 +710,19 @@ (ctx-set-current-ns ctx saved-ns) (if (pr 0) (pr 1) (r 1))) (r 1))) - # Success-type check (RFC 0006), decoupled from specialization: runs whenever - # JOLT_TYPE_CHECK is warn/error, regardless of :inline?. Read at runtime so it - # needs no rebuild. The analyzed IR (r 1) carries no specialization; the - # checker does its own inference. - (def tc (os/getenv "JOLT_TYPE_CHECK")) - (when (and tc (not= tc "off") (not= tc "0")) - (type-check! ctx (r 1) tc saved-ns)) + (when scm ((var-get scm) false false)) + (cond + # direct-link: collect the diagnostics infer-top emitted and report them + piggyback? + (let [td (ns-find (ctx-find-ns ctx "jolt.passes") "take-diags!")] + (when td + (def raw ((var-get td))) + (def diags (if (pv/pvec? raw) (pv/pv->array raw) raw)) + (when (and diags (> (length diags) 0)) + (report-diags! ctx diags level saved-ns)))) + # plain build with checking explicitly requested: a separate inference pass + (and level (not direct-link?)) + (type-check! ctx (r 1) level saved-ns)) result) # The analyzer's deliberate punt signal — (uncompilable why) throws the string diff --git a/src/jolt/evaluator.janet b/src/jolt/evaluator.janet index 72cc465..ff68c25 100644 --- a/src/jolt/evaluator.janet +++ b/src/jolt/evaluator.janet @@ -377,7 +377,7 @@ (def toplevel (get (ctx :env) :toplevel-eval)) # a require runs nested inside an outer file's eval; save/restore the outer # checker source so its later forms still convert offsets correctly (jolt-fqy) - (def checking (checker-enabled?)) + (def checking (or (checker-enabled?) (get (ctx :env) :inline?))) (def saved-src (and checking (get (ctx :env) :tc-source))) (def saved-file (and checking (get (ctx :env) :tc-file))) (when checking diff --git a/src/jolt/loader.janet b/src/jolt/loader.janet index d7e2028..7c82476 100644 --- a/src/jolt/loader.janet +++ b/src/jolt/loader.janet @@ -112,7 +112,7 @@ (load-ns ctx filepath) → namespace symbol string" [ctx filepath] (def source (slurp filepath)) - (when (checker-enabled?) + (when (or (checker-enabled?) (get (ctx :env) :inline?)) (track-positions! true) (put (ctx :env) :tc-source source) (put (ctx :env) :tc-file filepath)) diff --git a/test/integration/cli-test.janet b/test/integration/cli-test.janet index 8b490f6..d45e96d 100644 --- a/test/integration/cli-test.janet +++ b/test/integration/cli-test.janet @@ -118,6 +118,31 @@ r) (has "could not find method")) +# --- success checker default-on in direct-link, off in plain builds ---------- +# A provably-wrong defn (never called, so no runtime error): the checker is the +# only thing that can flag it. Plain build = silent (no dev regression); +# direct-link build = warns by default (free piggyback on inference). +(def tcw (string (or (os/getenv "TMPDIR") "/tmp") "/jolt-tcwarn-" (os/time) ".clj")) +(spit tcw "(ns tcw)\n\n(defn unused [s]\n (inc \"definitely-not-a-number\"))\n") +(check "plain build does not run the checker (no regression)" + (run-err tcw) + (fn [s] (nil? (string/find "type error" s)))) +(check "direct-link build warns by default (free checking)" + (do (os/setenv "JOLT_DIRECT_LINK" "1") + (def r (run-err tcw)) + (os/setenv "JOLT_DIRECT_LINK" nil) + r) + (fn [s] (and (string/find "type error" s) + (string/find "requires a number" s)))) +(check "JOLT_TYPE_CHECK=off disables it even in direct-link" + (do (os/setenv "JOLT_DIRECT_LINK" "1") + (os/setenv "JOLT_TYPE_CHECK" "off") + (def r (run-err tcw)) + (os/setenv "JOLT_DIRECT_LINK" nil) + (os/setenv "JOLT_TYPE_CHECK" nil) + r) + (fn [s] (nil? (string/find "type error" s)))) + (if (> fails 0) (error (string "cli-test: " fails " failing check(s)")) (print "\nAll CLI tests passed!")) From e071d09170793a2278877839b832028134845e6a Mon Sep 17 00:00:00 2001 From: Yogthos Date: Sat, 13 Jun 2026 13:47:36 -0400 Subject: [PATCH 18/20] =?UTF-8?q?docs:=20RFC=200006=20=E2=80=94=20mark=20u?= =?UTF-8?q?nions/user-fns/positions/default-on=20resolved?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Update the status, strictness levels, and open questions to reflect what landed: bounded unions (jolt-pz5), user-fn domains behind JOLT_TYPE_CHECK_USER (jolt-zo1), precise file:line:col (jolt-fqy), and the checker folded into one inference walk that piggybacks on direct-link specialization (on by default there, opt-in in plain builds). Align the error-reporting example with the actual output format. --- docs/rfc/0006-success-type-checking.md | 78 +++++++++++++++----------- 1 file changed, 45 insertions(+), 33 deletions(-) diff --git a/docs/rfc/0006-success-type-checking.md b/docs/rfc/0006-success-type-checking.md index ee6442d..73adad6 100644 --- a/docs/rfc/0006-success-type-checking.md +++ b/docs/rfc/0006-success-type-checking.md @@ -1,9 +1,14 @@ # RFC 0006 — Compile-time detection of provably-wrong code (success typing) -- **Status**: Implemented (jolt-y3b), first table. Core-fn error domains - (arithmetic on non-numbers, count/first/rest/next/seq/nth on non-seqable - scalars), `JOLT_TYPE_CHECK=off|warn|error`, decoupled from specialization. - Precise source locations (file:line:col) remain follow-up work. +- **Status**: Implemented. Core-fn error domains (arithmetic on non-numbers, + count/first/rest/next/seq/nth on non-seqable scalars), `JOLT_TYPE_CHECK= + off|warn|error`. Follow-ups landed: bounded scalar **unions** (jolt-pz5) so a + use is reported only when every member is in the error domain; **user-fn + error domains** behind `JOLT_TYPE_CHECK_USER` (jolt-zo1, closed-world); + precise **file:line:col** locations (jolt-fqy). The checker is now one + inference walk (folded into `infer`), and is **on by default in direct-link + builds** — where it piggybacks on the specialization inference for ~free — + and opt-in (`JOLT_TYPE_CHECK`) in plain builds. - **Champions**: jolt maintainers - **Created**: 2026-06-13 - **Depends on**: RFC 0005 (structural collection-type inference) @@ -112,8 +117,7 @@ A reported error includes: Example: ``` -type error at scene.clj:42:18 - (inc total) — `inc` requires a number, but `total` is a string +type error scene.clj:42:18: `inc` requires a number, but argument 1 is a string ``` Errors are attributed to the form the user wrote. For macro-expanded code, the @@ -122,14 +126,20 @@ tracks `:error-pos`), never at synthesized internals. ## Strictness levels -A single env/compile flag controls behavior, defaulting to non-breaking: +`JOLT_TYPE_CHECK` controls behavior: -- **off** — no checking (default for now). -- **warn** — report to stderr, do not fail compilation. The recommended rollout - default once the table is trusted. +- **off** — no checking. +- **warn** — report to stderr, do not fail compilation. **The default in + direct-link builds**, where checking rides the specialization inference for + ~free; opt-in elsewhere. - **error** — fail compilation on a provable type error. Opt-in for CI / strict builds. +When `JOLT_TYPE_CHECK` is unset, checking is **on (`warn`) in direct-link +builds** and **off in plain REPL/dev builds** (where it would cost a standalone +inference pass, ~2.6× compile). `JOLT_TYPE_CHECK_USER` additionally enables +reporting against inferred user-function domains (closed-world; see below). + Because the checker only fires on provable errors, even `error` mode cannot break a correct program: a correct program has no provable type errors to report. (A correct-but-untypeable program is simply not reported, since its @@ -193,26 +203,28 @@ smallest high-confidence table (arithmetic and seq/count/nth/first), and grow. destroys trust. Mitigation: start tiny, test each entry against the runtime, grow slowly. Open question: derive the table from the same machinery the runtime uses, to avoid drift? -- **Unions.** Today the inference joins to `:any` rather than forming unions - (`{:num | :str}`). Precise success typing wants unions (report only when - *every* member is in the error domain). Open question: add a small bounded - union type to RFC 0005's lattice, or keep `:any` and lose some precision (more - conservative, fewer reports, still no false positives)? Proposed: start with - `:any` (conservative), add unions if too many real errors are missed. -- **User-function signatures.** Reporting against inferred user-fn domains is - more powerful but rests on the closed-world assumption and on the inferred - signature being a true requirement. Proposed: core fns first; user fns behind - an explicit opt-in. -- **Negative/never types.** Some "provably wrong" cases are about a value being - the wrong arity or a fn vs a non-fn (calling a non-function). Worth including - the clear ones (calling a `:num` as a function) since the inference already - knows function-ness. -- **Position vs intent.** Reporting at the right source location through - inlining and macro expansion needs the position metadata to survive the - passes. The loader tracks `:error-pos`; the IR may need to carry form - positions for precise column reporting. -- **Interaction with the optimization gate.** The inference currently runs only - in optimization mode. The checker is valuable in normal builds too, so the - inference (at least its intra-procedural, sound-without-closed-world part) - may need to run for checking even when specialization is off. Open question: - decouple "run inference for checking" from "specialize from inference". +- **Unions.** *Resolved (jolt-pz5).* The lattice has a bounded scalar union + `{:union #{T...}}` (cap 4); differing if-branches form a union instead of + collapsing to `:any`, and a use is reported only when *every* member is in the + error domain. Unions are opaque to structural specialization, so codegen is + unchanged. +- **User-function signatures.** *Resolved (jolt-zo1), opt-in.* Behind + `JOLT_TYPE_CHECK_USER`: the checker re-checks a registered non-redefinable + user fn's body with one parameter bound to its concrete argument type; a + diagnostic the all-`:any` body did not have means that argument is provably + wrong. Monotonic, so still no false positives; closed-world, hence opt-in. +- **Negative/never types.** Still open. Some "provably wrong" cases are wrong + arity or a non-fn called as a fn; worth including the clear ones (calling a + `:num`) since the inference knows function-ness. +- **Position vs intent.** *Resolved (jolt-fqy).* The reader records each list + form's absolute offset (identity-keyed, so positions survive macroexpansion + exactly when the user's sub-form is spliced through); the analyzer stamps it + onto `:invoke` nodes, the checker carries it into each diagnostic, and the + back end renders `file:line:col`. Inlining/scalar-replace preserve it via + `assoc`. +- **Interaction with the optimization gate.** *Resolved (jolt audit).* The + checker is one inference walk folded into `infer`. In direct-link builds it + piggybacks on the specialization inference that already runs (~free, default + on); in plain builds it runs as a standalone pass only when `JOLT_TYPE_CHECK` + is set. "Run inference for checking" and "specialize from inference" are the + same walk now, gated by a `checking?` flag. From 328f88636e43756dca89e0e28ddec4fea5fa80a3 Mon Sep 17 00:00:00 2001 From: Yogthos Date: Sat, 13 Jun 2026 14:48:14 -0400 Subject: [PATCH 19/20] =?UTF-8?q?feat:=20negative/never=20types=20?= =?UTF-8?q?=E2=80=94=20calling=20a=20non-function,=20wrong-arity=20(jolt-w?= =?UTF-8?q?wy)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two provably-wrong cases the inference already has the facts for, closing the last RFC 0006 open question: - Calling a non-function. At an :invoke whose callee is provably :num or :str (the only non-callable types — keywords/maps/vectors/sets are IFn), report "cannot call a number as a function". Default level (no closed-world: the callee type is inferred at the call site). Covers (5 1), ("hi" 0), ((+ 1 2) :k), a let-bound number, and a var holding a number (via vtype-box in direct-link). A union is non-callable only when every member is, so ((if c 1 :k) x) is accepted (:kw is callable). Verified zero false positives on the ray tracer, which calls maps/keywords/vectors as fns throughout. - Wrong arity to a user fn. The registered single-fixed-arity sig (jolt-zo1) makes a mismatched arg count provably throw; reported under the JOLT_TYPE_CHECK_USER opt-in (same closed-world boundary; ^:redef/variadic skipped). Caught at compile time before the runtime arity error. Both fold into the existing infer walk, carry :pos for file:line:col, and keep no-false-positives. Gate green, suite 4718, conformance 335/335, runtime bench even (compile-time only). --- jolt-core/jolt/passes.clj | 74 ++++++++++++++++++-------- test/integration/cli-test.janet | 20 +++++++ test/integration/type-check-test.janet | 29 ++++++++++ 3 files changed, 100 insertions(+), 23 deletions(-) diff --git a/jolt-core/jolt/passes.clj b/jolt-core/jolt/passes.clj index 7b69114..fc6199b 100644 --- a/jolt-core/jolt/passes.clj +++ b/jolt-core/jolt/passes.clj @@ -860,7 +860,7 @@ (def ^:private elem-fns #{"rand-nth" "first" "peek" "last" "nth" "fnext" "second"}) ;; the checker's emission points, defined after infer but referenced from it -(declare check-invoke check-user-call register-user-fn!) +(declare check-invoke check-user-call register-user-fn! not-callable? type-name) (defn- var-key [fnode] (str (get fnode :ns) "/" (get fnode :name))) @@ -1044,7 +1044,12 @@ ;; everything else: type args, collect the call (var callee), use the ;; declared/estimated return type. range produces a numeric vector. :else - (let [fnode' (if iscall-var fnode (nth (infer fnode tenv) 1)) + (let [fr (when (not iscall-var) (infer fnode tenv)) + fnode' (if iscall-var fnode (nth fr 1)) + ;; the callee's value type: a var's from vtype-box (a fn is + ;; :truthy, a def carries its inferred type), else the inferred + ;; type of the callee expression (jolt-wwy) + callee-t (if iscall-var (get @vtype-box (var-key fnode)) (nth fr 0)) ares (mapv (fn [a] (infer a tenv)) args)] (when iscall-var (swap! calls-box conj [(var-key fnode) (mapv (fn [r] (nth r 0)) ares)])) @@ -1054,6 +1059,11 @@ (when @checking? (let [ats (mapv (fn [r] (nth r 0)) ares) pos (get node :pos)] (when cn (check-invoke cn args ats pos)) + ;; calling a provably non-function (jolt-wwy) + (when (not-callable? callee-t) + (swap! diag-box conj + {:op :call :type (type-name callee-t) :pos pos + :msg (str "cannot call " (type-name callee-t) " as a function")})) (when (and @strict-box iscall-var) (let [k (var-key fnode) usig (get @user-sig-box k)] (when usig (check-user-call k usig ats pos)))))) @@ -1128,6 +1138,15 @@ (every? not-seqable? (umembers t)) (or (= t :num) (= t :kw)))) +;; concrete non-callable values (jolt-wwy): calling them throws "Cannot call X +;; as a function". Only :num and :str — keywords/maps/vectors/sets are IFn, +;; :truthy/:any/:nil are ambiguous (accepted). A union is non-callable only when +;; every member is. +(defn- not-callable? [t] + (if (union-type? t) + (every? not-callable? (umembers t)) + (or (= t :num) (= t :str)))) + ;; arithmetic / numeric ops: EVERY argument must be a number. (def ^:private num-ops #{"+" "-" "*" "/" "inc" "dec" "mod" "rem" "quot" "min" "max" "abs" @@ -1213,11 +1232,13 @@ :params (get ar :params) :body (get ar :body)})))))))) (defn- check-user-call - "Strict mode: report a call whose concrete argument type provably makes the - callee body throw. For each concrete arg, re-check the body with ONLY that - parameter bound to its arg type (others :any); a diagnostic the all-:any body - did not already have means the argument alone is provably wrong. Monotonic — - binding a concrete type can only ADD error-domain hits — so no false positive. + "Strict mode: report a call to a registered user fn that provably throws — + either a WRONG ARITY (the registered fn has one fixed arity, so a different + arg count always throws, jolt-wwy) or an argument whose concrete type the body + rejects. For the latter, re-check the body with ONLY that parameter bound to + its arg type (others :any); a diagnostic the all-:any body did not already + have means the argument alone is provably wrong. Monotonic — binding a + concrete type can only ADD error-domain hits — so no false positive. Cycle-guarded so mutually recursive fns terminate." [key sig arg-types pos] (when (not (contains? @checking-box key)) @@ -1225,23 +1246,30 @@ (reset! checking-box (conj prev key)) (let [params (:params sig) body (:body sig) - base (isolated-diag-count body (all-any-env params)) npar (count params) - nargs (count arg-types) - np (if (< npar nargs) npar nargs)] - (reduce - (fn [_ i] - (let [at (nth arg-types i)] - (when (and (not= at :any) (not= at :truthy)) - (let [pe (assoc (all-any-env params) (nth params i) at)] - (when (> (isolated-diag-count body pe) base) - (swap! diag-box conj - {:op :user-call :argpos i :type (type-name at) :pos pos - :msg (str "argument " (inc i) " to `" (:name sig) - "` is " (type-name at) - ", which its body provably rejects")}))))) - nil) - nil (range np))) + nargs (count arg-types)] + (if (not= npar nargs) + ;; arity is provably wrong regardless of types — report and stop (the + ;; per-arg type re-check would bind params positionally, meaningless + ;; under a mismatch) + (swap! diag-box conj + {:op :user-call :type :arity :pos pos + :msg (str "wrong number of args (" nargs ") passed to `" + (:name sig) "` (expected " npar ")")}) + (let [base (isolated-diag-count body (all-any-env params))] + (reduce + (fn [_ i] + (let [at (nth arg-types i)] + (when (and (not= at :any) (not= at :truthy)) + (let [pe (assoc (all-any-env params) (nth params i) at)] + (when (> (isolated-diag-count body pe) base) + (swap! diag-box conj + {:op :user-call :argpos i :type (type-name at) :pos pos + :msg (str "argument " (inc i) " to `" (:name sig) + "` is " (type-name at) + ", which its body provably rejects")}))))) + nil) + nil (range npar))))) (reset! checking-box prev)))) ;; --- Inter-procedural driver API (jolt-767) consumed by the back end -------- diff --git a/test/integration/cli-test.janet b/test/integration/cli-test.janet index d45e96d..184d1b9 100644 --- a/test/integration/cli-test.janet +++ b/test/integration/cli-test.janet @@ -142,6 +142,26 @@ (os/setenv "JOLT_TYPE_CHECK" nil) r) (fn [s] (nil? (string/find "type error" s)))) +# negative/never types (jolt-wwy): calling a non-function is reported by default +# in direct-link; wrong-arity to a user fn under the JOLT_TYPE_CHECK_USER opt-in +(def tcn (string (or (os/getenv "TMPDIR") "/tmp") "/jolt-tcneg-" (os/time) ".clj")) +(spit tcn "(ns tcn)\n\n(defn nope []\n (let [n 5] (n 1)))\n") +(check "direct-link reports calling a number as a function" + (do (os/setenv "JOLT_DIRECT_LINK" "1") + (def r (run-err tcn)) + (os/setenv "JOLT_DIRECT_LINK" nil) + r) + (has "cannot call a number as a function")) +(def tca (string (or (os/getenv "TMPDIR") "/tmp") "/jolt-tcarity-" (os/time) ".clj")) +(spit tca "(ns tca)\n\n(defn f [x y] (+ x y))\n(defn g [] (f 1))\n") +(check "JOLT_TYPE_CHECK_USER reports wrong arity to a user fn" + (do (os/setenv "JOLT_DIRECT_LINK" "1") + (os/setenv "JOLT_TYPE_CHECK_USER" "1") + (def r (run-err tca)) + (os/setenv "JOLT_DIRECT_LINK" nil) + (os/setenv "JOLT_TYPE_CHECK_USER" nil) + r) + (has "wrong number of args (1) passed to `f` (expected 2)")) (if (> fails 0) (error (string "cli-test: " fails " failing check(s)")) diff --git a/test/integration/type-check-test.janet b/test/integration/type-check-test.janet index 28b5088..5580a24 100644 --- a/test/integration/type-check-test.janet +++ b/test/integration/type-check-test.janet @@ -45,6 +45,23 @@ (assert (= 0 (nd "(inc (count [1 2 3]))")) "count of vector + inc of :num both fine") (assert (= 0 (nd "(inc (first [1 2 3]))")) "first of vector -> :num, inc fine") +# --- calling a non-function (jolt-wwy): :num and :str are not callable -------- +(assert (= 1 (nd "(5 1)")) "calling a number is reported") +(assert (= 1 (nd "(\"hi\" 0)")) "calling a string is reported") +(assert (= 1 (nd "((+ 1 2) :k)")) "calling an arithmetic result (a :num) is reported") +(assert (= 1 (nd "(let [n 5] (n 1))")) "calling a let-bound number is reported") +(assert (= 1 (nd "(let [s \"x\"] (s 0))")) "calling a let-bound string is reported") +# (a var holding a number, e.g. (def nn 5) (nn 1), is caught in direct-link +# mode via vtype-box; the standalone checker has no var value types) +# callable values: keyword/map/vector/set as IFn — NOT reported +(assert (= 0 (nd "(:k {:k 1})")) "keyword call is fine") +(assert (= 0 (nd "({:a 1} :a)")) "map call is fine") +(assert (= 0 (nd "([10 20] 1)")) "vector call is fine") +(assert (= 0 (nd "(#{1 2} 1)")) "set call is fine") +(assert (= 0 (nd "(fn [c] ((if c 1 :k) 0))")) "union {:num | :kw} callee accepted (:kw is callable)") +(assert (= 0 (nd "(fn [f] (f 1))")) "calling an unknown (:any) param accepted") +(assert (= 1 (nd "(fn [c] ((if c 1 \"x\") 0))")) "union {:num | :str} callee — both non-callable — reported") + # --- bounded unions (jolt-pz5): report only when EVERY member is in the error # domain; accept when any member is valid. Differing branches used to collapse # to :any (accepted); now they form {:union #{...}} and are checked per-member. @@ -85,6 +102,18 @@ "strict: a ^:redef fn is not a stable requirement, not reported") (assert (= 1 (nds "(do (defn ufrec [x] (ufrec (+ x 1))) (ufrec \"s\"))")) "strict: self-recursion terminates (cycle guard) and the (+ x 1) on a string is reported once") +# wrong arity to a user fn (jolt-wwy), strict mode: the registered fixed arity +# makes a mismatched call provably throw, regardless of argument types +(assert (= 1 (nds "(do (defn uar [x y] (+ x y)) (uar 1))")) + "strict: 2-arg fn called with 1 arg is reported") +(assert (= 1 (nds "(do (defn uar2 [x] x) (uar2 1 2 3))")) + "strict: 1-arg fn called with 3 args is reported") +(assert (= 0 (nds "(do (defn uar3 [x y] (+ x y)) (uar3 1 2))")) + "strict: correct arity accepted") +(assert (= 0 (nd "(do (defn uar4 [x y] (+ x y)) (uar4 1))")) + "default level does NOT report user-fn arity (closed-world, opt-in)") +(assert (= 0 (nds "(do (defn ^:redef uar5 [x y] (+ x y)) (uar5 1))")) + "strict: ^:redef fn arity not checked (could be redefined)") # --- the diagnostic carries op + type + a message ---------------------------- (def one (in (diags "(inc \"x\")") 0)) From f9a1849ec8fff687b954c37b9b0f7ce18c4e131d Mon Sep 17 00:00:00 2001 From: Yogthos Date: Sat, 13 Jun 2026 14:48:39 -0400 Subject: [PATCH 20/20] =?UTF-8?q?docs:=20RFC=200006=20=E2=80=94=20mark=20n?= =?UTF-8?q?egative/never=20types=20resolved=20(jolt-wwy)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- docs/rfc/0006-success-type-checking.md | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/docs/rfc/0006-success-type-checking.md b/docs/rfc/0006-success-type-checking.md index 73adad6..fd6fbd8 100644 --- a/docs/rfc/0006-success-type-checking.md +++ b/docs/rfc/0006-success-type-checking.md @@ -213,9 +213,11 @@ smallest high-confidence table (arithmetic and seq/count/nth/first), and grow. user fn's body with one parameter bound to its concrete argument type; a diagnostic the all-`:any` body did not have means that argument is provably wrong. Monotonic, so still no false positives; closed-world, hence opt-in. -- **Negative/never types.** Still open. Some "provably wrong" cases are wrong - arity or a non-fn called as a fn; worth including the clear ones (calling a - `:num`) since the inference knows function-ness. +- **Negative/never types.** *Resolved (jolt-wwy).* Calling a provably + non-callable value (`:num`/`:str` — keywords/maps/vectors/sets are IFn) is + reported at the default level; wrong-arity to a registered single-fixed-arity + user fn is reported under the `JOLT_TYPE_CHECK_USER` opt-in. A union callee is + flagged only when every member is non-callable. - **Position vs intent.** *Resolved (jolt-fqy).* The reader records each list form's absolute offset (identity-keyed, so positions survive macroexpansion exactly when the user's sub-form is spliced through); the analyzer stamps it