https://gitlab.com/bss03/grtt is my published code. But, I have far more intuitions that I need to write code for than finished code.

While evaluating something well-typed under a context, the heap: does not need to contain a value for a binder with modality 0, must contain a single, strict value for a binder with a modality 1, must contain a single, lazy closure for a binder with a modality of ?, must contain multiple references to a shared, strict value for a binder with a modality n, must contain at least a single reference to a strict value for a binder with a modality of +, must contain at least a single reference to a lazy closure for a binder with a modality of *. Since the typing rules propagate the modalities to subterms precisely, we should be able to identify the exact point a closure must be forced to a value (or dropped) before runtime. That’s in addition to being able to compile linear functions to heap updates, eliminating at least some allocations.

There’s some similarities with both the exact-use-count and relevant-or-erased semirings, but I think some things (e.g. around sums) are hard/awkward/impossible to type and the ?/+/* modalities make some make things easier while still allowing the abstract machine to know exactly when to “optimize the heap” based on a runtime flow that “activates” a particular static analysis.

Of course, it’s still MLTT “compatible” – anything that would type-check in MLTT should type-check in my variation of GRTT by “simply” using the * modality everywhere – so you get full proofs-as-programs and a total language.

I’m probably a bit off in the weeds, but it still makes my brain buzz to think about and occasionally I’ll make progress. I’ve been a little bit distracted with https://gitlab.com/bss03/nested which should allow me to write the abstract machine as a fold, but as proven to be place I can also put a lot of programming time into (again, with sporadic real progress).