RFC 0005: Structural Type Inference

RFC 0005 — Structural collection-type inference

  • Status: Implemented — hint-free inference reaches the same specialization as an explicit ^:struct annotation.
  • Champions: jolt maintainers

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 passes 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 existing inference 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 (a 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 host 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. 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 inter-procedural fixpoint, recompile, escape gate, and closed-world assumption 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.

Compilation modes and defaults

Direct-linking — and the inference and specialization it enables — is the default for running a program and stays off for interactive work, chosen by the CLI run mode rather than a global opt-in flag:

modelinkingwhole-program
-m / -M NS (program entry)direct (default)auto (closed world)
FILE / -f / stdin (-)direct (default)no (per-namespace)
repl, -e, nrepl-serverindirect / openno

A program run is a closed world — every namespace is required, then the code runs to completion — so it direct-links: user code gets inlining, record shapes, and the inference's specialization. A -m / -M entry is the exact point where all requires are done and -main is about to run, so the whole-program cross-namespace pass (below) runs there automatically. Interactive modes stay open: a REPL, -e, and the nREPL server must let you redefine vars — which direct-linking seals against — so they keep the indirect, live-deref path.

Env overrides, all winning over the mode default:

  • JOLT_NO_DIRECT_LINK=1 — force the open/indirect path even for a program run (runtime redefinition, hot-reload, self-modifying code).
  • JOLT_NO_WHOLE_PROGRAM=1 — keep direct-linking but skip the whole-program pass (per-namespace inference only).
  • JOLT_DIRECT_LINK=1 — force direct-linking on even in an interactive mode.
  • JOLT_WHOLE_PROGRAM=1 — force the whole-program pass on in any direct-linked mode.
  • JOLT_NO_SHAPE=1 — disable the record/shape representation under direct-linking.

What direct-linking gives up is what Clojure's :direct-linking and jank's -Odirect-call give up: a direct call embeds its callee, so redefining the callee is not seen by already-compiled callers. Whole-program additionally const-links stable vars (data defs, record types, ^:redef), extending the same trade. That is why the interactive modes stay open and the opt-outs exist.

Cross-namespace inference

Per-namespace inference (a FILE run, or any namespace under JOLT_NO_WHOLE_PROGRAM) types a function's parameters from the call sites it can see within that namespace. A function whose record parameter is supplied by a caller in another namespace is left :any, its field reads keep the guard, and the values derived from it widen — so a decomposed program is markedly slower than the same code in one namespace (measured at ~3.7× on the ray tracer split across five namespaces). The information exists in the program; per-namespace compilation just can't see a caller in a not-yet-loaded namespace. Two ways to supply it:

  1. Whole-program (auto for -m / -M) runs one closed-world inference fixpoint over every loaded namespace before -main, typing each parameter from its call sites wherever they live. Namespaces required later (inside -main) fall back to per-namespace inference.
  2. Parameter type hints (^RecordType, RFC 0004) declare the type directly, so it also works in the open world — REPL, library code that must be fast for any caller, and hot-reloading servers — where the world cannot be closed.

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 inter-procedural 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 the inter-procedural pass: param/return inference assumes the compiled unit is the whole program. Documented there; unchanged.