Higher-Order Virtual Machine (HVM)

Higher-Order Virtual Machine (HVM)
github.com

Nonetheless, I eagerly await its future.

https://github.com/inpla/inpla/blob/main/Gentle_introduction...

I've noticed HVM since February last year and was quite convinced that they were really up to something; however now that I've gone through a pile of papers on Linear Logic and the book which HVM is based on (The Optimal Implementation of Functional Programming Languages, Asperti and Guerrini, https://www.amazon.co.jp/-/en/Andrea-Asperti/dp/0521621127), I believe that among other things, the issue presented here https://github.com/HigherOrderCO/HVM/issues/60 is really a fundamental blocker to serving as a general purpose runtime, which it appears HVM attempts at.

Fundamentally HVM is an impressively optimised implementation of Symmetric Interaction Combinators, a variety of Interaction Net. Symmetric Interaction Combinators is not related to lambda calculus in a trivial way, and thus as noted in the README, HVM does not 'support' the full Lambda Calculus. In a vast majority of cases the HVM approach really does simply evaluate lambda terms at impressive speed, but the failure cases are quite tricky to handle, in that they will fail silently, simply evaluating the term incorrectly. This issue however, is acknowledged in the README and can be tackled by the method described there, or by type-checking for these 'failure' cases https://github.com/HigherOrderCO/HVM/discussions/97.

The issue mentioned in #60 however, seems to be quite fundamental - HVM makes lambda evaluation fast by implementing lambda evaluation in terms of Symmetric Interaction Combinators and making sure each operation of SIC evaluates in constant time. This works in most cases, but as acknowledged in Asperti and Guerrini, in some cases the SIC representation of lambda terms simply become themselves very (exponentially) large. Victor appears to acknowledge that he is simply building a practical counterpart upon the theory as cited from Asperti and Guerrini, citing Asperti and Guerrini's 'safe rules', which has not yet been implemented, as his plan to prevent very large representations of lambda terms from occurring, but Asperti and Guerrini themselves acknowledge that their rules are probably incomplete. Crucially, these terms appear to show up in regular functional programming folds.

The promise of HVM is that we have finally found a way to naturally implement the parallelism inherent in pure lambda terms, without special annotation or extra accommodation for the runtime. As it stands, HVM still falls short of the lofty dream.