5 ms·

This looks pretty awesome, and holds much promise for the future. Optimal beta reduction has always seemed like something of theoretical interest only, but Vict

by 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`.
      - LightMachine 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. 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.
        capableweb 5y ago
        Just wanted to clarify that I definitely don't think this looks like a bad language as-is, I don't want to give the impression because of this small preference, it's less valuable (but I'm sure you knew that already). It's really impressive design, congratulations on getting it out for the world to play with :)
      - 5y ago
- 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!

by tromp 5y ago

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`.
    - LightMachine 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. 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.
      - capableweb 5y ago
        Just wanted to clarify that I definitely don't think this looks like a bad language as-is, I don't want to give the impression because of this small preference, it's less valuable (but I'm sure you knew that already). It's really impressive design, congratulations on getting it out for the world to play with :)
    - 5y ago
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!