6 ms·

Interaction Nets, Combinators, and Calculus – HVM

114 points by erlend_sh 4y ago

metadat 4y ago
Discussed today: Higher-Order Virtual Machine (HVM) https://news.ycombinator.com/item?id=35336113 https://news.ycombinator.com/item?id=35336113 (33 comments)
davemp 4y ago
Unfortunate acronym choice considering the term HVM is already used to refer to Hardware assisted Virtual Machines. [0] [0]: https://wiki.xenproject.org/wiki/Xen_Project_Software_Overview#HVM_and_its_variants_.28x86.29 https://wiki.xenproject.org/wiki/Xen_Project_Software_Overvi...
- andai 4y ago
  I think that's OK. Every time I look up a 3 letter initialism on Wikipedia, I have to scroll through dozens of irrelevant articles to find the one I'm looking for.
markusde 4y ago
> A caveat of this technique for reducing lambdas is that it doesn't exactly match the behavior of the normal lambda calculus. While it might reduce the same as the normal lambda calculus in many cases, it doesn't always. And that's totally fine, it doesn't need to match perfectly to be useful in it's own right. This seems like a serious problem for something trying to be so foundational... I'm kind of surprused the author doesn't go into more detail about it. Why is this fine? If not for evaluating arbitrary programs, what is HVM useful for?
- LightMachine 4y ago
  I think this kind of sentence makes such a huge disservice for the HVM. Rust closures also doesn't support the full λ-calculus! HVM supports way more λ-terms than Rust does. That said, we're working on full λ-calculus support, so this shouldn't be a problem soon.
  - markusde 4y ago
    Aha-- so then HVM allows a more efficient reduction of some lambda terms, but is not intended to replace something like GHC core? What is the subset of lambda terms which HVM can (soundly) evaluate?
    - LightMachine 4y ago
      Well, it should be a viable alternative to GHC once we implement full lambdas, but without them, it should be seen as a separate language, just like Rust. The complete subset of lambda terms that HVM can soundly evaluate hasn't been identified yet. It is known that HVM can, at least, soundly evaluate all terms typeable on Elementary Affine Logic (EAL), but, while that is a huge set, it isn't comprehensive, as HVM can evaluate many terms outside of EAL, including recursive terms such as the Y-Combinator.
      - markusde 4y ago
        Interesting-- thanks!
LightMachine 4y ago
Very well written and beautiful article.

114 points by erlend_sh 4y ago

Discussed today: Higher-Order Virtual Machine (HVM) https://news.ycombinator.com/item?id=35336113 https://news.ycombinator.com/item?id=35336113 (33 comments)

davemp 4y ago

Unfortunate acronym choice considering the term HVM is already used to refer to Hardware assisted Virtual Machines. [0] [0]: https://wiki.xenproject.org/wiki/Xen_Project_Software_Overview#HVM_and_its_variants_.28x86.29 https://wiki.xenproject.org/wiki/Xen_Project_Software_Overvi...

andai 4y ago
I think that's OK. Every time I look up a 3 letter initialism on Wikipedia, I have to scroll through dozens of irrelevant articles to find the one I'm looking for.

markusde 4y ago

> A caveat of this technique for reducing lambdas is that it doesn't exactly match the behavior of the normal lambda calculus. While it might reduce the same as the normal lambda calculus in many cases, it doesn't always. And that's totally fine, it doesn't need to match perfectly to be useful in it's own right. This seems like a serious problem for something trying to be so foundational... I'm kind of surprused the author doesn't go into more detail about it. Why is this fine? If not for evaluating arbitrary programs, what is HVM useful for?

LightMachine 4y ago
I think this kind of sentence makes such a huge disservice for the HVM. Rust closures also doesn't support the full λ-calculus! HVM supports way more λ-terms than Rust does. That said, we're working on full λ-calculus support, so this shouldn't be a problem soon.
- markusde 4y ago
  Aha-- so then HVM allows a more efficient reduction of some lambda terms, but is not intended to replace something like GHC core? What is the subset of lambda terms which HVM can (soundly) evaluate?
  - LightMachine 4y ago
    Well, it should be a viable alternative to GHC once we implement full lambdas, but without them, it should be seen as a separate language, just like Rust. The complete subset of lambda terms that HVM can soundly evaluate hasn't been identified yet. It is known that HVM can, at least, soundly evaluate all terms typeable on Elementary Affine Logic (EAL), but, while that is a huge set, it isn't comprehensive, as HVM can evaluate many terms outside of EAL, including recursive terms such as the Y-Combinator.
    - markusde 4y ago
      Interesting-- thanks!

LightMachine 4y ago

Very well written and beautiful article.