I've been following the work you've been doing for a while now, and the culmination of all your progress for the past few years toward HVM, has been very inspirational. Keep up the good work, and best of luck with HighOrderCo. If anyone, reading HVM's and Inpla's gentle introductions to Interaction Nets, is looking for an overview of Lafont's papers and Sato's implementation designs, you might enjoy:
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:
Author here! Thanks for posting :) Just want to make a brief note here that we raised a 4.5m seed round to found a tech startup, the Higher Order Company, to work on the HVM. Our goal is to improve the runtime, the Kind language, and eventually build our own hardware. There are already several cool ideas on the pipeline, so expect exciting news and massive improvements soon!
Yes, starting next week or so! We'll be looking for engineers that have skills relevant to our projects, including compilers, low-level assembly optimization, functional programming, type theory, parallel computing, and so on. Right now, we're quite busy with incorporation and bureaucracy, but you should see job postings in our to-be-released landing page (higherorderco.com) soon. Meanwhile, I answer DMs on Twitter (@VictorTaelin) and Discord (VictorTaelin#2253).
This seems very interesting, and I like your FAQ where you get honest, but your intro almost put me off:
"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?
I agree with most of your points, we should definitely rewrite and tone down the README. The FAQ was written a few months after, due to that kind of negative reception. To address your points, note that by "superseding" the Turing Machine, I do not mean they can compute uncomputable functions! The meaning is that, while both are equivalent in terms of *computability*, Interaction Nets have improved *computational* characteristics, such as strong confluence and concurrency. This is a very technical aspect that is addressed on the paper I linked. Regarding not buying the claim of no GC needed, this is interesting, since this is a well stablished result: HVM is entirely linear, so it can avoid global GCs for the same reason as Rust. The difference is that HVM is more inherently high level, since its support for lambda is way more first-class than Rust's closures, which are comparably slow and almost guarantee borrow-checker hell.
(Also, exponentially faster is used on the technical sense here! Optimal evaluators can reduce some programs with linear time complexity, while conventional runtimes are exponential.)
Interesting, though I can’t help but feel that the tone of the first few paragraphs could be a bit more.. humble? Even if the underlying model is much better, you can’t really compare a complete project to one that is alpha. Real world complexities catch up in the later phase of bigger projects.
I've never heard of interaction nets (which just shows how overspecialized CS can be: I guess I have a PhD in PLT?); so... I wikipedia'd it up. I normally don't trust Wikipedia any further than I can throw it, but ... "interaction nets":
Inpla is a very interesting project that is more elegant than HVM in several regards (as it doesn't need to worry about functional programming!) and should be more known. I've added a link to it from the HVM's repo a few months ago.
One thing that I don't see addressed (and the main problem I had with Haskell) is the predictibility of runtime: if I change a function somewhere to be 2x slower by doing something differently can it have a much bigger than 2x difference in functions that use it?
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.
Predictability is one of the most exciting aspects of HVM, to me. That's because everything is linear, so time and space costs are completely measurable, in a way that resembles C, but even more profoundly. For example, in the following GitHub issue:
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:
From these numbers, we can tell V2 scales better than V1, without doing any benchmark. Not only that, but we're able to write explicit formulas for the runtime cost of each version:
Which means both are O(N), but V2 has a 80x smaller linear coefficient. This precision extends to memory and space too. This is why we're so excited to build Kindelia to apply HVM to the context of blockchain VMs, as this granular measurability isn't available on GHC, which is why Cardano can't use the Haskell compiler, and must resort to an interpreter, greatly affecting its throughput. Of course, this is just one of many the applications of the HVM.
I wish I could say that I understand you, but at least what you write is exciting enough for me to read the paper that you linked, as it looks simple enough even for me:
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
Readit News
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:
http://tunes.org/~iepos/joy.html#linear
"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://en.wikipedia.org/wiki/Interaction_nets
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:
From these numbers, we can tell V2 scales better than V1, without doing any benchmark. Not only that, but we're able to write explicit formulas for the runtime cost of each version: Which means both are O(N), but V2 has a 80x smaller linear coefficient. This precision extends to memory and space too. This is why we're so excited to build Kindelia to apply HVM to the context of blockchain VMs, as this granular measurability isn't available on GHC, which is why Cardano can't use the Haskell compiler, and must resort to an interpreter, greatly affecting its throughput. Of course, this is just one of many the applications of the HVM.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