### Beta-reduction

After a 7-month hiatus, I'm back to working on the implementation of Deep. I scrapped much of the earlier code, and replaced it with a simpler design. My focus is getting the type system up and running.

I have been struggling to implement beta-reduction "properly", which turned out to be surprisingly tricky. The earlier version of my interpreter used Bruin indices and a closure-based execution model that was reasonably efficient.

To do partial evaluation and dependent types, however, I need to keep expressions in a symbolic form, with explicit sharing of common subexpressions. After toying with various arcane environment manipulations, I finally turned to the literature to see what the standard approach was, only to find that it's still a topic of ongoing research. I would have expected efficient beta-reduction to be a completely solved problem by now. :-)

In the meantime, I have scrapped the Bruin indices, and gone back to simple rewrites, with a bit of lazy copying to avoid the worst performance bottlenecks.

I have been struggling to implement beta-reduction "properly", which turned out to be surprisingly tricky. The earlier version of my interpreter used Bruin indices and a closure-based execution model that was reasonably efficient.

To do partial evaluation and dependent types, however, I need to keep expressions in a symbolic form, with explicit sharing of common subexpressions. After toying with various arcane environment manipulations, I finally turned to the literature to see what the standard approach was, only to find that it's still a topic of ongoing research. I would have expected efficient beta-reduction to be a completely solved problem by now. :-)

In the meantime, I have scrapped the Bruin indices, and gone back to simple rewrites, with a bit of lazy copying to avoid the worst performance bottlenecks.