A variable declared tracked is a pair: the value your program computes with,
and the id of the tape node that remembers where that value came from. The
AI course teaches what that machinery is for — this
page teaches the feature itself: what records, what refuses, and what every
answer means, with each rule quoted from the compiler that enforces it.
The example is examples/TrackedValues
in the tutorial repository.
Getting the file
make -C examples/TrackedValues runTrackedValues — the pair, the window, and the walk
the pair: x holds 3.000000, read back as plain data
one window: loss = 9.000000, d loss/d x = 6.000000
fan-out: d/dx = 7.000000, d/dy = 3.000000, d/dz = 3.000000
never recorded: d/dw = 0.000000; stale from the last window: d/dy = 0.000000
a tracked vector: d/dv = (10.000000, 100.000000), its value half = (2.000000, 3.000000)Every number is an exact dyadic rational — identical on every machine, at every optimization tier, on both architectures.
The pair
var
x : tracked float64;
v : tracked vector[2] of float64 := (2.0, 3.0);The inner type is a float32, a float64, or a vector or matrix over them —
the types whose derivative arithmetic the tape carries. Ordinary code touches
only the value half. A plain assignment writes it, a literal fills a tracked
tensor’s value half directly, and reading the variable into a plain twin
answers it:
x := 3.0; { the value half, written as ordinary data }
xv := x; { and read back the same way }
v := (8.0, 16.0); { a literal fills a tracked tensor's value half }One wall stands here, and it is the ordinary aggregate-literal rule, not a tape rule: a tracked scalar is a single float, so a list of values has nothing to fill —
an aggregate literal writes a whole composite value, and ’tracked float64’ is not one … assign the single value this position wants instead
Assignment between the tracked and the plain world is judged by the value types: a plain value entering a tracked variable promotes into its inner exactly as the plain pair would, and a tracked-to-tracked assignment copies both halves, so a value’s history travels with it.
The window and the walk
The tape is one per program, and its transcript is recorded inside the
tape … end window:
tape
loss := x * x;
end;
Backward(loss);
g := Gradient(x); { 2·x at 3 — exactly 6 }The window stands in the program’s own body — not in a subprogram, not inside a concurrent block, not inside another window. The compiler states the law itself (error 5465):
the tape window must stand in the program’s own body, outside every other window and every concurrent block: the tape is one per program in this delivery, its transcript is one task’s linear story, and the window is where that story is recorded
Backward walks one closed window exactly once, from one scalar seed, and the
walk comes before any Gradient read. Both rules are runtime traps at a named
line:
Backward was called twice on one tape window
Gradient was read before Backward walked the tape window
The recorded vocabulary
Inside the window, the operators + - * / and negation record — they
are the operations whose derivative rules the reverse walk carries. Beside
them stands a curated set of recorded verbs from the math unit: Sum,
Hadamard, Tanh, Exp, Ln, Sqrt, Softmax over vectors,
RowSoftmax, TanhMap, LayerNorm, CrossEntropy over matrices, and Dot
and Transpose from std. Each verb keeps its plain signature, judged over
the value halves — and each keeps its plain shape rules. Tanh is
vector-only, and the compiler says so in the tape’s own vocabulary (error
5473):
‘Tanh’ on tracked operands records onto the tape, and the recorded form wants a vector over one float element type: got ‘matrix[2, 2] of float64’ — the recorded vocabulary keeps each verb’s plain signature, judged over the value halves
A verb outside the vocabulary — Row, say — does not record, and the
compiler names the road out (error 5503):
‘Row’ does not record onto the tape: the recorded vocabulary carries only the verbs whose derivative rules the reverse walk knows, and the tracked argument at position 1 cannot travel a call outside it — read the value half into a plain variable by whole assignment, and hand ‘Row’ that plain value
Fan-out, and the two honest zeros
One knob feeding the loss through two roads collects blame from both — the reverse walk adds contributions where the forward story branched:
tape
loss := x * y + x * z;
end;
{ d/dx = y + z: the two roads' blame, added }And two answers are zero by design rather than by accident. A tracked variable the window never recorded still carries a zero id, so its blame is zero. A variable recorded in an earlier window carries an id into a transcript that no longer exists — the next window reset the tape — and a stale id answers zero the same way. No recorded road, no blame; the tape never guesses.
The tape under a fixed arena
The tape lives wherever the program’s memory class puts it. Under
--memory-class fixed-arena the window reset returns the transcript’s storage
wholesale, so a training loop’s tape reaches its high-water mark in the first
round and holds it — a bounded arena runs an unbounded number of rounds. The
same program, hosted or fixed-arena, prints the same digits.
Where this sits
The AI course teaches what the tape is for, from the first recorded window to a trained GPT. The typesystem reference carries the tracked row’s one line: no capabilities, deliberately — a tracked value’s operations are the autograd rules that record onto the tape, never the capability-gated machinery.