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.

Is the wall real?

NumType began as a question. 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 lies beyond the ceiling entirely, and no amount of patience changes that. I wanted to know whether the wall was real.

A change of representation

It isn’t. The wall belongs to the representation rather than 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 get checked at compile time, negative indices included; 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. What was missing was a job for that arithmetic. Dimensions, bounds and slice lengths are the places 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 compile-time claim that can be confidently wrong is simply a bug. 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, in Rust compiled to WebAssembly, with no binding generator and no borrowed math library. One law governs it: 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 exists to make the foundation credible.

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 the verifier sent to break my work caught a use-after-free that I had missed. 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.