LightMachine

Yes! But first we want to implement some essential features, like full lambda support and some high priority optimizations. Once HVM is ready to support production software, we'll provide docs on how to best use it as a general compilation target. This will be announced in our Discord server: http://discord.higherorderco.com/

Absal is just an early implementation and experiment. It is written in JS and not meant to be a production-ready runtime and general purpose compilation target. HVM has that goal. That said, Absal is a great repo to study and learn the theory.

TBH, I'm somewhat of a Bitcoin maximalist too, which is kinda ironic since I hold no BTC; I guess the lack of expressivity of the network counters the big appreciation I have for its stable monetary policy and true decentralization. That's why, on HOC, I only accepted external funding under the conditions that Kindelia may not have a pre-mine - and am very glad to have found VCs that share this vision. (Kindelia is one of our internal projects, and is essentially Bitcoin with HVM-based contracts.)

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.

No, I mean that users should choose whether they use lazy cloning or immutable references when sharing arguments, just like you have the choice for several pointer types in Rust. I don't think compilers should make that decision, since I like to have full control over my program's runtime costs. When compiling a language like Haskell to HVM, we can just use references by default, and lazy cloning could be opt-in (using some newtype or similar).

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:

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

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:

    TimeComplexity(FnV1(N)) = 402 + 400*N rewrites
    TimeComplexity(FnV2(N)) = 1403 + 5*N rewrites

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'm working on improving my communication :(

Of course! Let me write a complete overview on the subject. Consider the following program:

    (Foo a b) = (If a (F b) (G b))

It is easy to note that Foo makes an unnecessary clone of the 'b' variable, since it is used in different branches. This could be avoided by adding a lambda, as follows:

    (Foo a b) = ((If a λb(F b) λb(G b)) b)

That is what I mean when I said that, in most instances, cloning can be avoided by adding strategic lambdas. Now, in some cases, such as issue #60, this won't be possible. Issue #60 isolates a situation where lazy cloning is necessarily quadratic. Here it is:

    (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))))

What this program does: first, it converts a list like [1,2,3,4,5] into a list of where each element stores its tail: [[2,3,4,5],[3,4,5],[4,5],[5]]. Then, it takes the head of each element, resulting in [2,3,4,5]. Notice it is a very inefficient, roundabout implementation of 'tail', which happens to be quadratic on HVM, and linear on GHC. In this specific case, this could be fixed by just writing Tail as usual:

    (Tail (Cons x xs)) = xs

It is worth pointing out that this is the case in all examples where HVM is sub-optimal! That is, there is always an alternative algorithm that avoids unnecessary cloning. That said, of course, in more complex programs, it will be impossible to identify sub-optimal situations and fix automatically (unless supercompilers become practical). As such, it is important for HVM to be able to handle these programs without quadratic slowdowns. To understand how that could be accomplished, let's first note that the culprit of the quadratic slowdown is the way HVM handles a non-linear variable. On the line below:

    (Tails (Cons x xs)) = (Cons xs (Tails xs))

HVM's default behavior is to assume that, by writing `xs` twice, you meant to do a lazy clone. In other words, the program above is compiled as:

    (Tails (Cons x xs)) =
      let [xs_a, xs_b] = xs.lazy_clone()
      (Cons xs_a (Tails xs_b))

In order to work, lazy cloning adds a "fan node" to the program's graph, which uses space. That means that, if you perform a lazy clone and immediately discard it, you'll be left with a "useless clone node" that still occupies memory. On the program shown on issue #60, we're essentially constructing an entire Tail and immediately dropping it with a call to Head, and we do that recursively, so, after enough calls, we have, in memory, the equivalent of:

    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

Notice how this expression takes a list, clones it several times, discards all the clones, and then immediately returns the original list. These accumulating useless let-expressions (i.e., cloning nodes) are the source of the quadratic slowdown. So, how do we fix it? The solution proposed on TOIFPL book is to add safe pointers, which would allow us to remove redundant clone nodes when safe. But there is a simpler approach: just do NOT make a lazy clone there, to begin with! While lazy cloning is great for things like higher order lambda compositions, in some cases, a good-old pass-by-reference would do a better job. In a future version of the HVM, we could have something like:

    (Tails (Cons x &xs)) = (Cons xs (Tails xs))

Where `&` would mean "pass by immutable reference", skipping lazy cloning entirely, and making this program linear, as it should.

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.

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).

Victor here, thanks for the kind words. Regarding issue #60;

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!).

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!

Well I can't disagree more. I feel like that's the best value I get for $20 among everything I pay, by at least 3 orders of magnitude. This thing does so much for me, I can't live without it anymore. When it is down I just log in on playground and pay for the API. It got to this point...

I really wanted an online Pokémon-like experience that didn't require having a console and that didn't suck

Even if that was the case, it'd still be massively useful because it would allow code to be transposed between languages idiomatically. For example, certain things like game engines were only implemented in very messy C++ code. If GPT understands how these libraries work, could it recreate all these game engines as cleaned up, elegant Haskell code?

I sort of agree, but it still amazes me that it can get the code is correct, even though I asked for a highly specific style (i.e., use of recursion, representing "None" as null, the format of the JSON, making local functions, etc.). So, even thought it has never seen that exact implementation, it still assembles a working function that just works. If it was just mixing up different code it recalled from memory, it would likely have a bunch of silly errors here and there that I'd have to fix manually, but no, it just works. That's what impressed me.

It managed to write, in one shot, a working λ-calculus parser, using a very specific programming style I asked it in JavaScript, and then translated it all to Python, including sarcastic, rhyming GLaDOS comments.

https://twitter.com/VictorTaelin/status/1635726202231988225

It also seems to be extremely competent at writing Agda types and proofs. We need some tool that highly integrates it with entire codebases, allowing for major refactors to be requested as a prompt. That would be groundbreaking (understatement of the year), specially if coupled with a strongly typed language that prevents it from accidentally breaking things up.

Can you post your attempts? Would love to see it

Neither a human can solve the halting problem. There is no evidence the brain does anything that a computer can't do.

𝓢𝓲𝓷𝓰𝓾𝓵𝓪𝓻𝓲𝓽𝔂 𝓲𝓼 𝓬𝓸𝓶𝓲𝓷𝓰

No? Order of magnitude conveys the notion of something being 100x bigger, at minimum. A lot can mean much less than that.

> If you are falling into despair then it's going to be superdeterminism for you.

If you don't believe in fairy tales nor assume the existence of a magic mysterious force named "free will" *

I mean that interpretations have practical implications because they're the only way to find the true laws of physics, which in turn has obviously applications. For example, if you believe in superdeterminism, and you obviously should, then that will save a lot of work researching dead ends (like multiverse stuff), which will make us find the correct algorithms faster.

Wait isn't that the common assumption? That the universe is just an algorithm and we're trying to figure which is it?

And it is absurd to say it has no direct practical implications. We still don't know all of physics, and part of the reason is precisely because we're stuck in the wrong mindset regarding how nature works. Only a better insight on the true nature of the universe can give us the correct mathematical models.

So Reddit mods shadow-banned me on /r/cryptocurrency for posting a technology? I wonder why they'd do that.

Well, I didn't think about that possibility. Perhaps that's what happened, yes. But why not just remove the post and let me know the reason? This is really sketchy to me. It feels like manipulation, but perhaps I'm being unfair.

Kindelia is a p2p decentralized computer I'm building. It is essentially a massively distilled version of Ethereum. It is massively simpler (<10k LOC), more efficient (up to 867x more SSTORE/second under the same usage level), and secure (since it supports Agda, Lean, Kind and other proof languages natively). It is completely decentralized, there is no pre-mine (in fact, there isn't even a currency). My post was 100% respectful and fair, I was just explaining the tech, no ads, no sales. I was banned because I posted a new tech.

This has to be exposed. If people can't create and propose new projects, then it has became a rigged game that only the elite can win. How is that better than fiat?

You can have virtual game worlds (like a MMORPG) that can't ever be turned off, by nobody. That means your items will last forever. 50 years from now, your sword will still be on your backpack. Can't say that for company-hosted MMORPGs like World of Warcraft, because these companies might go bankrupt, close servers, update items, etc. Not a cure-the-cancer colonize-mars hype level, of course, but it is still an interesting neat thing you can do with blockchains.

> Whenever Ruby throws, it allocates 10k of memory and fills it with all sorts of information for debugging - including a full stack trace. And it was doing this work in the background every time someone iterated through an array.

Jesus

They're inexcusably awful. I still don't know why it is like that. Haskell gets hard things right and easy things terribly wrong.

Looks good. I'll keep that in mind and let you know if we write such a benchmark. Opening an issue would be helpful to remind us!