Marvin Mügge

Teaching the type checker arithmetic

Python’s scientific stack rests on one shared idea: a single n-dimensional array that everything else agrees on. TypeScript never got that layer. There are neighbours — a machine-learning framework here, a general math library there — but no typed n-d array that feels like infrastructure. What kept me circling the gap is that the missing piece is also the one place where a TypeScript answer could do something Python structurally cannot: put the type system itself to work on shapes, so a tensor bug surfaces while you type it instead of in production.

A question, not a product

NumType began as a question, not a product. The received wisdom says TypeScript can’t do arithmetic over dimensions of realistic size: the standard trick encodes a number as the length of a tuple, which costs one recursion step per unit of the value, and the checker’s recursion ceiling sits near a thousand. By that arithmetic, 1000 − 100 is out of reach — not slow, structurally impossible. I wanted to know whether the wall was real.

A change of representation

It isn’t — it belongs to the representation, not the checker. Turn a literal number into its decimal digit string and the problem changes shape: subtraction becomes schoolbook subtraction with borrow, digit by digit, the way children learn it. Seven digits cost about seven steps instead of a million. Comparison falls out of the same machinery almost free, which is how index bounds — negative indices included — get checked at compile time; written the same way, multiplication covers reshape and flatten, and a long division covers stepped ranges. The checker doesn’t count. It calculates.

The digit trick itself isn’t mine: the type-level community has run schoolbook arithmetic over digit strings before, in general-purpose utility libraries built to prove the checker can calculate at all. The missing piece was a job for that arithmetic — dimensions, bounds, slice lengths — where a computed number becomes a caught bug.

const win = NDArray.zeros([1024]).slice({ start: 100, stop: 1000 });
//    ^ hover: NDArray<[900]> — computed by the type checker

win.matmul(NDArray.zeros([5, 4]));
//         ~~~~~~ shape error, surfaced while typing

Two rules

Two rules kept the design honest. First: never wrong, only incomplete. Where a dimension is a literal, its shape is computed; where it’s a plain number, NumType stops promising and defers to a runtime check — the same gradual bargain that made TypeScript itself adoptable. A confidently wrong compile-time claim is a bug by definition, not a trade-off. Second: a minimum viable NumPy, not a clone. A deliberately narrow set of operations with the shape-typed core done properly beats four hundred operations with the interesting part skipped.

The other half

The numeric half is written from scratch — Rust compiled to WebAssembly, no binding generator, no borrowed math library — under one law: every fast kernel must produce answers bit-identical to the naive JavaScript reference, proven by a differential suite that includes the IEEE-754 edge cases nobody likes to think about. The package carries zero runtime dependencies, and a CI guard keeps it that way. But the squiggle is the product; the speed is there so the foundation is credible, not the other way round.

The way of working

The way of working is the same one that built this site, and the paper trail is public in the repository: every slice starts as a binding spec, gets implemented, and is then attacked by an independent verifier with a fresh context before it counts as done — with the findings recorded either way. The notes keep what went sideways, because that’s where the lessons live: the zero-copy plumbing I was proud of turned out not to be the bottleneck at all; vectorizing the elementwise operations measured as a dead end while removing a single per-element allocation was worth an order of magnitude; and one use-after-free was caught not by me but by the verifier sent to break my work. Editor latency — the whole promise — was measured against the real language server with a headless harness, and the hovers come back in a few hundredths of a millisecond.

Small on purpose

The library is small and may stay small. What I wanted to exist is the foundation stone: proof that TypeScript’s missing NumPy can carry types that do arithmetic — and that the proof fits in an editor hover.

NumType is on npm — code and research notes on GitHub.