Higher-Order Virtual Machine (HVM)
github.com
github.com
https://wiki.xxiivv.com/site/interaction_nets.html
If someone is looking for a graphical playground to experiment with interaction nets, here's Sylvain Lippi's InTwo(gtk):
https://github.com/max22-/intwo
Anyone looking to better understand linear logic in the context of IN ought to have a look at Victor's Absal:
https://github.com/VictorTaelin/abstract-algorithm
Someone below linked to Baker's excellent linear lisp paper(psi-lisp), I'd like to augment this recommendation with Linear Completeness theory of combinators:
[1] https://www.semanticscholar.org/search?q=typed%20assembly%20...
namely, Greg Morrisett and Neal Glew's work
https://www.semanticscholar.org/author/J.-G.-Morrisett/14364...
https://www.semanticscholar.org/author/MorrisettGreg/1643921... (semantic scholar incorrectly thinks there are two Greg Morrisetts)
In general though, I think we should move away from procedural instructions towards "interactional" instructions. HVM's AST can be seen as an assembly language with high-level instructions like LAM-APP (lambda application) and FUN-CTR (pattern-matching), and that's possible precisely because beta reduction is O(1) on interaction nets. A hardware with HVM's interactional instructions could make let us break out of the Von Neumann bottleneck and make processors much faster. Here is a table of HVM's core instructions:
.-----------------------------------------------------.
| Opcode | Effect | Cost |
|-----------|---------------------------------|-------|
| APP-LAM | applies a lambda | 2 |
| APP-SUP | applies a superposition | 4 |
| OP2-NUM | operates on a number | 2 |
| OP2-SUP | operates on a superposition | 4 |
| FUN-CTR | pattern-matches a constructor | 2 + M |
| FUN-SUP | pattern-matches a superposition | 2 + A |
| DUP-LAM | clones a lambda | 4 |
| DUP-NUM | clones a number | 2 |
| DUP-CTR | clones a constructor | 2 + A |
| DUP-SUP-0 | clones a superposition | 4 |
| DUP-SUP-1 | undoes a superposition | 2 |
| DUP-ERA | clones an erasure | 2 |
|-----------------------------------------------------|
"be up to exponentially faster than alternatives" – hmm
"Interaction Net, which supersedes the Turing Machine" – Interaction Net link points to a paper on Interaction Combinators. And talking about superseding Turing machines is embarrassing – do you have Oracle powers? (https://en.wikipedia.org/wiki/Oracle_machine)
"set to scale towards uncharted levels of performance" – that's just a bit cringy
I've come across claims of no GC needed and I don't buy it unless in restricted domains, and it would be nice to have a link towards what you mean by 'beta optimality'. I would like to see the sort benchmark being done something realistic (recursive bubble sort, the two words together don't look good). Also automatic parallelism..., Immutability apparently for free, everything higher-order, it seems you hit a lot of holy grails in one go. Rather too many for me to feel comfortable.
The FAQ by contrast is a whole lot more reasonable and upfront, perhaps be careful about overselling yourself?
Nonetheless, I eagerly await its future.
https://github.com/inpla/inpla/blob/main/Gentle_introduction...
Hopefully once the full LC is supported, we can try to make an STG-to-HVM-language translator.
With Rust, the type system guarantees safety and predictable runtime as well. I don't see how any model that doesn't have linear / affine typesystem implemented and exposed to the programming language give me the same guarantee.
https://github.com/HigherOrderCO/HVM/issues/167
I discuss how HVM is able to perform deforesting, one of the core techniques that made GHC so fast, "for free" at runtime, without being explicitly hardcoded. That is great, but the point I'd like to make is how I show that: by measuring the 'rewrite count' of a program with HVM's '-c' flag. It shows you how many rewrites a program evaluation took. Since each rewrite is a constant time operation, this gives us a very precise metric of the complexity of a program.
On the issue above, I implemented two versions of the same function, and measured their rewrite counts. Here are the tables:
Fn V1
N | rewrites
- | --------
0 | 402
1 | 802
2 | 1202
3 | 1602
4 | 2002
5 | 2402
6 | 2802
7 | 3202
8 | 3602
9 | 4002
Fn V2
N | rewrites
- | --------
0 | 1403
1 | 1408
2 | 1413
3 | 1418
4 | 1423
5 | 1428
6 | 1433
7 | 1438
8 | 1443
9 | 1448
TimeComplexity(FnV1(N)) = 402 + 400*N rewrites
TimeComplexity(FnV2(N)) = 1403 + 5*N rewrites
https://reader.elsevier.com/reader/sd/pii/S0890540197926432
It's funny, that as a BTC maxi I'm not fond of new tokens (like Cardano) being created, but the work they are funding are exceptional (my favourite is Vitalik funding a lot of longevity science, which would be the job of the governments, but they don't do anything about it).
Some more questions:
- Are you planning GPU backends? (emitting parallel C code and using CUDA / OpenCL compilers, like how Tinygrad does
- Can the code be used as a more efficient Jax / PyTorch compiler in the future? AI code is functional, though the building blocks (basic instructions, register, cache sizes, memory bandwidth) are the main optimization criteria
To address your questions:
Yes, we have plans for GPU backends. In fact, I have even written a working prototype some time ago! It reduces λ-terms on the GPU using the same rules as HVM, with all the locks and atomics in place, and it seems to achieve a near ideal speedup, even with thousands of nVidia cores:
https://gist.github.com/VictorTaelin/e924d92119eab8b1f57719a...
That said, it is still just a single-file prototype. Sadly, we couldn't include a GPU backend on this funding round, but it is definitely something we'll be investing in a future, specially if we manage to grow as a company. Imagine writing pure Haskell functions and they run in thousands of GPU cores with no efforts? Pure functional shaders, physics engines...
Regarding PyTorch, I don't think HVM would be more efficient than it for ML, because PyTorch is already maximally optimized to use GPUs to their limit. HVM should be seen as a way to run high level programs in a massively parallel fashion without needing to write low level CUDA code yourself, but it won't outperform manually optimized CUDA on GPUs. That said, I do believe interaction net based processors would greatly outperform GPUs by breaking the Von Neumann bottleneck and unifying memory and computation in billions of nano-interaction-cores. I do believe such architecture could one day empower AI and make our LLMs and RNNs much faster.
I took a quick look at the HVM runtime and can vaguely make out the shape of the memory and code that reduces terms. While it's cool to have a computational model that evaluates everything only once and avoids duplicating computation, if it does not compile programs to machine code to exploit hardware, then the single-core performance will be worse than C/C++/Rust.
Something that generates a few machines instructions in C/C++/Rust requires reducing a graph of terms - many CPU instructions for each reduction and many memory accesses that may have poor locality.
Is the idea that programs contain enough parallelism that is out of reach of human programmers so that HVM will make up for the single-core performance drag through parallelism?
Maybe I'm missing what the HVM compiler does?
Maybe hardware acceleration with FPGAs or ASICs could be applied?
In other words, can this beautiful and elegant computational model be implemented with efficiency that matches C/C++/Rust?
The FAQ mentions that every reduction rule can be compiled to machine code in theory. That's the core of what I'm asking - can reduction be implemented efficiently? I suspect it's not enough to have fast reduction rules, because that still requires a runtime that spends CPU cycles and memory accesses on reduction housekeeping. To be fast you need to minimize explicit reduction at runtime because that's not what CPUs are good at.
I guess an aggressive HVM compiler would find sub-programs that can be treated as leaf nodes and replaced entirely with compiled machine code. The machine code doesn't use interaction nets but it computes an equivalent result to the interaction net. This doesn't mean that reduction and interaction nets aren't used, they still serve a purpose for lazy evaluation and parallelism at higher levels of the program. The compiler would have to figure out where to draw the line between the high-level reduction runtime and the leaf nodes.
Anyway, this is just what comes to mind. I don't really know how HVM works, but thanks for sharing it.
I've looked up Victor Taelin and his HighOrderCo company that supposedly just raised $4.5M. So here we have this Brazilian guy who graduated university in 2017, and I don't mean that in a bad way. It's just a fact, a data point. Fresh ideas are always welcome. From his Twitter feed seems to be deeply into the crypto space. He is over- or at least heavily upselling this HVM project as the future of computing. Lots of fuzz about interaction nets and linear logic and that this is the next thing after Turing Machines and Lambda calculus. Ok, strong claims. It makes me a tad suspicious though. Outperforming GHC? Running a new chain that's not a chain so it's not a crypto currency, but somehow it's a chain, but it's formally verified, hm, ok. And how can he strongly claim this to be the superior thing if he just announced how to model complex numbers in his HVM project, and that GPT-4 helped him get this insight? I'd have expected Clifford Algebras to be basic knowledge for everybody working in this space.
I'm only superficially familiar with ETH, with Haskell's GHC, with Rust, with HOTT. But, I'd like to hear from people who know more than I do, and who are not already obvious fanboys of HighOrderCo with submarine PR interests -- how much weight should I put into this? Is it worth reading about, getting my head busy? I've spent an hour now trying to check up on things, but apart from a lot of fluff and quite a lot of technical jargon that went above my head, I'm left confused.
Is there something or is this just supposed to confuse me to get into the next scam?
Edit: Just to add to this. https://news.ycombinator.com/item?id=35344514 discusses an article written about the underlying tech. It's a terrible article on the level of a newcomer to programming who doesn't know much about functional programming and even admits as much. Victor Taelin comments with "Very well written and beautiful article." This must be a scam. I'll stop wasting my time on this until somebody manages to convince me otherwise.
I do notice Victor's tendency to be hyperbolic and defensive, which is quite unfortunate, and I don't know or care much about the blockchain that Victor is also running. (By the way, I think that Victor's real name is probably Victor Maia rather than Taelin, as you can corroborate from a number of sources; it seems Taelin is just his handle on Github. It seems that Victor used to work at Ethereum Foundation with the title of Researcher https://bobsummerwill.com/ethereum-foundation-people/?)
On the other hand, the computational model that Victor's HVM is built on was invented by Yves Lafont, and strongly inspired by Jean Yves Girard (who is known for Linear Logic, Girard's paradox, and System-F (of which, according to Wikipedia "forming a theoretical basis for languages such as Haskell")). I can assure you that Lafont and Girard are logicians of the highest caliber, and indeed the promises that HVM intends to fulfill are the same notions envisioned by Girard and computer scientists working on Geometry of Interaction and Interaction Nets. If you spend a few minutes to consider the case on the README where HVM claims to outperform GHC (e.g. regarding Lambda Multiplication), it should not be hard to understand why it is possible in certain cases for HVM to outperform essentially anything else, and the potential that improvements in computational models can bring.
In any case, Victor has indeed put a very promising computational model to serious optimisation, and that alone is worth earnest commendation. Reading in the details on HVM will make it clear that although it works today, it is still very much a prototype in-progress. Personally, I think the computational challenges that still need to be tackled to bring Interaction Nets to life remain intractable (as do Asperti and Guerrini, in IIRC chapter 10 of The Optimal Implementation of Functional Programming Languages; Victor mentions basing his implementation on Asperti and Guerrini's work, which makes it surprising that Victor is surprised that optimal reduction has edge cases), but any serious effort in this direction is badly needed and should probably be encouraged. If VCs are putting their money behind bringing Girard's ideas to popular imagination, then perhaps for once they are doing good.
As is well known in functional programming circles, mutation and non-referentially transparent operations make systems non-composable and incomprehensible. Pure, composable computation can generally be roughly modelled as terms in lambda calculus. However, elegant as lambda calculus may be as a computational model for computer scientists, to a rough approximation, CPU instructions resemble more of Turing machines. To a very rough approximation, we can take each CPU instruction to cost O(1) time, but on the other hand, lambda reduction takes a much more complex and variable cost depending on your term and reduction strategy, and is highly non-local. The potential of Interaction Nets lies in part, in allowing evaluation of lambda terms in essentially O(1) time.
Of course, Linear Logic reveals that many other facets regarding the efficiency of term evaluation are also deeply intertwined, and besides new solutions to evaluation steps and time-cost, Interaction Nets simultaneously act in a way which is local (allowing embarrassing parallelisation, and thus the whole possibility of HVM's GPU backend for arbitrary computation, albeit I believe, in progress) and also allows automatic erasure of unnecessary terms in large classes of terms (automatic garbage collection).
Together, the problems that Interaction Nets solve seem to altogether make the tradeoff between comprehensibility and efficiency an unnecessary choice.
I've noticed HVM since February last year and was quite convinced that they were really up to something; however now that I've gone through a pile of papers on Linear Logic and the book which HVM is based on (The Optimal Implementation of Functional Programming Languages, Asperti and Guerrini, https://www.amazon.co.jp/-/en/Andrea-Asperti/dp/0521621127), I believe that among other things, the issue presented here https://github.com/HigherOrderCO/HVM/issues/60 is really a fundamental blocker to serving as a general purpose runtime, which it appears HVM attempts at.
Fundamentally HVM is an impressively optimised implementation of Symmetric Interaction Combinators, a variety of Interaction Net. Symmetric Interaction Combinators is not related to lambda calculus in a trivial way, and thus as noted in the README, HVM does not 'support' the full Lambda Calculus. In a vast majority of cases the HVM approach really does simply evaluate lambda terms at impressive speed, but the failure cases are quite tricky to handle, in that they will fail silently, simply evaluating the term incorrectly. This issue however, is acknowledged in the README and can be tackled by the method described there, or by type-checking for these 'failure' cases https://github.com/HigherOrderCO/HVM/discussions/97.
The issue mentioned in #60 however, seems to be quite fundamental - HVM makes lambda evaluation fast by implementing lambda evaluation in terms of Symmetric Interaction Combinators and making sure each operation of SIC evaluates in constant time. This works in most cases, but as acknowledged in Asperti and Guerrini, in some cases the SIC representation of lambda terms simply become themselves very (exponentially) large. Victor appears to acknowledge that he is simply building a practical counterpart upon the theory as cited from Asperti and Guerrini, citing Asperti and Guerrini's 'safe rules', which has not yet been implemented, as his plan to prevent very large representations of lambda terms from occurring, but Asperti and Guerrini themselves acknowledge that their rules are probably incomplete. Crucially, these terms appear to show up in regular functional programming folds.
The promise of HVM is that we have finally found a way to naturally implement the parallelism inherent in pure lambda terms, without special annotation or extra accommodation for the runtime. As it stands, HVM still falls short of the lofty dream.
Short answer: this is true, but isn't a fundamental limitation and will be addressed in the future.
Long answer: this was quite a surprise to me back then, as it defies my understanding of "optimal", and was quite disappointing, but I learned a lot since. My current take is that, yes, some terms are quadratic on HVM while they are linear on the GHC, but that isn't due to some "catastrophic incompatibility", but just an inherent limitation of sharing-by-lazy-duplication. That said, as a practical runtime, HVM is not restricted to have only one way to share data. Rust, for example, has several ways: `&`, `&mut`, `Box`, `Rc`, `Arc`, `Cell`, `RefCell`, `Mutex`, `RwLock`, `* const T`, `*mut T`. We will add alternative pointer types to address this issue. That said, first we want to get the pure version completely polished, before moving into these optimizations. Meanwhile, it is worth noting that it is easy to fix these quadratic functions by adding strategic lambdas to avoid unnecessary cloning. This will make them linear again, so a functional language compiling to HVM properly wouldn't have any case where it underperforms GHC asymptotically (and would have several cases where it outperforms it!).
Indeed, if one were to figure out how to strategically add appropriate mechanisms to share data, perhaps the issue can be solved. It seems a highly nontrivial problem - but perhaps it would have taken someone brave as you to tackle it head on.
I can only hope that such strategic sharing could be solved and formalised - if we only had that together with HVM, effortless parallelism just feels like it could be within reach.
(I wonder if how the call-by-value linear logic translation compares with the call-by-name translation in terms of interaction nets, IIRC it should result equally in an optimal evaluator)
(Foo a b) = (If a (F b) (G b))
(Foo a b) = ((If a λb(F b) λb(G b)) b)
(Gen 0) = Nil
(Gen n) = (Cons n (Gen (- n 1)))
(Sum Nil) = 0
(Sum (Cons x xs)) = (+ x (Sum xs))
(Tails Nil) = (Cons Nil Nil)
(Tails (Cons x xs)) = (Cons xs (Tails xs))
(Heads Nil) = Nil
(Heads (Cons x xs)) = (Cons (Head x) (Heads xs))
(Head Nil) = 0
(Head (Cons x xs)) = x
Main = (Sum (Heads (Tails (Gen 1000))))
(Tail (Cons x xs)) = xs
(Tails (Cons x xs)) = (Cons xs (Tails xs))
(Tails (Cons x xs)) =
let [xs_a, xs_b] = xs.lazy_clone()
(Cons xs_a (Tails xs_b))
let [_, xs0] = xs.lazy_clone()
[_, xs1] = xs0.lazy_clone()
[_, xs2] = xs1.lazy_clone()
[_, xs3] = xs2.lazy_clone()
...
[_, xs{N}] = xs{N-1}.lazy_clone()
in xsN
(Tails (Cons x &xs)) = (Cons xs (Tails xs))
In short, the culprit for the quadratic slowdown is merely the fact that HVM automatically inserts a ".lazy_clone()" whenever you use a variable more than once, but there is no inherent incompatibility between interaction nets and good-old pass-by-reference, so HVM will have different pointer types that allow a programmer to implement functions like Tails that behave like they would on GHC, without any associated slowdown.
The case of erasing nodes after duplication 'unnecessarily' must be handled and cannot be dismissed - being much of the core use case of lazy evaluation.
From your breakdown it suggests that compilers to HVM use some heuristic which uses `&` immutable references on most data-like nodes, and lazy duplication on code-like nodes. I'm quite sure that still doesn't solve the issue of unnecessary duplications in the general case, but it does seem plausible that such measures suffice to slice the Gordian Knot in practice, similar to how you eliminated the 'oracle' with your superposition resolution - to very practically sidestep the uncommon, complicated case. Indeed, the distinction between code-like nodes and data-like nodes dictates very much of their behaviour during reduction, whereas in much of PLT literature and pure interaction nets, every node is 'code-like'.
I'm not sure if this is good enough in practice, if as I believe, HVM is meant to be a compiler target; I fear that good heuristics may not be enough, where the 'unnecessary' erase-after-duplicates arise from complex code paths, and may perhaps become apparent intermittently (but catastrophically) or only be clear on inspecting compilation output.
Looking forward to more of your work!
This looks like a really cool idea, and I'd love to see a GHC backend for it.
It might also be nice to have a brief explanation if an interaction between without just linking to a big theory paper.
[0] https://github.com/VictorTaelin/abstract-algorithm
eta: I only now notice that Victor Taelin is the author of both packages.
My understanding is that while parallelism (actually executing instructions simultaneously) is a property of the runtime, it depends upon concurrency (the separation of computations as independent) which is always something that has to be specified in the program source code.
Erlang has a similar property of "scaling with core-count for free" provided you write your program with a prodigious use of processes (which Erlang makes very easy and idiomatic). How is it that HVM is able to identify independent computations?
I admit to being only passingly familiar with Haskell-style FP, so perhaps the answer to my question is obvious.