My type checker is a table

Change the last return from n - 1 to n and I want the program to stop compiling. No test happened to find the bad input. The function promised a valid index, and its body failed to deliver one.

That is a useful place to start a type system. I want the promise to be cheap enough that I can put it on ordinary code, including code I am still editing. So I built a small checker with integer refinements, then kept the checking rules fixed while changing how it stores and updates the facts.

On the largest synthetic function I measured, checking fell from 15.8 milliseconds to 0.44. The two-parameter example barely moved. Both results belong in the story: there is a substantial speedup here, but it comes from removing a particular kind of repeated work.

Start with the program you want to reject#

Here is the little function. Given a positive length and any integer, it clamps that integer into the usable index range. The notation inside braces means an integer satisfying the predicate after the bar.

// Proposed surface syntax. The implementation below consumes an AST.fn slot(i: Int, n: {v: Int | 0 < v})  -> {v: Int | 0 <= v && v < n} {  if i < 0 { return 0 }  else if i < n { return i }  else { return n - 1 }}

The result still has the ordinary shape Int. Its refinement says more about which integers can come back. The promise mentions n, a value supplied at runtime. We do not need a separately compiled version of this function for every possible length.

The Flux tutorial gives a practical introduction to this arrangement: refine a base type with a predicate, check a function under its input assumptions, and establish its output guarantee. I am implementing a much smaller language here, with its own checker. There is no Flux or external solver hidden behind the examples.

The previous Numbers are sets argued for treating numeric facts as numeric facts rather than encoding the magnitude of a number in a tower of types. This time I wanted working code. A library encoding can be clever and still ask the host checker to evaluate far more machinery than an integer comparison needs.

Building the language yourself gives you a choice at that boundary. A bound can be a native part of checking. You get to choose its representation, its supported arithmetic, and how long its facts survive. That is where I would look for the large improvement, before writing a faster interpreter for elaborate type-level programs.

Choose a small arithmetic language#

My checker accepts conjunctions of facts shaped like x - y <= c, where c is a constant. This is enough for ordering, constant offsets, and bounds relative to a length. Give the constant zero its own slot and ordinary lower and upper bounds fit too.

0 <= i          becomes     0 - i <= 0i < n           becomes     i - n <= -1x + 3 <= y + 7  becomes     x - y <= 4x == y + 2      becomes     x - y <= 2  AND  y - x <= -2

The subtraction of one in the strict comparison is important. These are mathematical integers, so i < n means i <= n - 1. The same rewrite would be wrong for arbitrary real numbers. Equality is represented by two opposing bounds; the tiny front end exposes those as two conditions rather than adding another solver operation.

This fragment deliberately excludes x + y <= z, multiplication of variables, and arbitrary Boolean formulas inside a refinement. The checker rejects unsupported syntax. It does not approximate an unfamiliar assertion to true and carry on.

The restriction buys a specific data structure: a difference-bound matrix. Antoine Miné's work on this abstract domain describes compact relational numeric invariants and graph-based operations on them. That paper appeared at PADO II in 2001; the arXiv upload is from 2007. The underlying idea is established compiler machinery, not something I invented for this article.

There is current interest in making numeric refinements more usable too: Valentin Aebi and Carlo A. Furia's Practical Range Refinement Types with Inference was submitted on July 1, 2026. My experiment takes the smaller starting point of explicit input and output contracts. Inferring those contracts is a separate problem, and it is not included in the timings below.

The ordinary checker comes first#

The complete implementation starts from typed syntax trees. I skipped the parser so we can spend the example on checking rather than tokenization. The source-like snippet above is proposed notation; this is how the runnable fixture constructs it.

const i = variable("i");const n = variable("n");const result = variable("result");const slot: FunctionDef = {  name: "slot",  params: [{ name: "i", type: "Int" }, { name: "n", type: "Int" }],  requires: [lt(int(0n), n)],  ensures: [le(int(0n), result), lt(result, n)],  body: branch(lt(i, int(0n)), ret(int(0n)),    branch(lt(i, n), ret(i), ret(offset(n, -1n)))),};checkFunction(slot, "batched"); // returns normally

The helper functions and FunctionDef are exported by the implementation. Integer literals use TypeScript's bigint, which keeps arithmetic exact. Every integer expression in this language normalizes to one named value plus a constant offset, or to a constant alone.

Before reasoning about predicates, a shape pass checks names and operand types. Adding an offset to a Boolean fails there. Returning a Boolean from one of these integer functions also fails. It checks the whole body, including branches that arithmetic might later prove unreachable.

Only then does the refinement pass assume the input contract. At each return, it substitutes the returned expression for result in the output contract and tries to prove the resulting conditions. Assuming the desired output at that point would make the checker beautifully fast and completely useless.

For return n - 1, the two goals become 0 <= n - 1 and n - 1 < n. The first follows from the positive input length. The second holds for every mathematical integer. Change the return to n and the upper-bound goal becomes n < n. That fails.

There is also an explicit policy for impossible input contracts: reject them. A function requiring both n > 0 and n <= 0 should not get a reassuring checkmark merely because no caller can satisfy its premise. An impossible branch inside an otherwise usable function is different; we can skip its refinement obligations after checking its ordinary syntax and types.

Put the facts in a table#

Each entry D[a, b] stores an upper bound on a - b. Smaller numbers express stronger facts. An absent entry means no finite bound is known. The diagonal starts at zero because a value minus itself is zero.

Consider the middle return in slot. We know the input length is positive, the first test was false, and the second test was true. With rows and columns named 0, i, and n, the closed matrix is small enough to read directly.

Checking i < n now reads the i,n cell and compares it with -1. The same cell cannot prove i <= n - 2. We retained exactly the distinction an off-by-one mistake needs.

“Closed” means we have propagated consequences. If x - y <= 3 and y - z <= 4, adding them gives x - z <= 7. An all-pairs shortest-path calculation carries out these combinations. A negative diagonal means the assumptions imply x - x < 0, so the context is inconsistent.

The first implementation uses Floyd–Warshall closure after each new nonredundant fact. It is short, easy to inspect, and gives us a reference version. With V slots, the matrix takes quadratic space and a full closure takes cubic loop work. Once closed, a bound query needs one matrix lookup and one integer comparison.

There is no universal constant-time claim hiding in that last sentence. A comparison between enormous integers costs more than a comparison between small ones. Using bigint avoids silently exchanging correctness for convenient floating-point arithmetic.

A branch gets its own facts#

The first test, i < 0, adds a fact to its true branch. The false branch must receive the negation, not an empty context. For an integer atom a - b <= c, that negation is b - a <= -c - 1.

const [a, b, c] = normalize(body.test, names);const yes = context.fork();yes.assume(a, b, c);visit(body.yes, yes, path + "/then");const no = context.fork();no.assume(b, a, -c - 1n);visit(body.no, no, path + "/else");

Both branches fork from the parent. The false branch does not inherit the true branch's facts. A shared mutable context would otherwise make contradictory assumptions meet and could allow arbitrary return claims through an unreachable-state shortcut.

This is also why the proof engine has a separate inconsistent-state flag. It can stop exploring an impossible path without pretending the matrix still describes an ordinary set of reachable values. The tests include branch isolation and a check that adding an empty batch cannot accidentally revive an inconsistent context.

At this point the checker can verify all three returns. Its state consists of ordinary types, stable names for integer values, and one local table per active path. There is no recursive type computation proportional to the numeric value of n. There is, however, a lot of repeated closure work.

Stop rebuilding what the last fact already established#

Suppose the matrix was closed before we learned a - b <= c. Any newly tighter path has to use that new bound. Provided it does not create a negative cycle, a shortest useful path need use the new bound only once.

So a new route from i to j can combine the old route to a, the new bound, and the old route from b. That gives this update:

// D is already closed. Add a - b <= c.// First reject a negative cycle: D[b, a] + c < 0.D_new[i, j] = min(D_old[i, j], D_old[i, a] + c + D_old[b, j])

The contradiction test checks whether the new edge closes a negative cycle through the old reverse path. Otherwise, two nested loops update all affected pairs. The implementation snapshots the old column and row first, so in-place writes do not change the inputs to later updates.

That replaces a cubic closure with quadratic work per new fact. Facts already implied by the matrix return immediately. Both versions use that redundancy check; the comparison does not make the reference version do work that the optimized version avoids with an unrelated shortcut.

Then there is a more basic improvement. At function entry, every precondition is already in front of us. We do not need to close the table between reading the first and second line of the signature.

The third version inserts all entry bounds, closes once, and uses the incremental update for facts learned at branches. With E entry facts, the repeated-closure approach has a worst-case entry cost of O(EV³). Incremental insertion makes that O(EV²). Batching costs O(E + V³), before the body. These count arithmetic operations; integer width remains part of their real cost.

I would keep both batch and incremental operations in the checker API. A signature arrives as a batch. A path condition arrives as a new fact about an existing context. Making both callers use the same update strategy throws away information the compiler already has.

The measurement, including the boring case#

I timed complete calls to checkFunction, including the shape pass, normalization, fresh matrices, branch copies, and return checks. The syntax trees were built before timing. There is no parser, code generator, process startup, or file I/O in this measurement.

Besides slot, the fixture builds functions with 8, 16, or 32 integer parameters. Each parameter starts between -1000 and 1000; adjacent parameters are ordered; the last is positive. The body clamps the first parameter into the range below the last. This is a synthetic stress case for accumulating related facts, not a sample of somebody's production compiler workload.

The largest case improves by about 36 times from the straightforward reference to the batched version. The incremental version accounts for a large part of that gain, but batching the signature still matters. The matrix has 33 slots here, including the distinguished zero.

Meanwhile, the smallest case goes from roughly 7.2 to 6.6 microseconds. Its sample ranges overlap. I would not use that row to promise a meaningful improvement for tiny functions.

The environment was Node.js 22.16.0, TypeScript 5.8.3 emitting JavaScript, and a shared Debian 13 x86-64 container reporting an Intel Xeon Platinum 8573C. Everything ran on one thread. The harness uses three warmup batches, nine measured batches, and rotates the order of the implementations. Including warmups, it executed 112,428 function checks.

The raw results preserve every sample, batch size, environment notes, and source hashes. For the largest case, full closure ranged from 15.33 to 19.17 milliseconds; batching ranged from 0.392 to 0.481. Shared-machine noise, warm JIT behavior, and the small batch size of that expensive case all limit how precisely to read the ratio. I did not measure peak memory or cold startup.

Most importantly, this compares three implementations of the same small checker. It does not compare against Rust, TypeScript, Flux, or Z3. The Programming Z3 tutorial already describes specialized procedures for arithmetic fragments, including difference logic. A mature solver is not obliged to rediscover integer ordering with a general-purpose search every time.

The result I can support is narrower and useful: expressing bounds directly gave this checker an exact, compact problem, and changing when it computed closure removed most of the cost on the stress fixture. Adding arbitrary predicates to an existing type system would not automatically reproduce that result.

Make the fast version earn its answers#

I did not trust agreement between the first two implementations on one successful function. They share the same representation and could share the same mistake.

The test fixture checks 4,000 seeded random constraint prefixes against an independent Bellman–Ford implementation working from raw edges. It compares consistency and, for consistent contexts, every pairwise bound. A fresh batched closure is checked alongside the two update strategies.

A second test enumerates 900 small bounded systems. With two integer variables restricted to -2 through 2, it can enumerate every concrete assignment and compare both satisfiability and entailment against all three matrix implementations. That provides a different route to the expected answer.

At the language level, the fixture generates 109 small branching programs. All modes agree on the 13 accepted programs; interpreting those on 1,872 concrete inputs satisfies their return contracts. Negative tests cover the off-by-one return, the missing positive-length premise, unknown names, Boolean arithmetic, contradictory preconditions, branch leakage, and an unsupported expression. There are also exact-arithmetic tests beyond JavaScript's safe-number range.

These checks passed. They are not a formal proof of the implementation. For the verified foundations, Simon Wimmer and Peter Lammich's Archive of Formal Proofs development formalizes DBM operations and their canonical forms. My TypeScript code does not inherit that verification by using the same name.

The standalone fixture needs no new dependency in this repository. After its normal install, these commands type-check the examples, run the regression corpus, and run the benchmark. The recorded timing run used emitted JavaScript; the commands below use the repository's tsx runner, so treat a new run as a new measurement.

pnpm exec tsc -p examples/tsconfig.difference-refinements.jsonpnpm exec tsx examples/difference-refinements.test.tspnpm exec tsx examples/difference-refinements.bench.ts

The fixture configuration is separate because the blog's application typecheck does not include the examples directory. The checked-in results record the compiler version actually used, rather than assuming it matches whichever compiler the site currently installs.

What I would put in a real language#

I would keep the separation that made this implementation manageable: ordinary types establish shape; refinements establish a chosen set of value relationships; explicit function boundaries keep the proof contexts local. The earlier Make the type checker forget explored how those boundaries could fit Blot. Here we have an executable piece of that idea, with a cost we can inspect.

The current implementation caps a context at 256 slots and rejects a larger one. Dense quadratic storage is a reason to keep functions local, not permission to allocate a matrix for every value in a project. A production checker could use sparse representations or partition unrelated variables, but it would need new measurements and correctness checks.

Mutation is a more serious extension than another AST case. A fact about the old value of a variable must not silently become a fact about its replacement. I would give assignments fresh value identities, then define how joins retain only facts justified on every incoming path. Loops also need a preserved invariant or a sound fixed-point analysis. None of those operations is implemented in this fixture.

For function calls, an extension would check the callee's input requirements under the caller's facts, then import a renamed copy of its verified output summary. That is a useful interface for separate checking. It still needs rules for recursive definitions and escaping identities; merely serializing a local matrix is not enough.

Machine arithmetic needs its own deliberate choice. With wrapping unsigned bytes, 255 plus one is zero. The mathematical fact that adding one increases a value cannot justify that operation. A language can prove the addition stays in range, insert an overflow check, or use a solver with the intended bit-vector semantics. This example chooses unbounded integers so its arithmetic meaning is unambiguous.

Likewise, proving an integer is below n does not yet authorize an unchecked load from any array nearby. The compiler must connect n to that particular live array and account for changes to its length. Only then could a backend use the proof to remove a redundant bounds check. This article measures checking speed; it contains no generated machine-code benchmark.

I would grow the predicate language only when a real program needs something the current fragment cannot express. A general solver can be a reasonable next layer. Its unresolved obligations must remain unresolved, and expensive proof search should have a visible budget. An arithmetic theory chosen for predictability is valuable precisely because we know where its guarantees stop.

The function at the top is still my test. Let me write the bound in the signature. Reject the return that is one too large. Keep the common relationships in a representation the compiler can update without starting over. A small table does that job surprisingly well.