Tracked values and the tape

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 mica-container/examples/TrackedValues run

TrackedValues — 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)

a routine of its own: cube = 3.375000, d/dx = 6.750000

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 float — float16, bfloat16, float32 or float64 — or a tensor of any rank over one, 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 — a routine the window calls records into it, so open the window in the program’s body and call the routine from there

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

A routine of its own

A function or a procedure takes tracked values and answers one, and a call inside the window records its body as if it were written there:

function Cube(z : tracked float64) : tracked float64;
begin
    Cube := z * z * z;
end;

tape
    loss := Cube(x);
end;

Backward(loss);
g := Gradient(x);    { 3·x² at 1.5 — exactly 6.75 }

A tracked parameter crosses as the pair: the call hands the routine the history its argument carries, and the answer comes back with the history the body recorded. Parameters may be const, results and locals may be tracked, scalars and tensors alike, and a routine may call another that records — the whole chain lands on the one tape. Outside every window the same routine computes plainly and records nothing. A record holding tracked members enrolls them at the call, which Model depth shows, and a library’s routine records the same way, through the copy its contract names.

The window is still one task’s story, so a routine it calls may not open a concurrent block there (error 5627):

a concurrent block cannot stand inside ‘Train’, which the tape window calls while it records: the routine’s body runs inside the window’s transcript, one task’s linear story, and tasks running beside the recording would interleave what the reverse walk must read in order — schedule from a routine the window does not call, and record only the arithmetic

A task, a generator and a callback take no tracked parameter, because each runs beside a window rather than inside it, and a generator and a callback do no tracked work at all. A generator’s refusal (error 5628) names the road out:

the generator ‘Batches’ works on tracked values here: a generator’s body runs between its consumer’s pulls, and a tape window that pulls it would never see this work on its tape, so a generator computes on plain values only — do the tracked work in a routine, which records when the window calls it, and let the generator produce plain values

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, and each records at exactly the shapes its name computes at:

So y := Exp(x) records over a tracked float64 as it does over a tracked vector, and its gradient is exp(x) itself. Each verb keeps its plain signature, judged over the value halves, and its plain shape rules. Tanh over a matrix is TanhMap’s work, 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

The same sentence answers Sigmoid or Relu over a tracked scalar, which have no scalar word in the language; there the logistic curve is written as 1.0 / (1.0 + Exp(-x)), and every operation in it records.

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.