From what I can tell this is having a term rewrite system integrated into your language. Is this significantly different then Haskell manual rewrites. Which I admit are sometimes brittle.
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.
You're right about term rewriting as a staged evaluation scheme. Similar to Haskell, I made this PL/compiler for Morgan Stanley where qualified type constraints (for e.g. type classes) are interpreted as stage-0 programs and rewritten into stage-1 programs that compile down to stage-2 programs (so a similar kind of stratification):
https://github.com/morganstanley/hobbes
It looks like this method is aimed at doing user pattern-matching on expressions in the first stage, kind of integrating Haskell-style rewrite rules in the main user language (rather than bolting them on the side in comments).
Major language crush... Everything from the type system to the compilation model to c++ compat just oozes good taste. Glorious structural record types, real union types (my running theory is that expression-based languages lacking these - looking at you, rust - are insufferable) AND variants. Pattern matching, slices, unboxed arrays/primitives, eager evaluation... Damn I love it.
Hobbes looks so totally frickin' awesome, I'm so going to play with this tonight.
Incredible work!
What would be really cool for this language is to hook into jupyterlab via xeus. It's not even that hard to do - I did it for my own (far inferior) toy language.
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.
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.
