Hasnain says:

This is an amazingly well written piece of technical content. I now have another book and language to add to two extremely long lists. The author takes one key intuition all the way and gets some amazing results from it.

“HVM doesn't need a global, stop-the-world garbage collector because every "object" only exists in one place, exactly like in Rust; i.e., HVM is linear. The catch is that, when an object needs to be referenced in multiple places, instead of a complex borrow system, HVM has an elegant, pervasive lazy clone primitive that works very similarly to Haskell's evaluation model. This makes cloning essentially free, because the copy of any object isn't made in a single, expensive pass, but in a layer-by-layer, on-demand fashion. And the nicest part is that this clone primitive works for not only data, but also for lambdas, which explains why HVM has better asymptotics than GHC: it is capable of sharing computations inside lambdas, which GHC can't. That was only possible due to a key insight that comes from Lamping's Abstract Algorithm for optimal evaluation of λ-calculus terms. Finally, the fact that objects only exist in one place greatly simplifies parallelism. Notice how there is only one use of atomics in the entire runtime.c.

This was all known and possible since years ago (see other implementations of optimal reduction), but all implementations of this algorithm, until now, represented terms as graphs. This demanded a lot of pointer indirection, making it slow in practice. A new memory format, based on SIC, takes advantage of the fact that inputs are known to be λ-terms, allowing for a 50% lower memory usage, and letting us avoid several impossible cases. This made the runtime 50x (!) faster, which finally allowed it to compete with GHC and similar. And this is just a prototype I wrote in about a month. I don't even consider myself proficient in C, so I have expectations for the long-term potential of HVM.

HVM's optimality and complexity reasoning comes from the vast literature on the optimal evaluation of functional programming languages. This book, by Andrea Asperti and Stefano Guerrini, has a great overview. HVM is merely a practical, efficient implementation of the bookkeeping-free reduction machine depicted on the book (pages 14-39). Its high-order machinery has a 1-to-1 relationship to the theoretical model, and the same complexity bounds, and respective proofs (chapter 10) apply. HVM has additional features (machine integers, datatypes) that do not affect complexity.”

Posted on 2022-02-07T05:51:31+0000