From e7473f38cf77458e155b06c9bdea73dc3b8a7c0b Mon Sep 17 00:00:00 2001 From: Yogthos Date: Sat, 13 Jun 2026 10:17:21 -0400 Subject: [PATCH] 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".