#Inference — kinds, presentation, and the error policy

Kinds gives the relation: which kinds exist and which judgments hold. This page gives the algorithm: how a kind is actually assigned to every node of a program, how the presentation of a chart — pane, scale, guides, colour, parameter UI — is derived from those kinds rather than configured, and what happens when something does not type.

Three properties make the algorithm worth specifying precisely, rather than leaving it as an implementation detail. It is principal (the kind it synthesizes is the least one the program admits, so there is never a choice to make), it is deterministic (the same source always yields the same kinds, which is what lets two engines emit byte-identical code), and it is total (every editing state, including a half-typed line, gets a kind or a precise error — never a silent failure).

New here? Start with Guide §5 — Kinds: types that carry meaning → for the teaching version, then return here for the algorithm.

#Two modes

Inference is bidirectional: it reads the same typing rules in two directions.

Synthesis — Γ ⊢ e ⇒ κ — is the default, bottom-up mode. It produces the smallest kind the expression admits. Leaves synthesize their exact kind (close ⇒ price, 14 ⇒ lit, "hi" ⇒ string); introductions synthesize their structure (a record literal, a scene, a constructor); eliminations synthesize by computing — a call, a projection, a match, a delay, a resample, and every arithmetic node, which asks the dimensional algebra for its result kind.

Checking — Γ ⊢ e ⇐ κ — is the top-down mode, and it runs only at sites of consumption, where an expected kind already exists:

That last row is also what disambiguates the arrow: (x) -> x * 1.1 is a lambda exactly when its position expects a function, and a tween pair otherwise. Disambiguation is a consequence of the mode, not a separate rule (see Grammar).

#Subsumption is confined

The coercion rule — “an a may be used where a b is expected if a ≤ b” — fires only at the boundary between the two modes. To check e ⇐ κ: synthesize e ⇒ κ', then demand κ' ≤ κ. Silent if the edge is ≤safe; a warning with a quick-fix if it is ≤lossy; [ErrDim], [ErrArg] or [ErrPlot] — according to the position — if κ' ⊀ κ.

Coercion never fires during synthesis. A node is never spontaneously widened; its synthesized kind stays the lowest one known.

Why confinement is load-bearing. Suppose subsumption were allowed in synthesis. Then x = close - close could synthesize level or, by the lossy erasure edge, quantity. Both are derivable. But plot x reads the presentation registry at the kind: level gives a pane centred on zero, quantity gives a fallback auto pane. One program, two valid outputs, two different compiled artifacts — and the guarantee that the editor’s preview matches the shipped module (I7) would be gone. Confinement is what makes “the kind of an expression” a function rather than a choice.

#Principality

With synthesis defined as above, every expression has a principal kind: the unique smallest kind it admits. The proof is a one-line induction — each leaf synthesizes exactly, each node combines its children’s minimal kinds with either ⊔ or the dimensional algebra (both of which return a unique result, verified by enumeration), and the only widening rule is excluded from the mode. So the synthesized kind is the least one, and checking ≤ at each consumer is then complete.

The multi-site case. A field initialized to na synthesizes ⊥ at that site — but its kind is not stuck there: the principal kind of a record field is the join over all its construction and assignment sites. In the APP plane, a Model field written picked: na in init and picked: key (a string) in one arm of update has kind string, with na remaining a legal runtime value of that field (⊥ ≤ string). The fixpoint converges in one pass because the kinds being assigned never depend on the record itself. Declaring record Model { … } up front is the same thing written explicitly.

#Termination and determinism

The algorithm is a single bottom-up pass over the topologically sorted graph. It terminates because the lattice is finite by family and of finite height, the graph is acyclic (causality guarantees that), and ⊔, ⊓ and the algebra are all O(1) — there is no fixpoint iteration and no store of unification variables anywhere.

It is also confluent: a node’s synthesized kind depends only on the kinds of its inputs, and ⊔ is commutative and associative, so the result is independent of which topological order was chosen. Inference is therefore a deterministic function of the graph — the same program always yields the same kinds, hence the same emitted module. This is one of the foundations of the interpreter ≡ WASM byte-equality (see Compiler and runtime).

#Bounded polymorphism, resolved then forgotten

The catalogue is full of kind-preserving families: ema, sma, sum, highest, change, stat.stdev — each written (src: α ≤ quantity, len: lit) → ρ(α). This is the only polymorphism in v1, and it is deliberately shallow.

At each call site, α is resolved to a closed, monomorphic kind: α := the join of the kinds synthesized for the arguments in α positions; then α ≤ quantity is checked ([ErrArg] otherwise); then the return kind is the family’s shape instantiated at that α. For difference families, the shape is the δ derived from the frozen ± algebra: δ(price) = level.

a = ema(close, 20)              // α := price      ⇒ price
b = ema(rsi(close, 14), 9)      // α := osc(0,100) ⇒ osc(0,100)   — smoothing preserves the kind
c = change(close, 5)            // δ(price)        ⇒ level
d = change(rsi(close, 14), 5)   // δ(osc)          ⇒ osc, centred on 0

α is resolved and then forgotten. It is not a unification variable that persists across the program, so two sites can never contradict one another, and the “no general unification” property that keeps inference a single pass survives intact.

#Typing an unfinished program

An editor types a program that is being written, not one that is finished — so the algorithm assigns a kind to every editing state.

An unbound name (you are halfway through typing it) and a syntax hole (a parse error node) both synthesize a kind hole: a contained ⊤ that emits exactly one diagnostic ([ErrUnbound]) and does not poison its siblings.

From that follows the typable cone: the largest sub-graph in which every node, and every transitive input of every node, is free of ⊤ and free of holes. Live preview evaluates exactly that cone and renders the rest as --. A local mistake therefore never blanks the whole preview — a correct program has a cone equal to the whole graph, and a program with one unbound name still previews everything that does not depend on it.

The cone is a strictly editing-time artifact: a ⊤ in a consumed position is still a hard failure to emit code. The byte-identity guarantee is untouched.

#Incremental re-typing

On an edit, only the changed node and its downstream cone of kind consumers are re-synthesized; every other node’s kind is memoized under the pinned node identity that the compiler already maintains for hashing and common-subexpression elimination. Because the graph is acyclic and the lattice is monotone and finite, this converges in one downward pass.

Incremental re-typing is observationally equal to a full re-inference — it is the same function, memoized — so it can never disagree with the shipped module. It is what keeps the sub-16 ms editing budget, together with incremental parsing.

#Presentation is inferred, not configured

Here is the payoff of a kind system that tracks meaning. A kind already says what a value is; so it also says how it should be shown. That is why the first program anyone writes is one line long and needs no options:

Figure — kinds flow bottom-up; stdev is a dispersion (a vector), a literal multiple keeps its role, and point + vector = point lands the whole expression on the price axis — so it overlays.

The compiler derives a registry entry from the kind, and refines it with metadata from the operation itself:

registry := merge( reg(kind), opMeta(expression) )

reg(kind) supplies the defaults; opMeta refines them (an rsi adds its 30/70 guides). The complete default table:

The CSS class is part of the derivation, not a detail of the theme: the host stamps it on the rendered series, so a stylesheet can restyle every oscillator on the chart without any script naming a colour. It is the one place where “the presentation is inferred” reaches all the way out to the page.

Figure — reg(κ): each kind carries its own pane, scale, guides and CSS class, and the registry is merged with the operator’s own metadata. A string, a clock and a color are consumed, never plotted as a series; ⊤ and ⊥ are [ErrPlot]. None of it was configured.

Four rules complete the picture:

1. Overlay if and only if the value shares the price axis. Otherwise it gets a pane.
2. Co-plotting joins scales. Two series in one pane take the ⊔ of their bounds; if that join lands on quantity, you get [WarnBranchDim] and a suggestion to split the pane. (A price overlay next to a ratio pane is not a mix — it is two panes, and it warns about nothing.)
3. The final kind decides. level + price → price, so the expression overlays.
4. Reference lines from convention live in opMeta, not in the kind. osc(0,100) gives a midline; that rsi conventionally marks 30 and 70 is a property of rsi.

A record explodes into its fields, each presented at its own kind — which is why plot bollinger(close, 20, 2) yields three price lines plus a band, and plot macd(close) yields a centred pane with a histogram and a signal line, with no code to say so.

#Overrides — intent beats the default

Inference gives the default; the author overrides it in the plot block, and because the system knows the kind, the override is intelligent rather than blind:

m = macd(close)
plot m.macd { overlay }                  // a level FORCED onto the chart → it gets its OWN secondary axis
plot ema(close, 20) { pane }             // a price FORCED into a pane → auto-scaled, fine
plot m.hist { style: histogram, color: if m.hist > 0 then up else down }
plot rsi(close, 14) { guides: [20, 80] } // authored reference lines, kind-checked as level|osc

ich = ichimoku()                          // sourceless: it reads high/low/close itself
plot ich.chikou { offset: -26 }          // a DISPLAY shift: it moves the x position, never the value

Parameter UI is derived the same way: an input(…) synthesizes its kind, and the kind gives the widget (a numeric field with a range, a source picker, a boolean, an enumeration), with title:/group:/tooltip: as optional metadata. An accessibility descriptor is derived from the kind as well, so a plotted series is announced meaningfully without the author writing a label.

#What may be presented at all

Presentation admissibility is a judgment like any other, decided per kind, and enumerated exhaustively:

Note the deliberate asymmetry: dir is not plottable as a line and not orderable, but it is markable and is a legal bar-colouring channel. Its only presentation channels are the two that make sense for a three-valued direction.

Why enumerate instead of arguing. Because the lattice is finite by family, these tables are checked by machine — every kind, and every pair of kinds, is run through every judgment. “No kind is left without a semantics” is not a claim in a document; it is a test that fails when it stops being true.

#The error policy

An error is hard if and only if a load-bearing guarantee is violated — causality, totality, the firewall — or a dimensional impossibility appears in a demanding position. Everything else that is merely suspect is a warning with a quick-fix.

#Hard errors

The APP plane adds [ErrState] for an unbounded Model field, on exactly this pattern; see App plane.

#Warnings

Designed, not yet emitted. [WarnBoundsØ] (two osc bounds that intersect to nothing) is specified but the v1 engine has no emit-site for it yet. WarnNaNChain was an earlier documentation name for the code the engine actually raises — [WarnNaUpdate].

#What an error message is

A diagnostic is human, dimensional, actionable, and linked — never a stack trace:

price + osc — you are adding a price and a 0–100 oscillator.
  close + rsi(close, 14)
          ^^^^^^^^^^^^^^ osc(0,100), a dimensionless bounded value
  A point on the price axis and a dimensionless number have no common meaning.
  Did you mean  close + atr(14)  (a price + a displacement),
  or            close * norm(rsi(close, 14))  (scale the price by a fraction)?
  → kinds: the affine substrate

A refused repaint is explained, not merely forbidden (“this would make a past value change once the bar closes”), because the refusal is the feature.

Anti-cascade. A poisoned node propagates without re-diagnosing: one root fault produces exactly one message, and the nodes downstream of it stay quiet. A single typo does not produce forty errors.

#na at runtime

Kinds are static; na is the runtime story, and the two are designed to agree.

• Every comparison touching na yields na — never true, never false. Absence is tested with is_na(x) and presence with is_some(x), both signal.
• nz(x, d) (and its sugar x ?? d) substitutes a default; max/min absorb na pointwise, while window reducers propagate it (a window containing a hole yields na, matching the native oracle they must stay byte-identical to).
• A match on a possibly-na scrutinee must cover it — an na arm or _.
• Destructuring an na record gives every field na.
• A NaN produced by arithmetic is na — the kind is preserved, and it is displayed as a gap rather than as a failure. Division by zero is not an error; it is an absent value.
• Internally, na is forced to a single canonical bit pattern at every storage, hashing and serialization boundary. Nothing about that is observable in a program — it is what makes two engines agree on the bytes of a value that is not there (Memory model).

#See also

• Kinds — the lattice, the sorts, the tags, the named declarations.
• Operators — the dimensional algebra rule by rule.
• Grammar — how the modes of inference resolve the arrow and the container heads.
• Time and state — causality, warm-up, live() and the firewall in practice.
• Guide §12 — Working in the editor — kind-filtered completion, hover cards, the typable cone in live preview.
• Compiler and runtime — why deterministic inference is a prerequisite for byte-identity.