Relation to older work like BOHM?

[fritzo]

Hi @VictorTaelin, great work on your clear concise runtime, an approachable HOW.md, and many clever engineering tricks! I'd like to better understand those engineering tricks, especially compared to Asperti's older implementation BOHM (code | paper | book).

1. What are the memory layout tricks?

As I understand, nodes in HVM (a) are variable size (compared to BOHM's fixed size); (b) are packed into 64-bit words where (c) each word contains a pointer to another node, a port in that node, and the type of that node; and (d) elide unnecessary back pointers.

Do I understand correctly that you can (d) elide some pointers because that data is always available in the stack variable in reduce()? Are there other tricks I've missed?

2. How do you know the stack won't intersect itself?

It's cool that you can avoid those backpointers by maintaining a stack. Is there any risk of the stack looping around and intersecting itself via sharing? Or would that always imply the computation is nonterminating and thus irrelevant in practice? If stack self-intersection is allowed, how can you guarantee that a rewrite rule lower in the stack won't invalidate data higher in the stack (e.g. those elided backpointers)?

3. How does HVM track levels?

Lamping's algorithm has extra nodes "croissant" and "bracket", and @asperti simplified these to a single "triangle" node in BOHM. As I understand these nodes are needed for correct computation of level along paths (but my understanding is fuzzy). I don't see an obvious analog in HVM. As I understand PAR represents a fan-out and DP0,DP1 represent fan-ins.

Does HVM have an analog of "croissant", "bracket" or "triangle"? Is this related to VAR and ARG?

4. How do you guarantee "safe" garbage collection (in the technical sense of "safe")?

@asperti's BOHM guards the garbage collection rules for fan (DP0,DP1 in HVM) by a safe flag described in chapter 9 of his book. The situation he's avoiding is the ambiguous propagation of ERA:

And BOHM also uses safety to gate its triangle-fan reductions.
But I don't see an obvious computation of safety in HVM's collect().

Does HVM simply avoid rule requiring "safety"? Have you found a better way to collect garbage since that 1998 book? Sorry if I'm missing something 😊

Awesome project! No hurry in answering. Thanks for any help!

[VictorTaelin]

Great questions!

I'm sadly not too familiar with BOHM, I tried installing it a long time ago, but couldn't. The fact it implemented the full algorithm was unattractive to me, since that decreases the efficiency by ~10x for all the programs that don't need the extra machinery, which are also most of the programs that we care about in practice.

1 Memory Layout

Right now, HVM has a maximum size of 16 pointers per node, so it isn't really varlen. Much more than that would make lazy cloning unpractical. Your understanding about pointers and the stack seems mostly correct. I don't think there are any tricks you missed; it is pretty simple, lam/app nodes don't need a port to their parent, which I included in past implementations. Pointers don't quite include the port they point to, though. Compared to pure interaction nets (not BOHM), the LAM, PAR, CTR, CAL poitners always point to what would be the port 0; the VAR and DP0 pointer to port 1; the APP and DP1 pointer to port 2; the U32 pointer is unboxed.

2 Stack self-intersection

Perhaps I'm missing something you have in mind, in which case perhaps it would help if you could draw an example problematic situation on interaction nets, and I can reply by showing how it would be represented on HVM. But I don't see how a self-intersection would work. The stack only stores paths you passed through. So, for example, when you move from an application to a lambda, you know how to go back to the application, which is important, since the lambda doesn't store a pointer to its parent. But since rewrite rules only happen at the tip of the stack (which represents an active pair), and since the past pointers stored on the stack weren't on the surroundings of an active pair (otherwise we would have stopped there!), then it is impossible for a rewrite rule to affect these pointers.

3 Representation of levels

No, HVM does not have any complex representation of levels, in the form of additional nodes. It is just an implementation of the abstract subset of the optimal evaluation algorithm. The reason is that there isn't any known implementation of a complete "level tracker" (i.e., bookkeeping machinery / oracle) that doesn't decrease the overall efficiency of the machine by at least 10x, which is not acceptable. My observation, though, is that this "level tracker" is only necessary to make sure that the reduction of uninteresting ill λ-terms, is sound.

That said, there is a simpler solution that covers 99% of the λ-calculus, and virtually every useful, real-world λ-term: just store a constant level on every initial fan node. The DP0 and DP1 nodes reserve 24 bits for that. Since it is fixed, HVM isn't able to compute correctly a few λ-terms, but the class of terms it covers is massive. We have an entire dependent type-checker, including a parser, stringifiers, a HOAS-based evaluator, lists, contexts and many recursive algorithms on HVM. People have the impression that HVM is limited to EAL, but that is just not true.

In short, HVM made the compromise of giving up on a few exotic λ-terms, in exchange for a 10x practical speedup, which I consider the best decision until someone finds a bookkeeping algorithm that doesn't impact the efficiency so profoundly.

4 Garbage collection

BOHM uses the safe flag to allow optimizing certain redundant nodes away, which improves its complexity in some cases. This has nothing to do with the "garbage-collection-free" property of interaction nets, though. HVM just frees memory when an erasure rule is triggered, which is sufficient to make it GC-free. The collect() function is just an optimization that frees unreachable subnets without having to compute its redexes, but its result is always the same as running the erasure rules directly.

Since HVM doesn't have control operators, the problem described on chapter 9 is much less relevant for us. That said, there are cases where it impacts HVM's performance. Not in the form of garbage leaks, but in the form of sub-optimal complexity. For example, issue #60 shows some inputs that are quadratic instead of linear, because of accumulating redundant DUP nodes. The "safe" flag would allow us to implement the optimization depicted in that image, which would, I believe, solve that issue.