Metalanguage

[jonsterling]

It will likely be easier to fire up a "RedML" style metalanguage than it was in RedPRL. A very basic one of these could be a priority, as it would make it easier to fiddle with stuff (like, "print this definition", "evaluate this code", "quote this value", "normalize", etc.).

[jonsterling]

A good first step will be to factor out everything from the elaborator into the refiner, which has already begun.

Then we can recast elaboration as the evaluation semantics of the metalanguage, just like we did in redprl.

[jonsterling]

It's about time to start doing this seriously.

[spitters]

Did you choose for Eff, /-prolog, ... as metalanguage?

[jonsterling]

@spitters I think that it will end up being closer to Eff.

But I also want to clarify that in a project like this, one does not (cannot) just choose an existing language off the shelf, such as Eff or lambda-prolog --- to build a metalanguage for a proof assistant is a matter of language-design, rather than language-adoption or language-integration (the science of proof assistants is not yet at the point where these things can be likened to jigsaw puzzle pieces). So keeping that perspective in mind, I hope to build something inspired in many ways by the metalanguage of Andromeda.

Lambda-prolog is super cool as well, and I'd like to use those ideas in the future, but on reflection, it's not quite what I have in mind with redtt. What would be awesome is to find a way to integrate features from lambda prolog into the ML, maybe even using algebraic effects as an implementation strategy.

[brendanzab]

Curious - why you would choose to use a meta language, and not RedTT itself, like Lean and F* do?

[jonsterling]

It's a good question. The idea of metaprogramming in the same language, which appears in Idris, Lean and Agda, has certainly been shown to be practical and useful. One thing I like about it is that you can prove properties of (e.g.) heuristic decision procedures, etc. Note that I would characterize this as saying that Lean^0's metalanguage is Lean^1, rather than that they chose not to use a metalanguage.

On the other hand, the main problem in my view is that metalanguages usually have features which we don't know a principled type-theoretic interpretation of. This includes things like control effects (for instance, the algebraic effects and handlers that appear in Andromeda; but also other stuff, including store and even IO!). One approach, which is used by Lean, Agda, Idris, is to bung all the stuff you need into a monad, but I feel that this is not really what we should aim for.

In the next decade, I anticipate that we will find more direct accounts of sophisticated programming language features like these, principally effects, in a type-theoretically sensible way. In the meanwhile, I'd like to study metalanguage design as a language design issue, rather than either trying to shoehorn everything into a monad in the redtt core language, or trying to solve all problems of type theoretic semantics simultaneously.

By the way, one way to mediate between these things is to provide a way to reflect data from the metalanguage into the object language, and then let the metalanguage call functions in the object language, and get their results. This lets you do all the cool stuff that comes from having a metalanguage that resembles the object language, but without needing them to literally be the same.

[brendanzab]

Yeah, I can see the effects could be a pain, and it's just be nice to sidestep it for now. Thanks for explaining your reasoning!

[favonia]

Can we close this issue now?