LightMachine

It does that! There are no GC pauses on HVM's model. Compiling Haskell to it would be neat.

That isn't how it works. HVM threads work transparently, you don't need to think about them. The same data structure *can* be visible to multiple threads under some conditions, through cloning; for example, consider the following program:

    (Sum Nil        )  = 0
    (Sum (Cons x xs))  = (+ x (Sum xs))
    (Head (Cons x xs)) = x

    (Main x) =
      let xs = (Cons 1 (Cons 2 (Cons 3 Nil)))
      (Pair (Sum xs) (Head xs))

The result of this program is `(Pair 6 1)`. Since `Pair` is the topmost (root) node of the normal form, each of its elements will be computed in a separate thread. Because of that, the same `[1,2,3]` list will be accessed by each thread. But that's not actually a shared reference, because values only exist in one place; instead, the lazy cloner makes copies of the list, layer-by-layer, and sends these copies to the thread that will handle them.

Note that if the same expression was written in a deeper position of the normal form, it would be evaluated sequentially. This is what avoids the fine-grained parallelism issue. It also means that in many cases HVM will not be as parallel as it could, though! But when the parallelism kicks in, it is always productive.

> That is not always true. There’s some overhead to introducing parallelization so it’s not always worth it unless you have a big enough chunk of work.

This isn't fine-grained parallelism though! As I said, HVM spawns threads on to-be-evaluated redexes closes to the root of the program's normal form. So, either there is a significant speedup, or the program is sequential (or too small), and there is no speedup, but the overhead is minuscule, since a bounded, small amount of spawn() occurs. To be clear: there is no situation where HVM's parallelism will make the program significantly slower, which *does* happen if you use too many sparks on Haskell. That will never happen on HVM.

> But the other reason fine grained parallelism isn’t often worth it even if it can provide a speedup for a single computation:

Yep that's definitely a good reason. Thanks for sharing. (You can just run HVM in a single thread, though.)

> It’s very cool in a “wow that’s neat” kind of way, but, well we already have machine ints that are even faster

I couldn't disagree more. Just because I used integers as an example, which happens to be optimized, it means an entire optimization technique isn't interesting? This applies to every data structure that can be defined algebraically.

> My other question - it seems like this approach requires giving up on separate compilation?

Compiling a function in isolation is fine, why wouldn't it be? Not sure I get it.

I don't think the authors are focused on engineering matters; they're researchers after all. But that's just my guess. Also, there is an obsession with covering the full λ-calculus, which the abstract algorithm doesn't. A lot of energy has been put in that. I think this is just wrong. Rust has severe limitations on how you can write lambdas. HVM has some, which seldom occur in practice.

Regardless, some people did try implementing this in practice, dozens of times, including myself. It just wasn't that fast except for these cases where the asymptotics are superior. A naive implementation just stores graphs/edges on memory, but most of these edges are redundant. For example, a lambda doesn't need to point to its parent. By trying to turn the graph in a tree, I've ended up with SIC [0], which, once implemented efficiently, cut down memory and computation costs significantly. Doing so was tricky, specially because 1. the missing edges complicated the transversal; 2. some upward edges can't disappear (variables); 3. DUP nodes aren't part of expressions, they just "float", which was counter intuitive to get right. Finally, I learned to appreciate the fact that global rewrite rules are better than case-trees for recursive functions, since they greatly reduce the total rewrite count.

So, in short, my journey was:

1. Learn the abstract algorithm

2. Implement it naively as a graph

3. Optimize it by making trees whenever possible

4. Favor rewrite equations over case-trees

These steps lead to the design of HVM, which does fairly well in practice.

[0] https://github.com/VictorTaelin/Symmetric-Interaction-Calcul...

`dup a b = {x0 x1}` will just substitute `a` by `x0` and `b` by `x1`, no matter where `a` and `b` are. So, if you apply that, verbatin, to:

    (Pair λx0(λy0(Pair a c)) λx1(λy1(Pair b d)))

You get:

    (Pair λx0(λy0(Pair x0 c)) λx1(λy1(Pair x1 d)))

Does that make sense?

There aren't. Kind is more stable, is more JS-looking and less Haskell-looking, which makes it more practical IMO, has a super fast JS compiler and you can write React-like apps on it easily, but some work is needed to improve the type-checker performance when certain syntax sugars are used. The core's performance is superb, though.

Idris2, I can't comment much. All I know is that I envy its unification algorithm and synthesis features. Its syntax is more haskellish, if you like that. It seems less mature in some aspects, though. Very promising language overall.

Thank you!

I know it needs improvements, there is even a disclaimer in the top of HOW.md. I'll go over it and improve sentences like that in a future.

I do disagree with SPJ here, though. On HVM, you can have complete control over how the resources (both space and time) are used in your programs and algorithms. That is why it outputs the memory (space) and rewrites (time) cost of each program you run, and it is so precise you can even make formulas of how much memory and how many rewrites your functions will demand. You can absolutely have tight memory control in HVM, just like in C. Being lazy, high-level, etc. is NOT incompatible with that, I'd argue.

Andrea Asperti's only mistake was thinking he was wrong.

This is MIT licensed, so feel free to fork, use, edit and sell it without even notifying me. Now go ahead and get rich!

You mean, the whole project? Or just the runtime? The runtime has recently been ported to go by Caue F. He posted it in our Telegram: https://pastebin.com/0X0bbW8b

Perhaps you could team up?

I didn't want to be misleading, sorry. My reasoning was to just benchmark identical programs.

I personally think Haskell's approach to parallelism is wrong, though, since it demands in-code annotations to work. The problem is that the decision on whether an expression should be parallelized doesn't depend on the code itself, but on where the expression is used. For example, if `fib(42)` is the topmost node of your program's normal form, you always want to parallelize its branches (`fib(41)` and `fib(40)`), but if it is called in a deeply nested list node, you don't. That information isn't available on the code of `fib`, so placing "spark" annotations seems conceptually wrong.

HVM parallelizes by distributing to-be-evaluated redexes of the normal form among available cores, prioritizing these close to root. Here is an animation: https://imgur.com/a/8NtnEa3. That always seems like the right choice to me. After all, it just returns the same result, faster. I could be wrong, though. In which case you think parallelism isn't the correct choice? Is it because you don't always want to use the entire CPU? Would love to hear your reasoning.

> Like I get that it helps a lot if you’re doing multiplication with Church numerals…

This isn't about multiplication with Church numerals. Don't you find it compelling to write binary addition as "increment N times" and have it be as efficient as the add-with-carry operation? Making mathematically elegant code fast matters, and HVM does that. See the overview [0] for instance. Also, this allows us to have all the "deforestation" optimizations that Haskell applies on List with hardcoded #rewrite pragmas, for any user-defined datatype, which is also quite useful. There are certainly many uses that I'm not creative enough to think of.

[0] https://github.com/Kindelia/HVM/blob/master/HOW.md#bonus-abu...

That is really not true, but I do agree Haskell passes that impression, for the wrong reasons. I'm working hard to fix these misconceptions on HVM, Kind-Lang and related projects!

Since HVM is linear, adding some mutability would be completely fine and would NOT break referential transparency (because values only exist in one place!). So, we could actually have "pure mutable arrays". In order to make that mix up well with lazy cloning, though, we'd need to limit the size of array to about 16. But larger arrays could be made as trees of mutable 16-tuples. There was a post about it, but I can't find it right now.

> On a quick scan, it seems to be some more things than just `let`. One example would be `(Main n) = (Sum (Gen n))` should be closer to `(define Main (n) (Sum (Gen n)))` or similar.

Good point.

> Could even get rid of the parenthesis for arguments (`(n)` => `n`) and treating forms inside `define` the same as `let`.

No, because non-curried functions are a feature. If we did that, every function would be curried. Which is nice, but non-curried functions are faster (lots of lambdas and wasteful copies are avoided using the equational rewrite notation), so they should be definitely accessible.

I fixed the link. This is all part of the system described on the book, HVM is merely a very fast practical implementation. The additions (thinks like machine integers and constructors) don't affect the core.

Changing it to pure s-expressions would be easy though, I guess just `let` isn't following that rule? I do love the no-parenthesis lets though.

Yes! The fact HVM can apply a function 2^N times in N steps is still mind-blowing to me. I think solutions to important problems might come from exploiting this fact. Keep in mind you need to use some techniques for that to work. In special, there are 3 important rules. I've just written an overview here: https://github.com/Kindelia/HVM/blob/master/HOW.md#bonus-abu...

Author here.

HVM is the ultimate conclusion to years of optimal evaluation research. I've been a great enthusiast of optimal runtimes. Until now, though, my most efficient implementation had barely passed 50 million rewrites per second. It did beat GHC in cases where optimality helped, like λ-encoded arithmetic, but in more real-world scenarios, it was still far behind. Thanks to a recent memory layout breakthrough, though, we managed to reach a peak performance of 2.5 billion rewrites per second, on the same machine. That's a ridiculous 50x improvement.

That is enough for it to enjoy roughly the same performance of GHC in normal programs, and even outperform it when automatic parallelism kicks in, if that counts! Of course, there are still cases where it will perform worse (by 2x at most usually, and some weird quadratic cases that should be fixed [see issues]), but remember it is a 1-month prototype versus the largest lazy functional compiler in the market. I'm confident HVM's current design is able to scale and become the fastest functional runtime in the world, because I believe the optimal algorithm is inherently superior.

I'm looking for partners! Check the notes at the end of the repository's README if you want to get involved.

The reason for the syntax is that HVM aims to be a low level compile target, which sounds confusing because closures make it look very high level, but it should be seen as LLVM IR. It isn't meant for direct human use on the long term. Ideally it will be the compile target of languages like Haskell, Lean, Idris, Agda, Kind (my language) and others. As such, I just went for a syntax that simplifies and speeds up parsing, while still keeping it usable if you need to manually edit: there is no backtracking on this syntax.

VictorTaelin here. It won't show a speedup because you already optimized it to a low level algorithm manually! The point of that benchmark is to stress-test the cost of overwhelming abstraction. What is really notable is that addition by repeated increment on HVM performs as well as addition with a carry bit. The former is an elegant one-liner, the later is a 8-cases error prone recursive definition. The point is to show how you can often write highly abstract, elegant mathematical definitions, and it will perform as well as a manually crafted version, and that is very cool.

HVM is the ultimate conclusion to years of optimal evaluation research. I've been a great enthusiast of optimal runtimes. Until now, though, my most efficient implementation had barely passed 50 million rewrites per second. It did beat GHC in cases where optimality helped, like λ-encoded arithmetic, but in more real-world scenarios, it was still far behind. Thanks to a recent memory layout breakthrough, though, we managed to reach a peak performance of *2.5 billion* rewrites per second, on the same machine. That's a ridiculous 50x improvement.

That is enough for it to enjoy roughly the same performance of GHC in normal programs, and even outperform it when automatic parallelism kicks in, if that counts! Of course, there are still cases where it will perform worse (by 2x at most usually, but remember it is a 1-month prototype versus the largest functional compiler in the world). I'm confident HVM's current design is able to scale and become the fastest functional runtime in the world, because I believe the optimal algorithm is inherently superior.

I'm looking for partners! Check the notes at the end of the repository's README if you want to get involved.

Thank you! Sad this post got no traction. I wonder if Hacker News allows posting again in a future.

Speaking of the subject, if someone DOES want a credential and already knows a lot of CS, are there good online courses that provide sped up process? I have been programming since 20 years ago, am a lead developer at a large company, but have no degree. Sadly some companies like Google do require it to even consider submissions, so I wonder if I should enroll an online course just for the paper.

That isn't even necessary. I've been exploring GPT-3 for a while and it is completely incapable of any reasoning. If you enter short unique logical sentences like "Bob had 5 apples, gave 2 to Mary, then ate the same amount. How many apples Bob has left?" No matter how many previous examples you give it (to be sure it gets the question), it gets it wrong. It is simply incapable of reasoning about what is going on.

This mindset kills more people than Hitler. Have a good day.

You do not understand the situation. Breaking ECDSA would mean everyone gains access to everyone else's private keys. There is no recovery after that, because even if the network is updated to use a quantum-resistant scheme, how do you prove you're the owner of that BTC? And without a central party, who decides you're the rightful owner of your BTC, if 10's of other people insist they own it?

Well [Kind](https://github.com/uwu-tech/kind) has only one "axiom" (the lambda), so, I don't know? This is a really inspiring thought and I'm glad people are debating it for the content and not attacking Wolfram just because.

Mining is voting weighted by wasted CPU power. Stake is voting weighted by wealth. That's all, really.

Both are used to build decentralized networks, since they allow it to pick a random participant to order the previous X transactions (aka block), without being susceptible to sybil attacks. PoS is much less energy-hungry than PoW, but it has a problem: how do you distribute money fairly, to begin with? Which is why Ethereum started with a few years of PoW to only then shift to PoS. Pretty clever IMO.