topos

Why it is shaped this way

Vision

The argument, the three commitments, and the five rules.

0 Parameter[2, 2]0 Parameter [2, 2]1 Input[1, 2]1 Input [1, 2]2 MatMul[1, 2]2 MatMul [1, 2]3 Tanh[1, 2]3 Tanh [1, 2]4 Mul[1, 2]4 Mul [1, 2]5 Sum[]5 Sum []6 Leaf[]6 Leaf []7 Broadcast[1, 2] shape=[1, 2]7 Broadcast [1, 2] shape=[1, 2]8 Leaf[1, 2]8 Leaf [1, 2]9 Add[1, 2]9 Add [1, 2]10 Mul[1, 2]10 Mul [1, 2]11 Mul[1, 2]11 Mul [1, 2]12 Leaf[1, 2]12 Leaf [1, 2]13 Add[1, 2]13 Add [1, 2]14 Add[1, 2]14 Add [1, 2]15 Leaf[1, 2]15 Leaf [1, 2]16 Mul[1, 2]16 Mul [1, 2]17 Sub[1, 2]17 Sub [1, 2]18 Mul[1, 2]18 Mul [1, 2]19 Leaf[1, 2]19 Leaf [1, 2]20 Add[1, 2]20 Add [1, 2]21 Permute[2, 2] order=[1, 0]21 Permute [2, 2] order=[1, 0]22 MatMul[1, 2]22 MatMul [1, 2]23 Permute[2, 1] order=[1, 0]23 Permute [2, 1] order=[1, 0]24 MatMul[2, 2]24 MatMul [2, 2]25 Leaf[1, 2]25 Leaf [1, 2]26 Add[1, 2]26 Add [1, 2]27 Leaf[2, 2]27 Leaf [2, 2]28 Add[2, 2]28 Add [2, 2]
Plate 1. One small graph and its derivative, drawn from the spec. The lighter nodes are the ones differentiate appended: the chain rule as more of the same graph.

Topos is an autodiff compiler stack. Record a graph, inspect it, differentiate it, compile it, emit it. The spec is an immutable value and the state is yours. The network never moves; a training step is a pure data transform of caller-owned parameters.

The goal is a complete compiler whose first-principles design makes it the easiest place to build the next thing. Better a few strict rules than lots of features: that is how the next idea stays easy. Once the graph is written, its sizes do not change.

That means three commitments:

  • The whole modern ML-compiler stack, small enough to read. One spec, a short list of named interpretations of it. Every stage is visible and printable, none of it magic.
  • Every result provable. The plain interpreter is the executable spec; anything faster must match it, bit for bit by default. A claim is one assert away from proof.
  • Built for learning and research. New ideas plug in at named seams, with the oracle as ground truth. The core stays closed and simple on purpose. Completeness is the point: the stack aims at the whole compiler.

A typical compiler rewrites the program until it becomes something that can run. Topos does not. The tape is written once; everything after it is a named way of reading the same spec. That list is the compiler — small enough to read because there is nothing else.

  • Recording writes the tape and infers every shape at the expression that records it. Sealing freezes that as the spec.
  • The interpreter runs it. Those bits are the truth.
  • Reverse mode is the same scan backward. The same derivative rules can also record themselves as ordinary nodes, so compiled training is a forward plan over that extra tape — fusion and liveness then apply to the chain rule itself.
  • A plan is a schedule of what to run, what to keep, and what to free. It is derived from the spec and holds no state.
  • Fusion is an offer a run may elect, never a rewrite of the tape.
  • Emission writes the plan as text for an industrial backend. It is a sibling of describe, not a second compiler.

That list is also where new work lands. A new element type, a new fusion, a new backend, a new emission target, a new AD mode — each plugs in at a named seam and is proven against the interpreter. The idea does not need a fork, and a hand-rolled equivalent has the same standing as a built-in.

Adoption may follow; it is never chased. No benchmark races, no coverage races, no plugin bazaar.

Who it is for#

Learners and teachers first. The crate teaches autodiff, and what a compiler does with it afterwards, by being small enough to read with every stage printable: the spec, its gradient, the schedule, and the emitted text are readings of one graph, and every claim is one assert from proof.

Systems researchers second. A new element type, AD mode, fusion, backend, or emission target plugs in at a named seam and is graded against the interpreter, without forking the crate.

Production is an export of that discipline, not a third promise. What the stack hands over is a closed, statically shaped function with a shipped oracle and a StableHLO boundary, embeddable in a Rust process. It is offered where it fits and never chased: there is no coverage race with the general frameworks, and the ground worth holding is the small, checkable stack.

The rules#

Five rules, one axis each: what a program means, what may be read, what is true, how a faster form earns its spelling, what the core owns.

  1. The tape is the spec. Recording writes it, sealing fixes it. Everything downstream — derivatives, plans, fusions, backends, emission — is a derived artifact: free to change the spelling, forbidden to change the meaning. Shapes are static and tapes are cheap — one tape per shape bucket, re-record rather than generalize. A plan holds no state, so it survives every training step and every reopen.
  2. Say what you want to read. Observability is declared — roots and observes — never inferred, and a read outside the declaration fails loudly. The declaration is the license every optimization runs on: the observed must survive any rewrite; the unobserved is fair game to fuse away.
  3. The interpreter's bits are the truth. The plain interpreter is the executable spec: whole-spec evaluation always walks the reference paths, so its bits are the same in every build, on every platform. Every plan, backend, and emitted module must reproduce those bits under the exact posture; a compiled backend serves only under the fast posture a plan or an entry declares. Seeded runs replay exactly; anything that reorders float math is that labeled option, never a silent one.
  4. Composition is the default. A fused or native form buys its way in with a measured reason — float behavior or real cost. The primitives compose; specialized spelling is earned.
  5. The core is enough; facades prove it. The core owns exactly what the crate exists to do. Every facade — layers, optimizers, losses — composes through the public surface alone, so a hand-rolled equivalent behaves identically and each facade stands as proof that the primitives suffice.

Principles#

Constraints the vision names without arguing. One file per principle; the type names in each "Spelled today" section may rot, the rest must not.

Openings#

Decisions and what they paid for, in openings. Not constraints — consequences. An opening may wait on a seam that is designed but not yet collected.