· 6 min read
The collapse flag
Reading HVM4's single-file runtime shows the interaction calculus surviving its fourth rewrite while the machine around it quietly turns from an evaluator into a program-search engine.
This morning I published an essay about learning to read the output of HVM2, the interaction-net runtime under Bend, with a pencil and a pinned version number. By dinnertime the pin had slipped. The repository worth reading is HVM4, unreleased and warning you off five lines into its README, and according to its author an HVM5 already exists and runs five times faster. So this follow-up trades the pencil for the source: HVM4's entire runtime is one 6,435-line C file, and I spent the evening in it.
Two things came out of that reading. The calculus at the center has barely moved through four rewrites, while everything around it has been replaced every time — and the newest machinery exists to run many candidate programs at once and fish out the one that answers.
Four machines, four bets#
The lineage is short but violent. Each generation kept the theory and re-bet the engineering:
HVM1 promised to be "exponentially (in the asymptotical sense) faster than alternatives, including Haskell's GHC" on higher-order code, and its README still says "Production Ready Soon!". HVM2 went strict, targeted CUDA, got a paper, and became the machine Bend shipped on — the one this morning's essay dissected. Then the third swung back to lazy, swapped Rust for Haskell, and grew a compiler that lifts hot fragments into C.
Lazy, strict, lazy: the same theory keeps auditioning in different theaters. An ecosystem lives downstream of every audition — Bend programs, tutorials, my own morning essay — and it reinterviews for its part each time.
The calculus that survives every rewrite#
What never changes is the Interaction Calculus: a lambda calculus where variables are affine and global, plus two dual constructs — duplication, which lets one value exist in two places, and superposition, which lets two values exist in one place. The whole engine is four rewrite rules. Here are the two that do the work, straight from the theory doc:
(λx.body)(arg) ! x &L= &L{a, b}; t-------------- APP-LAM ------------------- DUP-SUPx ← arg x₀ ← abody x₁ ← b tIn HVM4 every one of those terms is a single 64-bit word — an 8-bit tag, 24 bits of label, 32 bits of payload. The 6,435 lines are mostly the four rules multiplied out across numbers, constructors, and pattern matches: 61 interactions, each with its own documentation file and a sequent-calculus comment in the source.
The load-bearing subtlety is labels. A duplication meeting a superposition with the same label annihilates, pairing first with first; different labels commute and produce every combination:
(&A{1, 2} + &A{10, 20}) (&A{1, 2} + &B{10, 20})-----------------------&A{11, 22} &A{&B{11, 21}, &B{12, 22}}Read that right column again. Two two-way superpositions with distinct labels just computed a four-way cross product in one expression. Every node picks, through its label, whether it zips pairwise or multiplies into every combination.
The second purpose#
A cross product of every choice is a search space, and this is where HVM4 stops being a faster HVM2. Collapse — enumerating the plain lambda terms hiding inside a superposed result — is a first-class CLI flag, -C10 meaning "give me ten answers." And once you know to look, the term table reads like an inventory for something other than evaluation:
| Sign in the repo | What it is for |
|---|---|
ANY | A wildcard that "duplicates itself, equals anything" — a hole a search can fill |
| Stuck names | Heads that stay symbolic instead of reducing away |
| Equality node | Structural comparison as a term inside the machine |
| Priority wrapper | Steers which branches the collapser visits first |
| Runtime labels | Superpositions whose labels are computed while the program runs |
None of those make Fibonacci faster. And the benchmark directory gives the game away — gen_mul4k.hvm does not compute a number:
@expr = λ&L. λ{ 0n: λf. λx. x; 1n+: λ&K. λf. λx. ! f &(L) = f ! x &(L) = x &(L){f₀(x₀), 1n+@expr(L+1,K,f₁,x₁)}}@main = ! &F = λF. @muln(1, 100000n, F) ! e0 = @Y(F)(3n) === 12000n ! e1 = @Y(F)(4n) === 16000n @when([e0,e1], [F])@expr superposes, at every step, "stop here" against "keep building," using a fresh runtime label per layer so choices multiply instead of pairing. @main then constrains an unknown function to satisfy two equations and asks the collapser for whatever survives. The output of this benchmark is a program. That is SupGen, the program-synthesis project this runtime now clearly serves, sitting in the folder where fib benchmarks used to live.
Honesty requires an asterisk here, in two directions. The November announcement promised compilation of interaction-calculus functions to "zero-overhead machine code", and the word compile appears nowhere in this repository — so the public HVM4 is a very fast interpreter, and the compiler lives somewhere I cannot read yet.
The other direction: unlike this morning's essay, nothing here was executed. The README says "you're here before launch. Use at your own risk," and every reduction quoted above is the repo's own documented output, not mine. I read the machine without once turning the crank, and a benchmark of my own is the obvious debt for a third essay.
The Jacquard loom in the picture above holds its whole pattern space in a chain of punched cards, and weavers rebuilt looms around the card chain for a century without changing the cards. Four runtimes in, that is what the Interaction Calculus looks like to me — and somewhere past the pin I set this morning, the fifth loom is reportedly already threaded.