15 ms·

High-order Virtual Machine (HVM): Massively parallel, optimal functional runtime

493 points by Kinrany 5y ago

AlexanderTheGr8 5y ago
Does anyone know how this affects people who write code in OOP-languages like C++/Java? The only time I have used a functional language is first year of college, and it was a pain.
tromp 5y ago
This looks pretty awesome, and holds much promise for the future. Optimal beta reduction has always seemed like something of theoretical interest only, but Victor has been working many years on making it more practical, which deserves a lot of respect. > HVM files look like untyped Haskell. Why not make it look exactly like Haskell? So that every valid Haskell program is automatically a valid Hvm program, while the reverse need not hold due to hvm being untyped. Instead the syntax looks like a mix of Haskell and Lisp, with parentheses around application, and prefix operators. I prefer the cleaner Haskell syntax. Some of the speedup examples look somewhat artificial: The exponential speedup is on 2^n compositions of the identity function, which has no practical use. It would be nice to show such a speedup on a nontrivial function. The arithmetical example uses a binary representation, but strangely uses unary implementation of operators, with addition implemented as repeated increment, and multiplication as repeated addition. Why not use binary implementation of operators? Does that not show a good speedup?
- salimmadjd 5y ago
  I totally agree on the syntax, Haskell is far cleaner. I’m not sure what the reasoning was here. I hope the author or others can shed some light.
  - capableweb 5y ago
    > I’m not sure what the reasoning was here. I hope the author or others can shed some light. From my point of view, the author almost made it into s-expressions, but decided not to go all the way, which (imo) would have been amazing and the "cleanest" (although I don't like using the term "clean" for code, it's so subjective). I'd like to have some light shed over the decision not to go all the way.
    - fithisux 5y ago
      Not very knowledgeable, does it mean it can be a foundation for a Scheme compiler?
      - deleted 5y ago
        [deleted]
    - klysm 5y ago
      Well we gotta have _some_ word for subjective quality.
      - dkarl 5y ago
        We do have "elegant," which to me means "intellectually ergonomic." Something can be "beautiful" while being totally intimidating and impossible for a human to work with, it can be "easy" despite wasteful complexity because it you can confidently work through the cruft, but "elegant" implies both beauty and ease, fitting naturally to our human mental capabilities without unnecessary detail.
    - deleted 5y ago
      [deleted]
    - LightMachine 5y ago
      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.
      - capableweb 5y ago
        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. Not sure the change would be as easy as you think, but happy to be proven otherwise ;) A `let` could assume un-even amount of forms in it and only evaluate the last one, using the other ones as bindings. Example from your README: (Main n) = let size = (\* n 1000000) let list = (Range size Nil) (Fold list λaλb(+ a b) 0) (define Main (n) (let size (\* n 1000000) list (Range size Nil) (Fold list λaλb(+ a b) 0))) Could even get rid of the parenthesis for arguments (`(n)` => `n`) and treating forms inside `define` the same as `let`.
  - sfvisser 5y ago
    My guess is the author just picked the simplest syntax to parse in order to demonstrate the tech. If it works and shows to be successful you can always write a GHC (or whatever) backend that compiles to this runtime. Maybe come up with some binary IL etc
    - hexo 5y ago
      Or write self-hosting GHC backend that works like HVM does. That would be very neat. For me, these projects (such as HVM) are great research stuff showing us how to do (or not do) things.
  - LightMachine 5y ago
    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.
    - conaclos 5y ago
      Is there some pages that compare Kind and Idris 2?
      - LightMachine 5y ago
        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.
    - The_rationalist 5y ago
- LightMachine 5y ago
  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.
  - tromp 5y ago
    Oh, you can write addition as repeated increment, and you get the efficiency of addition in binary? Wow; that certainly is impressive.
    - LightMachine 5y ago
      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-abusing-beta-optimality https://github.com/Kindelia/HVM/blob/master/HOW.md#bonus-abu...
      - giovannibonetti 5y ago
        > 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. Is it just me, or does that look similar to the Fast Fourier Transform (FFT) [1] speedup (against the regular Fourier Transform implementation)? [1] https://en.wikipedia.org/wiki/Fast_Fourier_transform https://en.wikipedia.org/wiki/Fast_Fourier_transform
        HelloNurse 5y ago
        What kind of similarity do you perceive? What analogue of Fourier transforms and of the involved algebraic structures can you find in heterogeneous graphs of constructors?
- divs1210 5y ago
  > I prefer the cleaner Haskell syntax. My God, this is written so matter-of-factly that it hurts. To me, Lisp is awesome BECAUSE of its uniform syntax! To me, Lisp is waaaaaay cleaner and always unambiguous! I guess what I'm saying is that it's subjective.
  - JonChesterfield 5y ago
    Lisp and Haskell are both easier to read than this syntactic hybrid of the two, but that might be familiarity
- chriswarbo 5y ago
  > Why not make it look exactly like Haskell? So that every valid Haskell program is automatically a valid Hvm program, while the reverse need not hold due to hvm being untyped. > I prefer the cleaner Haskell syntax. "Haskell syntax" is a pretty bad design in my experience. Firstly, it isn't just one thing: there's Haskell 98 and Haskell 2010, but most "Haskell" code uses alternative syntax from GHC extensions (lambda case, GADTs, type applications, view patterns, tuple sections, etc.). (Frustratingly, those extensions are often applied implicitly, via a separate .cabal file, which makes parsing even harder; plus lots of "Haskell code" is actually written as input for a pre-processor, in which case all bets are off!) GHC alone includes two separate representations of Haskell's syntax (one used by the compiler, one used by TemplateHaskell). Other projects tend to avoid both of them, in favour of packages like haskell-src-exts. I've worked on projects which manipulate Haskell code, and getting it to parse was by far the hardest step; once I'd managed to dump it to an s-expression representation the rest was easy!
Labo333 5y ago
Can someone point me to a reference explaining what beta reduction is?
- tromp 5y ago
  https://en.wikipedia.org/wiki/Lambda_calculus#%CE%B2-reduction https://en.wikipedia.org/wiki/Lambda_calculus#%CE%B2-reducti... Basically, beta-reduction is the single primitive that performs all computation in the lambda calculus. When you apply the function mapping x to M, to argument N, the result is M with all occurences of x replaced by N.
  - agounaris 5y ago
    Is there any practical example on this? Whats a common use casE?
    - opnitro 5y ago
      Any evaluation of a functional-based language is going to use this. Here's a simple example: Let's say I have a function `add1` `add1 = \x -> x + 1` (A function that takes a value `x` and then computes `x + 1` And then I write the program: `add1 2` If we want to evaluate this program, first we substitute the variable to get `add1 2` -> `(\x -> x + 1) 2` Then we perform "beta reduction" to get: `(\x -> x + 1) 2` -> `2 + 1` Then it's simple arithmetic: `2 + 1` -> `3` "The point" here is to have formal rules for defining what a computation means. This helps with writing proofs about what programs do, or what is possible for programs to do. For example, say I have a simple program with static types. I might want to prove that if the programs type checks, type errors will never occur when you run the program. In order to do this proof, I have to have some formal notion of what it means to "run the program". For a functional language, beta reduction is one of those formal rules.
      - tsimionescu 5y ago
        I will note though that in the actual lambda calculus there is no "+", "2" or "1" - it's functions all the way. 1 is typically defined in the Church encoding as \f -> \x -> f x. Addition is \m -> \n -> \f -> \x -> m f (n f x). Finding the Church encoding of 2 is left as an exceecise. We can then use beta reduction to compute 1 + 1 by replacing m and n with 1: 1 = \f -> \x -> f x (\m -> \n -> \f -> \x -> m f (n f x)) 1 1 =>beta \f -> \x -> 1 f (1 f x) \f -> \x -> 1 f x = (\f -> \x -> f x) f x =>beta 1 f x = f x \f -> \x -> 1 f (1 f x) <=> \f -> \x -> 1 f (f x) (\f -> \x -> f x) f (f x) =>beta \f -> \x -> f f x - the Church encoding of 2. This is how computation using beta reduction only looks like.
dean177 5y ago
Readers will find HOW.md interesting too: https://github.com/Kindelia/HVM/blob/master/HOW.md https://github.com/Kindelia/HVM/blob/master/HOW.md
- cwillu 5y ago
  “In other words, think of HVM as Rust, except replacing the borrow system by a very cheap .clone() operation that can be used and abused with no mercy. This is the secret sauce! Easy, right? Well, no. There is still a big problem to be solved: how do we incrementally clone a lambda? There is a beautiful answer to this problem that made this all possible. Let's get technical!” Every third paragraph feels like the autogenerated flavour text gibberish of a kerbal space program mission description.
  - mrpf1ster 5y ago
    I enjoyed it, you can clearly see the author is excited about explaining his work.
  - throwaway17_17 5y ago
    I don’t know that I would go as far as you did, but the writing style is a little bit to hyperbolic or maybe just to rhetorical/conversational for my tastes.
  - LightMachine 5y ago
    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.
  - hnlmorg 5y ago
    As an author of a language myself and going through the process of documenting it, let me assure you that writing technical docs is several orders of magnitude harder than writing comments on HN. And not only is it hard but it is also extremely time consuming and far less interesting than writing code too. Yet it needs to be done. To that end, the value of community support in writing documentation can never be overstated. So if you have any issues specific issues with his documentation then I'm sure the author would welcome a pull request.
jsnell 5y ago
This had a Show HN a few days ago: https://news.ycombinator.com/item?id=30152714 https://news.ycombinator.com/item?id=30152714
fulafel 5y ago
The submission title says "optimal", the README says "beta-optimal", what do they mean in this context and are they true?
- opnitro 5y ago
  "Optimal" in this context means it never repeats the work of beta reduction when it doesn't have to. Ie, evaluating `(\x -> x + x) (2 * 2)` only evaluates `2 * 2` once.
  - rowanG077 5y ago
    Why is this special? Doesn't that mean GHC is beta optimal since afaik it stores thunks to computations.
    - opnitro 5y ago
      GHC is not beta optimal, due to some complications around what happens when a closures are created. (This is `HOW.md` claims)
  - astrange 5y ago
    That's not optimal on real machines; it's often faster to recalculate x*y than to cache it. In general this "optimal" strategy seems to assume infinite memory that's all accessible at the same speed.
    - opnitro 5y ago
      "Beta Optimial" != Fastest Execution strategy for all kinds of code. Just defining the term, not arguing about it's engineering application.
      - astrange 5y ago
        The project certainly says it has "drastically improved efficiency" and "uncharted levels of performance". I don't think "massively parallel" is all that good for performance either, because battery life is part of that.
deleted 5y ago
[deleted]
carterschonwald 5y ago
The fellow behind this has been hammering at experiments around so called optimal reduction strategies for a while! As another commenter’s remarks imply; some of the so called benefits for what are called optimal reduction strategies are limited to efficiently manipulating data structures that are represented by lambdas. And that’s also probably why this is Untyped. Makes it easier to embed / support such an encoding
- throwaway17_17 5y ago
  Agreed, but the reference he makes to the symmetric interaction calculus blog post seems to at least have basis in sound logic/semantic principles. I haven’t read the whole post, but I am at least willing to give it a chance.
  - carterschonwald 5y ago
    Linear logic inspired ideas are always great
yewenjie 5y ago
So many new programming languages coming up with clever features that makes me wish I could mix and match their core features while using libraries from more popular languages. Up and coming Languages I am excited about - 1. Roc - https://www.youtube.com/watch?v=vzfy4EKwG_Y https://www.youtube.com/watch?v=vzfy4EKwG_Y 2. Zig - https://ziglang.org/ https://ziglang.org/ 3. Scopes - https://sr.ht/~duangle/scopes/ https://sr.ht/~duangle/scopes/ 4. Gleam - https://gleam.run/ https://gleam.run/ 5. Odin - https://github.com/odin-lang/Odin https://github.com/odin-lang/Odin 6. Koka - https://github.com/koka-lang/koka https://github.com/koka-lang/koka 7. Unison - https://github.com/unisonweb/unison https://github.com/unisonweb/unison
- arc776 5y ago
  Nim - https://nim-lang.org/ https://nim-lang.org/ Lets you mix and match other libraries with their native ABI as it compiles to C, C++, ObjC and JS + has excellent FFI.
  - metadat 5y ago
    What about support for using Golang or C# packages? That'd be handy. Interesting read about NIM- https://www.quora.com/Why-hasnt-Nim-Nimrod-become-as-popular-as-Go-Rust-and-Swift https://www.quora.com/Why-hasnt-Nim-Nimrod-become-as-popular... Key points: - Nim lacks official support to multiple inheritance or interfaces (as that in Java) or mixin (as that in Ruby). It feels uneasy when implementing common design patterns, which is important for middle to large-sized projects. - The error messages emitted from Nim compiler looks a bit obscure. Sometimes you have to guess or google to comprehend what really happens in your code. These seem like pretty good problems compared to common annoyances and caveats in many other languages.
    - arc619 5y ago
      TBF the reply in that link was written 4 years ago, before the language went 1.0 > Nim lacks official support to multiple inheritance or interfaces Multiple inheritance is a bit of a trainwreck IMO (see diamond problem). The language isn't designed around OOP, and is instead procedural with metaprogramming for extension. You get more bang for your buck this way, but for people with their head in inheritance it’s probably a shock.
afranchuk 5y ago
Really neat. I've been working on a lazy parallel language and so I read the "HOW" document closely to see the secret sauce. What's exciting to me is that, while I'm not familiar with the academia behind their decisions, it seems that I arrived at the same result with regard to their lazy clones: I realized early in the language that caching the eval results would make things really fast, and this caching ends up doing exactly what their lazy clones achieves! Of course one place I don't cache is in function application because the language is not pure (so we want side effects to occur again), but this makes me think it might be really good to derive which functions/subexpressions are pure and allow the cache to be retained through function calls for those. I'm gonna keep a close watch on this. I should probably read more white papers :)
- LightMachine 5y ago
  Thank you!
- chriswarbo 5y ago
  > I realized early in the language that caching the eval results would make things really fast, and this caching ends up doing exactly what their lazy clones achieves! Sounds similar to the evaluation model of the Nix expression language (the pure functional programming language used by the Nix package manager). It caches evaluation results, which (a) avoids re-computing identical expressions, and (b) allows some infinite loops to be detected. See https://www.researchgate.net/publication/222827743_Maximal_Laziness_An_Efficient_Interpretation_Technique_for_Purely_Functional_DSLs https://www.researchgate.net/publication/222827743_Maximal_L...
  - afranchuk 5y ago
    Thanks for bringing that up! I suspected that nix did that, but wasn't sure. This language is also a "task runner" (being used for build systems mainly), so it's not surprising that it behaves like nix does.
LightMachine 5y ago
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_rationalist 5y ago
  How does it compare to https://github.com/beehive-lab/TornadoVM https://github.com/beehive-lab/TornadoVM
  - HelloNurse 5y ago
    > TornadoVM accelerates parts of your Java applications on heterogeneous hardware devices such as multicore CPUs, GPUs, and FPGAs. So a HVM-like interpreter could be written in Java or variants thereof (instead of Rust), in order to take advantage of TornadoVM to run efficient lazy evaluation on exotic devices.
- auggierose 5y ago
  JFYI, the "This book" link on https://github.com/Kindelia/HVM/blob/master/HOW.md https://github.com/Kindelia/HVM/blob/master/HOW.md goes to a research gate page which has the wrong book for download (something about category theory). So, this dup primitive, is that explained in the book as well, or is this a new addition in your implementation?
CyberRabbi 5y ago
A problem with Haskell and with this is that they are inherently only suitable for batch processing. You cannot build interactive systems that have real-time requirements with these languages because how computation is done is not generally under control of the programmer. People attempt to program interactive systems with Haskell but then they spend most of their time adapting their program to GHC’s particular evaluation strategy. Usually the optimized program ends up convoluted and nothing like how Haskell code should look, additionally still with no guarantees on the run time.
- tromp 5y ago
  Would you say DOOM is interactive with real-time requirements? https://github.com/rainbyte/frag https://github.com/rainbyte/frag
  - CyberRabbi 5y ago
    The vast majority of the code in that repository is in the IO monad and uses carefully placed “!” eager evaluation annotations. Both facts only serve to reinforce my point that a programmer must have control over the way in which computations proceed to build interactive applications. Haskell does allow some level of control over this as I said but it ends up not looking like Haskell, it looks like C with funny syntax.
    - travv0 5y ago
      > The vast majority of the code in that repository is in the IO monad and uses carefully placed “!” eager evaluation annotations. Looking through that repository, I believe we have extremely different definitions of "vast majority."
      - CyberRabbi 5y ago
        Nearly everything in Render.hs is in the IO monad. That is a fact, not a subjective opinion. I point out those routines because they are the heart of the application.
gbrown_ 5y ago
I see the author is replying here so I just wanted to say I enjoyed following the Formality posts on your blog and updates on GitHub and hope there's time for more of that in the future. Wishing you all the best with this project! As an aside it may be a convenient reference if you laid out the history of Formality/Kind as I think a large portion of your target audience already knew about Formality. The rename gets a little lost in IMHO, at first glance at least.
deleted 5y ago
[deleted]
mountainriver 5y ago
Really awesome, any thoughts on autodiff?
fritzo 5y ago
Great work Victor, it's so encouraging to see Asperti & Guerrini's research receive engineering attention! Anton Salikhmetov also had some nice implementations [1] a few years ago. As I understand, even Andrea Asperti didn't believe his approach was practical [2] :) Any idea how hard it would be to extend with a nondeterminism operator, as in Plotkin's parallel or? (fork a computation and terminate if either branch terminates) [1] https://dblp.org/pid/49/4772.html https://dblp.org/pid/49/4772.html [2] https://arxiv.org/abs/1701.04240 https://arxiv.org/abs/1701.04240
- LightMachine 5y ago
  Andrea Asperti's only mistake was thinking he was wrong.
mikewarot 5y ago
Disclaimer: I'm just a Pascal programmer... so I didn't grok the nitty gritty of the lambda calculus, but I think enough to see where this is going. This evokes a similar feeling to when I learned that Lisp wasn't John McCarthy's target programming language. I began to wonder how powerful that intended language would have been, if everyone hadn't stopped at the bootstrap language. There is great power in what is shown, and I suspect even more power in what it enables. I look forward to see where this goes, there clearly could be another similar leap. Question: Does this mean it's possible to rework Rust to remove the accursed borrow checker? (I tried learning Rust, and stopped at the Borrow Checker, so I gotta ask)
- namibj 5y ago
  For the most part, Rust's borrow checker just serves to verify that non-`unsafe` code doesn't modify/deallocate memory that is still accessible through a different pointer (a reference , in Rust terms; actual (raw) pointers free of such implications can't be used for data access without `unsafe`). They further imply that they are non-NULL and their pointee is dereferenceable (no segfault; correctly aligned) and a valid bitpattern for the pointee type. These assumptions are provided to LLVM, allowing a bunch of optimizations already. Mutable references further guarantee `noalias`/`restrict`, as a mutable reference to some memory location implies no other references to that memory exist, an exclusivity enabling aggressive store-to-load forwarding and elimination of redundant stores. The non-NULL nature makes `Option<&T>` pointer-sized, so semantically nullable pointers have no memory cost and just force explicit handling of their NULL state when accessed (there are convenience method-syntax functions and `match` statements who's cases (patterns, in Rust terms) look like type constructors on the left side of a `=>` and have the inner values bound to the identifiers on the expression to the right of the `=>`). If a function itself returns an `Option`, `foo?` can be used to just unpack a `Some(bar)` and `return None;` on the nullable case. This syntax also works with `Result<T, E>` which allows conveying detailed errors (similar to exceptions, but with performance matching C's negative return codes instead of C++'s unwinding). References are written as `&T` for immutable ones and `&mut T` for mutable ones. Raw pointers are written as `const T` for immutable ones and `mut T` for mutable ones. These guarantees of no-mutable-shared-memory not guarded by explicit `Atomic` types (or concurrent datastructures (I count `Mutex` and `RwLock`)) carry semantic guarantees beyond what an auto-`.clone()` and/or GC can provide. I highly suggest you to try Rust again, but this time using non-lexical-lifetimes (NLL(s)), which shift the lifetime enforcement from simple lexical scope to a control-flow-graph based reachability. They lack the unintuitively-restrictive limitations particularly notable with loops, while still simplifying to abstract over combinatorial path explosion. BorrowChk is your friend, I promise. Just ask in e.g. the Community Discord if you're getting rejected for no good reason despite trying to understand/work around it's complaints. You're not really fighting it; it's more like a sparring partner than an enemy. Also, `.clone()` and `#[derive(Debug, Clone, Copy)]` are your friends when fighting BorrowChk.
FullyFunctional 5y ago
This is incredibly exciting and a tour-de-force. My immediate thoughts are on turning this into a hardware automaton, eg. an FPGA softcore like Reduceron. I see some interesting questions like how to handle user defined rewrite rules, but nothing insurmountable.
deleted 5y ago
[deleted]

493 points by Kinrany 5y ago

Does anyone know how this affects people who write code in OOP-languages like C++/Java? The only time I have used a functional language is first year of college, and it was a pain.

tromp 5y ago

This looks pretty awesome, and holds much promise for the future. Optimal beta reduction has always seemed like something of theoretical interest only, but Victor has been working many years on making it more practical, which deserves a lot of respect. > HVM files look like untyped Haskell. Why not make it look exactly like Haskell? So that every valid Haskell program is automatically a valid Hvm program, while the reverse need not hold due to hvm being untyped. Instead the syntax looks like a mix of Haskell and Lisp, with parentheses around application, and prefix operators. I prefer the cleaner Haskell syntax. Some of the speedup examples look somewhat artificial: The exponential speedup is on 2^n compositions of the identity function, which has no practical use. It would be nice to show such a speedup on a nontrivial function. The arithmetical example uses a binary representation, but strangely uses unary implementation of operators, with addition implemented as repeated increment, and multiplication as repeated addition. Why not use binary implementation of operators? Does that not show a good speedup?

salimmadjd 5y ago
I totally agree on the syntax, Haskell is far cleaner. I’m not sure what the reasoning was here. I hope the author or others can shed some light.
- capableweb 5y ago
  > I’m not sure what the reasoning was here. I hope the author or others can shed some light. From my point of view, the author almost made it into s-expressions, but decided not to go all the way, which (imo) would have been amazing and the "cleanest" (although I don't like using the term "clean" for code, it's so subjective). I'd like to have some light shed over the decision not to go all the way.
  - fithisux 5y ago
    Not very knowledgeable, does it mean it can be a foundation for a Scheme compiler?
    - deleted 5y ago
      [deleted]
  - klysm 5y ago
    Well we gotta have _some_ word for subjective quality.
    - dkarl 5y ago
      We do have "elegant," which to me means "intellectually ergonomic." Something can be "beautiful" while being totally intimidating and impossible for a human to work with, it can be "easy" despite wasteful complexity because it you can confidently work through the cruft, but "elegant" implies both beauty and ease, fitting naturally to our human mental capabilities without unnecessary detail.
  - deleted 5y ago
    [deleted]
  - LightMachine 5y ago
    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.
    - capableweb 5y ago
      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. Not sure the change would be as easy as you think, but happy to be proven otherwise ;) A `let` could assume un-even amount of forms in it and only evaluate the last one, using the other ones as bindings. Example from your README: (Main n) = let size = (\* n 1000000) let list = (Range size Nil) (Fold list λaλb(+ a b) 0) (define Main (n) (let size (\* n 1000000) list (Range size Nil) (Fold list λaλb(+ a b) 0))) Could even get rid of the parenthesis for arguments (`(n)` => `n`) and treating forms inside `define` the same as `let`.
- sfvisser 5y ago
  My guess is the author just picked the simplest syntax to parse in order to demonstrate the tech. If it works and shows to be successful you can always write a GHC (or whatever) backend that compiles to this runtime. Maybe come up with some binary IL etc
  - hexo 5y ago
    Or write self-hosting GHC backend that works like HVM does. That would be very neat. For me, these projects (such as HVM) are great research stuff showing us how to do (or not do) things.
- LightMachine 5y ago
  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.
  - conaclos 5y ago
    Is there some pages that compare Kind and Idris 2?
    - LightMachine 5y ago
      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.
  - The_rationalist 5y ago
LightMachine 5y ago
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.
- tromp 5y ago
  Oh, you can write addition as repeated increment, and you get the efficiency of addition in binary? Wow; that certainly is impressive.
  - LightMachine 5y ago
    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-abusing-beta-optimality https://github.com/Kindelia/HVM/blob/master/HOW.md#bonus-abu...
    - giovannibonetti 5y ago
      > 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. Is it just me, or does that look similar to the Fast Fourier Transform (FFT) [1] speedup (against the regular Fourier Transform implementation)? [1] https://en.wikipedia.org/wiki/Fast_Fourier_transform https://en.wikipedia.org/wiki/Fast_Fourier_transform
      - HelloNurse 5y ago
        What kind of similarity do you perceive? What analogue of Fourier transforms and of the involved algebraic structures can you find in heterogeneous graphs of constructors?
divs1210 5y ago
> I prefer the cleaner Haskell syntax. My God, this is written so matter-of-factly that it hurts. To me, Lisp is awesome BECAUSE of its uniform syntax! To me, Lisp is waaaaaay cleaner and always unambiguous! I guess what I'm saying is that it's subjective.
- JonChesterfield 5y ago
  Lisp and Haskell are both easier to read than this syntactic hybrid of the two, but that might be familiarity
chriswarbo 5y ago
> Why not make it look exactly like Haskell? So that every valid Haskell program is automatically a valid Hvm program, while the reverse need not hold due to hvm being untyped. > I prefer the cleaner Haskell syntax. "Haskell syntax" is a pretty bad design in my experience. Firstly, it isn't just one thing: there's Haskell 98 and Haskell 2010, but most "Haskell" code uses alternative syntax from GHC extensions (lambda case, GADTs, type applications, view patterns, tuple sections, etc.). (Frustratingly, those extensions are often applied implicitly, via a separate .cabal file, which makes parsing even harder; plus lots of "Haskell code" is actually written as input for a pre-processor, in which case all bets are off!) GHC alone includes two separate representations of Haskell's syntax (one used by the compiler, one used by TemplateHaskell). Other projects tend to avoid both of them, in favour of packages like haskell-src-exts. I've worked on projects which manipulate Haskell code, and getting it to parse was by far the hardest step; once I'd managed to dump it to an s-expression representation the rest was easy!

Labo333 5y ago

Can someone point me to a reference explaining what beta reduction is?

tromp 5y ago
https://en.wikipedia.org/wiki/Lambda_calculus#%CE%B2-reduction https://en.wikipedia.org/wiki/Lambda_calculus#%CE%B2-reducti... Basically, beta-reduction is the single primitive that performs all computation in the lambda calculus. When you apply the function mapping x to M, to argument N, the result is M with all occurences of x replaced by N.
- agounaris 5y ago
  Is there any practical example on this? Whats a common use casE?
  - opnitro 5y ago
    Any evaluation of a functional-based language is going to use this. Here's a simple example: Let's say I have a function `add1` `add1 = \x -> x + 1` (A function that takes a value `x` and then computes `x + 1` And then I write the program: `add1 2` If we want to evaluate this program, first we substitute the variable to get `add1 2` -> `(\x -> x + 1) 2` Then we perform "beta reduction" to get: `(\x -> x + 1) 2` -> `2 + 1` Then it's simple arithmetic: `2 + 1` -> `3` "The point" here is to have formal rules for defining what a computation means. This helps with writing proofs about what programs do, or what is possible for programs to do. For example, say I have a simple program with static types. I might want to prove that if the programs type checks, type errors will never occur when you run the program. In order to do this proof, I have to have some formal notion of what it means to "run the program". For a functional language, beta reduction is one of those formal rules.
    - tsimionescu 5y ago
      I will note though that in the actual lambda calculus there is no "+", "2" or "1" - it's functions all the way. 1 is typically defined in the Church encoding as \f -> \x -> f x. Addition is \m -> \n -> \f -> \x -> m f (n f x). Finding the Church encoding of 2 is left as an exceecise. We can then use beta reduction to compute 1 + 1 by replacing m and n with 1: 1 = \f -> \x -> f x (\m -> \n -> \f -> \x -> m f (n f x)) 1 1 =>beta \f -> \x -> 1 f (1 f x) \f -> \x -> 1 f x = (\f -> \x -> f x) f x =>beta 1 f x = f x \f -> \x -> 1 f (1 f x) <=> \f -> \x -> 1 f (f x) (\f -> \x -> f x) f (f x) =>beta \f -> \x -> f f x - the Church encoding of 2. This is how computation using beta reduction only looks like.

dean177 5y ago

Readers will find HOW.md interesting too: https://github.com/Kindelia/HVM/blob/master/HOW.md https://github.com/Kindelia/HVM/blob/master/HOW.md

cwillu 5y ago
“In other words, think of HVM as Rust, except replacing the borrow system by a very cheap .clone() operation that can be used and abused with no mercy. This is the secret sauce! Easy, right? Well, no. There is still a big problem to be solved: how do we incrementally clone a lambda? There is a beautiful answer to this problem that made this all possible. Let's get technical!” Every third paragraph feels like the autogenerated flavour text gibberish of a kerbal space program mission description.
- mrpf1ster 5y ago
  I enjoyed it, you can clearly see the author is excited about explaining his work.
- throwaway17_17 5y ago
  I don’t know that I would go as far as you did, but the writing style is a little bit to hyperbolic or maybe just to rhetorical/conversational for my tastes.
- LightMachine 5y ago
  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.
- hnlmorg 5y ago
  As an author of a language myself and going through the process of documenting it, let me assure you that writing technical docs is several orders of magnitude harder than writing comments on HN. And not only is it hard but it is also extremely time consuming and far less interesting than writing code too. Yet it needs to be done. To that end, the value of community support in writing documentation can never be overstated. So if you have any issues specific issues with his documentation then I'm sure the author would welcome a pull request.

jsnell 5y ago

This had a Show HN a few days ago: https://news.ycombinator.com/item?id=30152714 https://news.ycombinator.com/item?id=30152714

fulafel 5y ago

The submission title says "optimal", the README says "beta-optimal", what do they mean in this context and are they true?

opnitro 5y ago
"Optimal" in this context means it never repeats the work of beta reduction when it doesn't have to. Ie, evaluating `(\x -> x + x) (2 * 2)` only evaluates `2 * 2` once.
- rowanG077 5y ago
  Why is this special? Doesn't that mean GHC is beta optimal since afaik it stores thunks to computations.
  - opnitro 5y ago
    GHC is not beta optimal, due to some complications around what happens when a closures are created. (This is `HOW.md` claims)
- astrange 5y ago
  That's not optimal on real machines; it's often faster to recalculate x*y than to cache it. In general this "optimal" strategy seems to assume infinite memory that's all accessible at the same speed.
  - opnitro 5y ago
    "Beta Optimial" != Fastest Execution strategy for all kinds of code. Just defining the term, not arguing about it's engineering application.
    - astrange 5y ago
      The project certainly says it has "drastically improved efficiency" and "uncharted levels of performance". I don't think "massively parallel" is all that good for performance either, because battery life is part of that.

deleted 5y ago

[deleted]

carterschonwald 5y ago

The fellow behind this has been hammering at experiments around so called optimal reduction strategies for a while! As another commenter’s remarks imply; some of the so called benefits for what are called optimal reduction strategies are limited to efficiently manipulating data structures that are represented by lambdas. And that’s also probably why this is Untyped. Makes it easier to embed / support such an encoding

throwaway17_17 5y ago
Agreed, but the reference he makes to the symmetric interaction calculus blog post seems to at least have basis in sound logic/semantic principles. I haven’t read the whole post, but I am at least willing to give it a chance.
- carterschonwald 5y ago
  Linear logic inspired ideas are always great

yewenjie 5y ago

So many new programming languages coming up with clever features that makes me wish I could mix and match their core features while using libraries from more popular languages. Up and coming Languages I am excited about - 1. Roc - https://www.youtube.com/watch?v=vzfy4EKwG_Y https://www.youtube.com/watch?v=vzfy4EKwG_Y 2. Zig - https://ziglang.org/ https://ziglang.org/ 3. Scopes - https://sr.ht/~duangle/scopes/ https://sr.ht/~duangle/scopes/ 4. Gleam - https://gleam.run/ https://gleam.run/ 5. Odin - https://github.com/odin-lang/Odin https://github.com/odin-lang/Odin 6. Koka - https://github.com/koka-lang/koka https://github.com/koka-lang/koka 7. Unison - https://github.com/unisonweb/unison https://github.com/unisonweb/unison

arc776 5y ago
Nim - https://nim-lang.org/ https://nim-lang.org/ Lets you mix and match other libraries with their native ABI as it compiles to C, C++, ObjC and JS + has excellent FFI.
- metadat 5y ago
  What about support for using Golang or C# packages? That'd be handy. Interesting read about NIM- https://www.quora.com/Why-hasnt-Nim-Nimrod-become-as-popular-as-Go-Rust-and-Swift https://www.quora.com/Why-hasnt-Nim-Nimrod-become-as-popular... Key points: - Nim lacks official support to multiple inheritance or interfaces (as that in Java) or mixin (as that in Ruby). It feels uneasy when implementing common design patterns, which is important for middle to large-sized projects. - The error messages emitted from Nim compiler looks a bit obscure. Sometimes you have to guess or google to comprehend what really happens in your code. These seem like pretty good problems compared to common annoyances and caveats in many other languages.
  - arc619 5y ago
    TBF the reply in that link was written 4 years ago, before the language went 1.0 > Nim lacks official support to multiple inheritance or interfaces Multiple inheritance is a bit of a trainwreck IMO (see diamond problem). The language isn't designed around OOP, and is instead procedural with metaprogramming for extension. You get more bang for your buck this way, but for people with their head in inheritance it’s probably a shock.

afranchuk 5y ago

Really neat. I've been working on a lazy parallel language and so I read the "HOW" document closely to see the secret sauce. What's exciting to me is that, while I'm not familiar with the academia behind their decisions, it seems that I arrived at the same result with regard to their lazy clones: I realized early in the language that caching the eval results would make things really fast, and this caching ends up doing exactly what their lazy clones achieves! Of course one place I don't cache is in function application because the language is not pure (so we want side effects to occur again), but this makes me think it might be really good to derive which functions/subexpressions are pure and allow the cache to be retained through function calls for those. I'm gonna keep a close watch on this. I should probably read more white papers :)

LightMachine 5y ago
Thank you!
chriswarbo 5y ago
> I realized early in the language that caching the eval results would make things really fast, and this caching ends up doing exactly what their lazy clones achieves! Sounds similar to the evaluation model of the Nix expression language (the pure functional programming language used by the Nix package manager). It caches evaluation results, which (a) avoids re-computing identical expressions, and (b) allows some infinite loops to be detected. See https://www.researchgate.net/publication/222827743_Maximal_Laziness_An_Efficient_Interpretation_Technique_for_Purely_Functional_DSLs https://www.researchgate.net/publication/222827743_Maximal_L...
- afranchuk 5y ago
  Thanks for bringing that up! I suspected that nix did that, but wasn't sure. This language is also a "task runner" (being used for build systems mainly), so it's not surprising that it behaves like nix does.

LightMachine 5y ago

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_rationalist 5y ago
How does it compare to https://github.com/beehive-lab/TornadoVM https://github.com/beehive-lab/TornadoVM
- HelloNurse 5y ago
  > TornadoVM accelerates parts of your Java applications on heterogeneous hardware devices such as multicore CPUs, GPUs, and FPGAs. So a HVM-like interpreter could be written in Java or variants thereof (instead of Rust), in order to take advantage of TornadoVM to run efficient lazy evaluation on exotic devices.
auggierose 5y ago
JFYI, the "This book" link on https://github.com/Kindelia/HVM/blob/master/HOW.md https://github.com/Kindelia/HVM/blob/master/HOW.md goes to a research gate page which has the wrong book for download (something about category theory). So, this dup primitive, is that explained in the book as well, or is this a new addition in your implementation?

CyberRabbi 5y ago

A problem with Haskell and with this is that they are inherently only suitable for batch processing. You cannot build interactive systems that have real-time requirements with these languages because how computation is done is not generally under control of the programmer. People attempt to program interactive systems with Haskell but then they spend most of their time adapting their program to GHC’s particular evaluation strategy. Usually the optimized program ends up convoluted and nothing like how Haskell code should look, additionally still with no guarantees on the run time.

tromp 5y ago
Would you say DOOM is interactive with real-time requirements? https://github.com/rainbyte/frag https://github.com/rainbyte/frag
- CyberRabbi 5y ago
  The vast majority of the code in that repository is in the IO monad and uses carefully placed “!” eager evaluation annotations. Both facts only serve to reinforce my point that a programmer must have control over the way in which computations proceed to build interactive applications. Haskell does allow some level of control over this as I said but it ends up not looking like Haskell, it looks like C with funny syntax.
  - travv0 5y ago
    > The vast majority of the code in that repository is in the IO monad and uses carefully placed “!” eager evaluation annotations. Looking through that repository, I believe we have extremely different definitions of "vast majority."
    - CyberRabbi 5y ago
      Nearly everything in Render.hs is in the IO monad. That is a fact, not a subjective opinion. I point out those routines because they are the heart of the application.

gbrown_ 5y ago

I see the author is replying here so I just wanted to say I enjoyed following the Formality posts on your blog and updates on GitHub and hope there's time for more of that in the future. Wishing you all the best with this project! As an aside it may be a convenient reference if you laid out the history of Formality/Kind as I think a large portion of your target audience already knew about Formality. The rename gets a little lost in IMHO, at first glance at least.

deleted 5y ago

[deleted]

mountainriver 5y ago

Really awesome, any thoughts on autodiff?

fritzo 5y ago

Great work Victor, it's so encouraging to see Asperti & Guerrini's research receive engineering attention! Anton Salikhmetov also had some nice implementations [1] a few years ago. As I understand, even Andrea Asperti didn't believe his approach was practical [2] :) Any idea how hard it would be to extend with a nondeterminism operator, as in Plotkin's parallel or? (fork a computation and terminate if either branch terminates) [1] https://dblp.org/pid/49/4772.html https://dblp.org/pid/49/4772.html [2] https://arxiv.org/abs/1701.04240 https://arxiv.org/abs/1701.04240

LightMachine 5y ago
Andrea Asperti's only mistake was thinking he was wrong.

mikewarot 5y ago

Disclaimer: I'm just a Pascal programmer... so I didn't grok the nitty gritty of the lambda calculus, but I think enough to see where this is going. This evokes a similar feeling to when I learned that Lisp wasn't John McCarthy's target programming language. I began to wonder how powerful that intended language would have been, if everyone hadn't stopped at the bootstrap language. There is great power in what is shown, and I suspect even more power in what it enables. I look forward to see where this goes, there clearly could be another similar leap. Question: Does this mean it's possible to rework Rust to remove the accursed borrow checker? (I tried learning Rust, and stopped at the Borrow Checker, so I gotta ask)

namibj 5y ago
For the most part, Rust's borrow checker just serves to verify that non-`unsafe` code doesn't modify/deallocate memory that is still accessible through a different pointer (a reference , in Rust terms; actual (raw) pointers free of such implications can't be used for data access without `unsafe`). They further imply that they are non-NULL and their pointee is dereferenceable (no segfault; correctly aligned) and a valid bitpattern for the pointee type. These assumptions are provided to LLVM, allowing a bunch of optimizations already. Mutable references further guarantee `noalias`/`restrict`, as a mutable reference to some memory location implies no other references to that memory exist, an exclusivity enabling aggressive store-to-load forwarding and elimination of redundant stores. The non-NULL nature makes `Option<&T>` pointer-sized, so semantically nullable pointers have no memory cost and just force explicit handling of their NULL state when accessed (there are convenience method-syntax functions and `match` statements who's cases (patterns, in Rust terms) look like type constructors on the left side of a `=>` and have the inner values bound to the identifiers on the expression to the right of the `=>`). If a function itself returns an `Option`, `foo?` can be used to just unpack a `Some(bar)` and `return None;` on the nullable case. This syntax also works with `Result<T, E>` which allows conveying detailed errors (similar to exceptions, but with performance matching C's negative return codes instead of C++'s unwinding). References are written as `&T` for immutable ones and `&mut T` for mutable ones. Raw pointers are written as `const T` for immutable ones and `mut T` for mutable ones. These guarantees of no-mutable-shared-memory not guarded by explicit `Atomic` types (or concurrent datastructures (I count `Mutex` and `RwLock`)) carry semantic guarantees beyond what an auto-`.clone()` and/or GC can provide. I highly suggest you to try Rust again, but this time using non-lexical-lifetimes (NLL(s)), which shift the lifetime enforcement from simple lexical scope to a control-flow-graph based reachability. They lack the unintuitively-restrictive limitations particularly notable with loops, while still simplifying to abstract over combinatorial path explosion. BorrowChk is your friend, I promise. Just ask in e.g. the Community Discord if you're getting rejected for no good reason despite trying to understand/work around it's complaints. You're not really fighting it; it's more like a sparring partner than an enemy. Also, `.clone()` and `#[derive(Debug, Clone, Copy)]` are your friends when fighting BorrowChk.

FullyFunctional 5y ago

This is incredibly exciting and a tour-de-force. My immediate thoughts are on turning this into a hardware automaton, eg. an FPGA softcore like Reduceron. I see some interesting questions like how to handle user defined rewrite rules, but nothing insurmountable.

deleted 5y ago

[deleted]