Because of the nondeterminism we get from the metalanguage being a logic language, we don't have to worry about applying optimizers in a particular order. You can compose optimizers together, produce the possible results, and then select the best using a heuristic. Of course, the search space is potentially huge, so I'm looking into integrating constraints.

Yes. As I’ve said elsewhere, the system is not limited to simple term rewrites.

Is there an example of such a program? I don't see anything like that in the github repo.

Unfortunately not! Embarrassingly, I haven't implemented pattern matching yet, which means functions like `sum` and `filter` can't be written. So far all my effort has gone towards the metaprogramming system. Bugfixing has me occupied at the moment, but after that I plan on doing pattern matching.

The difference is that it’s much more general - the metalanguage is an actual logic language, not limited to simple rewrites. You can (read: will be able to, haha) prove properties about meta-level program transformations. For those interested, I’m basing my system off of Twelf and Abella.

Any inspiration taken from Shen?

I saw it a while back and thought the ideas were cool, but I didn’t check it out in enough detail to draw inspiration from it.

Not really. A detailed account of 2LTT can be found in this paper https://arxiv.org/abs/1705.03307 - 2LTT can be thought of as a general, type theoretic framework for metaprogramming.

Is there an introduction to 2LTT for those with only a basic understanding of type theory?

Unfortunately there isn't, but I'll try my best here: In two level type theory, your language is actually two languages - a "meta language" (or meta level) and an "object language" (or object level). Additionally, we have a construct for relating object-level terms/types to meta-level terms/types. There are other, more type theory heavy qualifiers, but that's the basic idea.

It's quite a simple system, but it turns out to subsume quite a lot of others. Depending on how your conversion construct behaves, you can get vastly different metaprogramming systems.

The most important consideration when determining what you can do with 2LTT is how "similar" your two languages are, in a rough sense of the word. Remember that these really are two separate languages - they can have entirely different features and behave completely differently. Peridot is actually a good example, the object language is functional and dependently typed, while the meta language is more akin to λProlog or Twelf (it's a logic language).

If the two languages are identical, you can get something akin to partial evaluation for example. Peridot is on the other end of the spectrum, where the languages are completely dissimilar.

Note that 2LTT is actually even more broad than this. I'm talking specifically about 2LTT's applications to metaprogramming, but the authors of that paper used it to overcome some limitations of theorem proving in homotopy type theory.

TL;DR: In two-level type theory, your language is really two languages (levels) stuck together. You also have a construct to relate object-level terms/types to meta-level terms/types (notably, the reverse is not allowed). Depending on how this construct works, you can get all kinds of metaprogramming systems.