> Notice also how, in some steps, lambdas were applied to arguments that appeared outside of their bodies. This is all fine, and, in the end, the result is correct.
But one of the example steps is this transformation:
dup a b = {x0 x1}
dup c d = {y0 y1}
(Pair λx0(λy0(Pair a c)) λx1(λy1(Pair b d)))
------------------------------------------------ Dup-Sup
dup c d = {y0 y1}
(Pair λx0(λy0(Pair x0 c)) λx1(λy1(Pair x1 d)))
I think I’m missing a subtlety. This step substitutes the a/b superposition into the lambdas, but I don’t see how it knows the the x0 goes into the first lambda and the x1 goes into the second one. After all, in HVM bizarro-land, lambda arguments have no scope, so the reverse substitution seems equally plausible and even syntactically valid:
(Pair λx0(λy0(Pair x1 c)) λx1(λy1(Pair x0 d)))
This substitution produces two magically entangled lambdas, which seems fascinating but not actually correct. How does the runtime (and, more generally, the computational system it implements) know in which direction to resolve a superposition?
“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.
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.
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.
> Notice also how, in some steps, lambdas were applied to arguments that appeared outside of their bodies. This is all fine, and, in the end, the result is correct.
But one of the example steps is this transformation:
I think I’m missing a subtlety. This step substitutes the a/b superposition into the lambdas, but I don’t see how it knows the the x0 goes into the first lambda and the x1 goes into the second one. After all, in HVM bizarro-land, lambda arguments have no scope, so the reverse substitution seems equally plausible and even syntactically valid: This substitution produces two magically entangled lambdas, which seems fascinating but not actually correct. How does the runtime (and, more generally, the computational system it implements) know in which direction to resolve a superposition?