The nodes HVM5 skips

I ended the HVM4 article with a fifth loom reportedly threaded. Then I typed HigherOrderCO/HVM5 into GitHub and got a 404. As far as I can tell, public HVM still ends at HVM4. Outsiders have a June 6 announcement and one benchmark screenshot for HVM5.

The available material still reveals a direction. HVM5 looks less like a new calculus than a new boundary between code and data: keep lambdas and matches static when possible, drive them through a CEK-like evaluator, and stop building interaction nodes whose only job is to be consumed immediately.

The memory column gives it away#

Victor Taelin's announcement says HVM5 is done, runs about five times faster than HVM4, and keeps SupGen happy. I copied three rows from the attached screenshot because the headline hides the interesting part:

The first two workloads get much faster while their peak memory falls from five-digit megabytes to a handful. regex-match loses throughput, and other rows in the screenshot do too. The runtime has a workload shape rather than one constant multiplier.

Adding the displayed wall times gives HVM5 a little over a threefold improvement across that table, which leaves the post's fivefold figure dependent on a subset or another aggregation the screenshot does not name. Fine. Either calculation leaves the same heap profile: HVM5 performs roughly the same class of reductions without dragging gigabytes of graph behind them.

The prompt before the runtime#

One week before the announcement, Taelin published a design prompt for rebuilding HVM from scratch. I cannot prove the resulting experiment became HVM5, but the timing, SupGen target, and benchmark vocabulary make it the strongest public clue I found.

The prompt reaches back to an older CGen evaluator that reportedly handled far more interactions per second by matching eliminators directly against values. Its CEK-style transition rules look almost offensively ordinary:

app (Mat a b) (Inl x   : s) = app a (x:s)app (Mat a b) (Inr x   : s) = app b (x:s)app (Get b)   (Tup x y : s) = app b (x:y:s)

A match sees an injection and jumps to the corresponding branch. Tuple elimination receives both fields without first allocating a lambda-match node, an application node, and the links required to remove them again. Static function bodies behave as code while environments and arguments carry the changing state.

HVM4 already separates static book terms from dynamic heap terms. Its memory documentation gives every term the same 64-bit representation and uses ALO nodes to expand immutable book terms lazily into mutable heap terms. Even ALO-LAM creates a fresh linked binder before evaluation can continue. That machinery preserves graph sharing, and the benchmark records its allocation cost.

Duplication keeps the hard part#

Direct dispatch is easy until a duplicated value turns out to be a lambda. The design prompt singles out DUP-LAM because either projection may force the value first, somewhere far from the other one:

! F &L = λx.f----------------! G &L = fF₀ ← λ$x0. G₀F₁ ← λ$x1. G₁x  ← &L{$x0,$x1}

Whichever side arrives first must create two related lambdas and leave the other side pointing at the same decision. Re-evaluating the closure independently would discard the sharing discipline that keeps Interaction Calculus from exploding on precisely the search programs HVM is built to run. Why? Why is the node you most want to remove also the node carrying the asymptotic guarantee?

The screenshot suggests a useful compromise. Its small nano column still beats HVM5 on the few specialized cases shown, while HVM5 covers the wider benchmark set. A general runtime keeps enough representation to preserve DUP/SUP correlations without reifying every static piece of the program as a live graph node.

I left the HVM5 404 tab beside HVM4's ALO-LAM rule and wrote one note at the top of my scratch file: when the repository opens, trace the first DUP-LAM. For now, the cursor sits after that rule and the HVM5 tab still returns 404.